Book X · Proposition 20

X.20

If a rational area be applied to a rational straight line, it produces as breadth a straight line rational and commensurable in length with the straight line to which it is applied.Heath, 1908

Every step, checked

• the line is rationalgiven
• the area applied is rationalgiven
• the breadth produced is rationalby X.20
• and commensurable in length with the line applied toby X.20

What it needs, and what needs it

Needs: nothing earlier.

Used by: X.22

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.20",
    THEOREM,
    sample=_rational_pair_commensurable,
)
def prop_X_20(a, b) -> Out:
    """The converse of X.19: dividing a rational area by a rational line."""
    hypothesis("the line is rational", is_rational_line(a) and sign(a) > 0)
    area = a * b
    hypothesis("the area applied is rational", is_rational_area(area))
    breadth = area / a
    claim("the breadth produced is rational", "X.20", is_rational_line(breadth))
    claim("and commensurable in length with the line applied to", "X.20",
          commensurable(breadth, a))
    return Out(breadth=breadth)