G.357 odd number odd

IX.26

If from an odd number an odd number be subtracted, the remainder is even.

odd_number_odd()

prove / A C / is even

construct From the odd number / A B / let the odd number / B C / be subtracted

construct Since / A B / is odd, let the unit / B D / be subtracted ;

∵ odd_number_divisible_defassert / A D / is even

∵ odd_number_divisible_defassert For the same reason / C D / is also even

∵ even_number_even∴ So that / A C / is also even

Dependency Graph