Book X · Proposition 73

X.73

If from a rational straight line there be subtracted a rational straight line commensurable with the whole in square only, the remainder is irrational; and let it be called an apotome.Heath, 1908

Every step, checked

• both lines are rational in squaregiven
• they are commensurable in square onlygiven
• the remainder is irrationalby X.73
• Book X calls it an apotomeby X.73
• and assigns it one of the six speciesby X.85-90

What it needs, and what needs it

Needs: nothing earlier.

Used by: X.85 X.86 X.87 X.88 X.89 X.90 XIII.6 XIII.11 XIII.16 XIII.17 XIII.18

Rests on: X.85-90

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(
    "X.73",
    THEOREM,
    sample=_rational_pair_in_square_only,
)
def prop_X_73(a, b) -> Out:
    hypothesis("both lines are rational in square", is_rational_in_square(a) and is_rational_in_square(b))
    hypothesis("they are commensurable in square only", not commensurable(a, b))
    greater, lesser = (a, b) if sign(a - b) > 0 else (b, a)
    remainder = greater - lesser
    claim("the remainder is irrational", "X.73", not isinstance(remainder, Fraction))
    named = classify(remainder)
    claim("Book X calls it an apotome", "X.73", named.family == "apotome")
    claim("and assigns it one of the six species", "X.85-90",
          named.species in ("first", "second", "third", "fourth", "fifth", "sixth"))
    return Out(apotome=remainder, species=named.species)