Book IX · Proposition 27

IX.27

If from an odd number an even number be subtracted, the remainder will be odd.Heath, 1908

Every step, checked

• an odd number has an even subtractedgiven
• the subtraction is a proper onegiven
• the remainder is oddby IX.25

What it needs, and what needs it

Needs: IX.25

Rests on: Def.VII.6

Depth: 4 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.27", THEOREM,
             sample=lambda rng: _pair_by_parity(rng, False, True))
def prop_IX_27(a: int, b: int) -> Out:
    hypothesis("an odd number has an even subtracted",
               not measures(2, a) and measures(2, b))
    hypothesis("the subtraction is a proper one", a > b, guard=True)
    because(prop_IX_25, a, b) if measures(2, a) and not measures(2, b) and a > b else None

    because(prop_IX_25, a + b, b) if measures(2, a + b) and not measures(2, b) else None

    claim("the remainder is odd", "IX.25", not measures(2, a - b))
    return Out(remainder=a - b)