Book X · Proposition 15

X.15

If two commensurable magnitudes be added together, the whole will also be commensurable with each of them; and, if the whole be commensurable with one of them, the original magnitudes will also be commensurable.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• they are commensurablegiven
• the whole is commensurable with each of themby X.15
• and conversely, a whole commensurable with one makes them commensurableby X.15

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(
    "X.15",
    THEOREM,
    sample=_commensurable_pair,
)
def prop_X_15(a, b) -> Out:
    hypothesis("the magnitudes are positive", sign(a) > 0 and sign(b) > 0, guard=True)
    hypothesis("they are commensurable", commensurable(a, b))
    claim("the whole is commensurable with each of them", "X.15",
          commensurable(a + b, a) and commensurable(a + b, b))
    claim("and conversely, a whole commensurable with one makes them commensurable",
          "X.15", commensurable(a + b, a) == commensurable(a, b))
    return Out(whole=a + b)