G.361 odd number measure

IX.30

If an odd number measure an even number, it will also measure the half of it.

odd_number_measure()

prove it will also measure the half of it; C is not odd

assert Let the odd number A measure the even number B

assert A measures B, let it measure it according to C

assert If possible, let it be so

assert A measures B according to C,

assert A by multiplying C has made B

assert B is made up of odd numbers the multitude of which is odd

∵ many_odd_numbers_ix_23assert B is odd ⇒⇐, for by hypothesis it is even

assert C is not odd; therefore C is even

assert A measures B an even number of times

∴ For this reason then it also measures the half of it

Dependency Graph

Required for

G.362