G.284 prime number prime

VII.29

Any prime number is prime to any number which it does not measure.

prime_number_prime(A, B)

given A be a prime number, let it not measure B

prove B, A are prime to one another

given A be a prime number, let it not measure B

assert If B, A are not prime to one another, some number will measure them

assert Let C measure them

assert C measures B, and A does not measure B,

assert C is not the same with A

assert C measures B, A,

assert it also measures A which is prime, though it is not the same with it ⇒⇐

assert no number will measure B, A

∴ A, B are prime to one another

Dependency Graph

Required for

G.285, G.342, G.343, G.344, G.364, G.370