Book VIII · Proposition 9

VIII.9

If two numbers be prime to one another, and numbers fall between them in continued proportion, then, however many numbers fall between them in continued proportion, so many will also fall between each of them and an unit in continued proportion.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: VIII.2

Rests on: Def.VII.20

Depth: 4 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.9",
    THEOREM,
    sample=progression,
)
def prop_VIII_9(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]))
    # p^(n-1) and q^(n-1) are the extremes; each reaches down to a unit through
    # its own powers, and there are as many steps as there were between them.
    to_unit_first = [q ** k for k in range(count)]
    to_unit_last = [p ** k for k in range(count)]
    because(prop_VIII_2, p, q, count) if coprime(p, q) else None

    claim("a progression runs from a unit up to each extreme", "VIII.2",
          in_continued_proportion(to_unit_first) and in_continued_proportion(to_unit_last)
          and to_unit_first[0] == 1 and to_unit_last[0] == 1)
    claim("with as many terms between as fell between the extremes", "VIII.9",
          len(to_unit_first) == count and len(to_unit_last) == count)
    return Out(first=to_unit_first, last=to_unit_last)