Book IX · Proposition 13

IX.13

If as many numbers as we please beginning from an unit be in continued proportion, and the number after the unit be prime, the greatest will not be measured by any except those which have a place among the proportional numbers.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: IX.12

Depth: 2 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.13",
    THEOREM,
    sample=lambda rng: (rng.choice([p for p in range(2, 20) if is_prime(p)]),
                        rng.randint(4, 7)),
)
def prop_IX_13(prime: int, count: int) -> Out:
    hypothesis("the number after the unit is prime", is_prime(prime))
    hypothesis("the progression is genuine", count >= 4, guard=True)
    terms = [prime ** k for k in range(count)]
    because(prop_IX_12, prime, count) if prime > 1 and count >= 4 else None

    claim("the greatest is measured by no number outside the progression", "IX.12",
          all(measures(d, terms[-1]) == (d in terms)
              for d in range(1, terms[-1] + 1) if measures(d, terms[-1])))
    return Out(terms=terms)