Book X · Proposition 75

X.75

If from a medial straight line there be subtracted a medial straight line which is commensurable with the whole in square only, and which contains with the whole a medial rectangle, the remainder is irrational; and let it be called a second apotome of a medial straight line.Heath, 1908

Every step, checked

• the greater term is the greatergiven
• the remainder is irrationalby X.75
• and it is second apotome of a medial lineby X.75

What it needs, and what needs it

Needs: nothing earlier.

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(ref, THEOREM, sample=_kind_sample(kind))
def _difference(a, b, _k=kind) -> Out:
    hypothesis("the greater term is the greater", sign(a - b) > 0)
    remainder = a - b
    claim("the remainder is irrational", ref,
          not isinstance(remainder, Fraction))
    claim(f"and it is {SUBTRACTED_NAMES[_k]}", ref,
          classify(remainder).name == SUBTRACTED_NAMES[_k])
    return Out(remainder=remainder)