Book IX · Proposition 11

IX.11

If as many numbers as we please beginning from an unit be in continued proportion, the less measures the greater according to some one of the numbers which have place among the proportional numbers.Heath, 1908

Every step, checked

• the progression is genuinegiven
• the less measures the greaterby IX.11
• and the quotient is itself one of the proportional numbersby IX.11

What it needs, and what needs it

Needs: nothing earlier.

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.11",
    THEOREM,
    sample=_from_a_unit,
)
def prop_IX_11(ratio: int, count: int) -> Out:
    hypothesis("the progression is genuine", ratio > 1 and count >= 4, guard=True)
    terms = [ratio ** k for k in range(count)]
    claim("the less measures the greater", "IX.11",
          all(measures(terms[i], terms[j])
              for i in range(count) for j in range(i, count)))
    claim("and the quotient is itself one of the proportional numbers", "IX.11",
          all(terms[j] // terms[i] in terms
              for i in range(count) for j in range(i, count)))
    return Out(terms=terms)