Book X · Proposition 7

X.7

Incommensurable magnitudes have not to one another the ratio which a number has to a number.Heath, 1908

Every step, checked

• the magnitudes are positivegiven
• they are incommensurablegiven
• their ratio is not that of any number to a numberby X.7
• and no pair of numbers puts them in proportionby X.5

What it needs, and what needs it

Needs: X.5

Depth: 4 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.7",
    THEOREM,
    sample=_incommensurable_pair,
)
def prop_X_7(a, b) -> Out:
    hypothesis("the magnitudes are positive", sign(a) > 0 and sign(b) > 0, guard=True)
    hypothesis("they are incommensurable", not commensurable(a, b))
    # X.5 speaks of commensurable magnitudes, and this proposition is about the
    # pair that are not: Euclid reaches it by supposing the contrary, so the
    # appeal has no figure here that is not the one being refuted.
    claim("their ratio is not that of any number to a number", "X.7",
          not isinstance(a / b, Fraction))
    claim("and no pair of numbers puts them in proportion", "X.5",
          not any(a * q == b * p
                  for p in range(1, 25) for q in range(1, 25)))
    return Out()