Book IX · Proposition 17

IX.17

If there be as many numbers as we please in continued proportion, and the extremes of them be prime to one another, the last will not be to any other number as the first to the second.Heath, 1908

Every step, checked

• the ratio is a genuine onegiven
• a genuine progression is asked forgiven
• the extremes are prime to one anothergiven
• the first does not measure the secondby VIII.6
• so the last is to no other number as the first is to the secondby IX.16

What it needs, and what needs it

Needs: VIII.6 IX.16

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.17",
    THEOREM,
    sample=progression,
)
def prop_IX_17(p: int, q: int, count: int) -> Out:
    hypothesis("the ratio is a genuine one", p > 1 and q > 1, guard=True)
    hypothesis("a genuine progression is asked for", count >= 3, guard=True)
    terms = continued_proportion(1, (p, q), count)
    hypothesis("the extremes are prime to one another", coprime(terms[0], terms[-1]))
    because(prop_IX_16, terms[0], terms[-1])
    because(prop_VIII_6, p, q, count)

    claim("the first does not measure the second", "VIII.6",
          not measures(terms[0], terms[1]))
    claim("so the last is to no other number as the first is to the second", "IX.16",
          not any(terms[0] * c == terms[1] * terms[-1]
                  for c in range(1, terms[1] * terms[-1] + 1)))
    return Out()