Book IX · Proposition 8

IX.8

If as many numbers as we please beginning from an unit be in continued proportion, the third from the unit will be square, as will also those which successively leave out one; the fourth will be cube, as will also all those which leave out two; and the seventh will be at once cube and square, as will also those which leave out five.Heath, 1908

Reading a progression from a unit as powers: the third term is a square, the fourth a cube, the seventh both -- because 2, 3 and 6 are.

Every step, checked

• the progression is genuinegiven
• the terms are in continued proportion from a unitby Def.VII.20
• the third from the unit is square, and so are the alternate onesby IX.8
• the fourth is cube, and so is every third after itby IX.8
• and the seventh is at once square and cubeby IX.8

What it needs, and what needs it

Needs: nothing earlier.

Used by: IX.9 IX.10

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.8",
    THEOREM,
    sample=_from_a_unit,
    note="Reading a progression from a unit as powers: the third term is a "
    "square, the fourth a cube, the seventh both -- because 2, 3 and 6 are.",
)
def prop_IX_8(ratio: int, count: int) -> Out:
    hypothesis("the progression is genuine", ratio > 1 and count >= 7, guard=True)
    terms = [ratio ** k for k in range(count)]  # 1, r, r^2, ...
    claim("the terms are in continued proportion from a unit", "Def.VII.20",
          terms[0] == 1 and in_continued_proportion(terms))
    claim("the third from the unit is square, and so are the alternate ones",
          "IX.8", all(is_square(terms[k]) for k in range(2, count, 2)))
    claim("the fourth is cube, and so is every third after it", "IX.8",
          all(is_cube(terms[k]) for k in range(3, count, 3)))
    claim("and the seventh is at once square and cube", "IX.8",
          is_square(terms[6]) and is_cube(terms[6]))
    return Out(terms=terms)