G.366 number half odd

IX.33

If a number have its half odd, it is even-times odd only.

number_half_odd()

prove A is even-times odd only

assert Let the number A have its half odd

∵ even_times_odd_defassert Now that it is even-times odd is manifest; for the half of it, being odd, measures it an even number of times

assert I say next that it is also even-times odd only

assert If A is even-times even also,

∵ even_times_even_defassert It will be measured by an even number according to an even number

assert So that the half of it will also be measured by an even number though it is odd ⇒⇐

∴ A is even-times odd only

Dependency Graph