G.362 odd number prime

IX.31

If an odd number be prime to any number, it is prime to the double of it.

odd_number_prime()

prove A is prime to C

assert Let the odd number A be prime to any number B, and let C be double of B

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

assert Let a number measure them, and let it be D

assert Now A is odd

assert D is also odd

assert D which is odd measures C, and C is even,

∵ odd_number_measureassert [D] will measure the half of C also

assert B is half of C

assert D measures B

assert It also measures A

assert D measures A, B which are prime to one another ⇒⇐

assert A cannot but be prime to C

∴ A, C are prime to one another

Dependency Graph