Book VIII · Proposition 7

VIII.7

If there be as many numbers as we please in continued proportion, and the first measure the last, it will measure the second also.Heath, 1908

Every step, checked

• the ratio and length are genuinegiven
• the first measures the lastgiven
• then it measures the second alsoby VIII.7
• and indeed every one of themby VIII.6

What it needs, and what needs it

Needs: VIII.6

Depth: 1 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(
    "VIII.7",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 5), rng.randint(3, 5)),
)
def prop_VIII_7(ratio: int, count: int) -> Out:
    """A progression whose ratio is a whole number, so the first measures the last."""
    hypothesis("the ratio and length are genuine", ratio > 1 and count >= 3, guard=True)
    terms = continued_proportion(1, (ratio, 1), count)
    hypothesis("the first measures the last", measures(terms[0], terms[-1]))

    claim("then it measures the second also", "VIII.7", measures(terms[0], terms[1]))
    claim("and indeed every one of them", "VIII.6",
          all(measures(terms[0], term) for term in terms))
    return Out(terms=terms)