Book IX · Proposition 35

IX.35

If as many numbers as we please be in continued proportion, and there be subtracted from the second and the last numbers equal to the first, then, as the excess of the second is to the first, so will the excess of the last be to all those before it.Heath, 1908

The sum of a geometric series, and the step IX.36 needs. Euclid states it as a proportion because he has no formula to state.

Every step, checked

• the progression is genuinegiven
• the terms are in continued proportionby Def.VII.20
• as the excess of the second is to the first, so is the excess of the last to all those before itby IX.35
• which sums the seriesby IX.35

What it needs, and what needs it

Needs: nothing earlier.

Used by: IX.36

Rests on: Def.VII.20

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.35",
    THEOREM,
    sample=lambda rng: (rng.randint(2, 5), rng.randint(3, 6)),
    note="The sum of a geometric series, and the step IX.36 needs. Euclid states "
    "it as a proportion because he has no formula to state.",
)
def prop_IX_35(ratio: int, count: int) -> Out:
    hypothesis("the progression is genuine", ratio > 1 and count >= 3, guard=True)
    terms = [ratio ** k for k in range(count)]
    excess_of_second = terms[1] - terms[0]
    excess_of_last = terms[-1] - terms[0]
    before = sum(terms[:-1])

    claim("the terms are in continued proportion", "Def.VII.20",
          in_continued_proportion(terms))
    claim("as the excess of the second is to the first, so is the excess of the "
          "last to all those before it", "IX.35",
          excess_of_second * before == terms[0] * excess_of_last)
    claim("which sums the series", "IX.35",
          before * (ratio - 1) == terms[-1] - terms[0])
    return Out(total=before)