Book IX · Proposition 28

IX.28

If an odd number by multiplying an even number make some number, the product will be even.Heath, 1908

Every step, checked

• an odd number multiplies an even onegiven
• the product is evenby IX.21

What it needs, and what needs it

Needs: IX.21

Rests on: Def.VII.6

Depth: 1 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition("IX.28", THEOREM,
             sample=lambda rng: _pair_by_parity(rng, False, True))
def prop_IX_28(a: int, b: int) -> Out:
    hypothesis("an odd number multiplies an even one",
               not measures(2, a) and measures(2, b))
    because(prop_IX_21, [a]) if measures(2, a) else None

    because(prop_IX_21, [a * b]) if measures(2, a * b) else None

    claim("the product is even", "IX.21", measures(2, a * b))
    return Out(product=a * b)