Book IX · Proposition 30

IX.30

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

Every step, checked

• the number is oddgiven
• it measures an even numbergiven
• it measures the half of it as wellby IX.30

What it needs, and what needs it

Needs: nothing earlier.

Used by: IX.31

Depth: 0 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.30", THEOREM,
             sample=lambda rng: (2 * rng.randint(1, 15) + 1, rng.randint(1, 20)))
def prop_IX_30(number: int, multiple: int) -> Out:
    # The multiple is arbitrary and the evenness is a hypothesis, so oddness has
    # something to do. Building the even number as ``number * 2 * multiple``
    # instead makes the half divisible whatever the parity, and the proposition
    # then holds for reasons of its own construction: 4 measures 12 and does not
    # measure 6, and no such case could arise.
    product = number * multiple
    hypothesis("the number is odd", not measures(2, number))
    hypothesis("it measures an even number", measures(2, product))
    claim("it measures the half of it as well", "IX.30", measures(number, product // 2))
    return Out(half=product // 2)