Book X · Proposition 14

X.14

If four straight lines be proportional, and the square on the first be greater than the square on the second by the square on a straight line commensurable with the first, the square on the third will also be greater than the square on the fourth by the square on a straight line commensurable with the third.Heath, 1908

The condition that sorts the six binomial species: whether the line whose square is the excess is commensurable with the greater.

Every step, checked

• the magnitudes are positivegiven
• the four are proportionalgiven
• the squares of the greater exceed those of the lessgiven
• the excess passes across the proportionby X.11

What it needs, and what needs it

Needs: X.11

Depth: 1 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.14",
    THEOREM,
    sample=_four_lines_with_excess,
    note="The condition that sorts the six binomial species: whether the line "
    "whose square is the excess is commensurable with the greater.",
)
def prop_X_14(a, b, c, d) -> Out:
    hypothesis("the magnitudes are positive", all(sign(x) > 0 for x in (a, b, c, d)), guard=True)
    hypothesis("the four are proportional", a * d == b * c)
    hypothesis("the squares of the greater exceed those of the less",
               sign(a * a - b * b) > 0 and sign(c * c - d * d) > 0)
    first = sqrt(a * a - b * b)
    second = sqrt(c * c - d * d)
    because(prop_X_11, a, b, c, d) if a * d == b * c else None

    claim("the excess passes across the proportion", "X.11",
          commensurable(first, a) == commensurable(second, c))
    return Out(excesses=(first, second))