Book X · Proposition 13

X.13

If two magnitudes be commensurable, and the one of them be incommensurable with any magnitude, the remaining one will also be incommensurable with the same.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• the first two are commensurablegiven
• the first is incommensurable with the thirdgiven
• then the second is incommensurable with it tooby X.13

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.13",
    THEOREM,
    sample=lambda rng: _commensurable_pair(rng) + (_magnitude(rng),),
)
def prop_X_13(a, b, c) -> Out:
    hypothesis("the magnitudes are positive", all(sign(x) > 0 for x in (a, b, c)), guard=True)
    hypothesis("the first two are commensurable", commensurable(a, b))
    hypothesis("the first is incommensurable with the third", not commensurable(a, c))
    claim("then the second is incommensurable with it too", "X.13",
          not commensurable(b, c))
    return Out()