Book IX · Proposition 34

IX.34

If a number neither be one of those which are continually doubled from a dyad, nor have its half odd, it is both eventimes even and even-times odd.Heath, 1908

Every step, checked

• the number is neither a doubling from a dyad nor has an odd halfgiven
• it is even-times even, being measured by an even number an even number of timesby Def.VII.8
• and also eventimes odd, being measured by an even number an odd number of timesby Def.VII.9

What it needs, and what needs it

Needs: nothing earlier.

Rests on: Def.VII.8, Def.VII.9

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.34", THEOREM,
             sample=lambda rng: (rng.randint(2, 5), 2 * rng.randint(1, 10) + 1))
def prop_IX_34(power: int, odd: int) -> Out:
    number = 2 ** power * odd
    hypothesis("the number is neither a doubling from a dyad nor has an odd half",
               power >= 2 and odd > 1 and not measures(2, odd))
    claim("it is even-times even, being measured by an even number an even number "
          "of times", "Def.VII.8", measures(4, number))
    claim("and also eventimes odd, being measured by an even number an odd number "
          "of times", "Def.VII.9", measures(2, number) and measures(odd, number))
    return Out(number=number)