Book IX · Proposition 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
Needs: IX.12
Depth: 2 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@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)