Book VIII · Proposition 1

VIII.1

If there be as many numbers as we please in continued proportion, and the extremes of them be prime to one another, the numbers are the least of those which have the same ratio with them.Heath, 1908

The extremes of a progression being coprime is what makes it the least of its kind -- and VIII.3 is the converse.

Every step, checked

What it needs, and what needs it

Needs: VII.20 VII.21

Used by: VIII.2

Rests on: Def.VII.20

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(
    "VIII.1",
    THEOREM,
    sample=progression,
    note="The extremes of a progression being coprime is what makes it the least "
    "of its kind -- and VIII.3 is the converse.",
)
def prop_VIII_1(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]))

    # Consecutive terms are *not* coprime -- p^k q^(n-1-k) and its successor
    # share p^k q^(n-2-k). What makes the progression least is that the whole
    # set has no common measure, which the extremes being coprime forces.
    because(prop_VII_20, terms[0], terms[-1], terms[0], terms[-1])
    because(prop_VII_21, terms[0], terms[-1]) if coprime(terms[0], terms[-1]) else None

    claim("the numbers are in continued proportion", "Def.VII.20",
          in_continued_proportion(terms))
    claim("the terms have no common measure but a unit", "VII.21",
          common_measure(terms) == 1)
    claim("so no smaller progression has the same ratios", "VII.20",
          not any(all(measures(d, term) for term in terms)
                  for d in range(2, min(terms) + 1)))
    return Out(terms=terms)