Book X · Proposition 37

X.37

If two medial straight lines commensurable in square only and containing a rational rectangle be added together, the whole is irrational; and let it be called a first bimedial straight line.Heath, 1908

Every step, checked

• both lines are medialgiven
• they are commensurable in square onlygiven
• the rectangle they contain is rationalgiven
• the whole is irrationalby X.37
• and it is a first bimedialby X.37

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.37",
    THEOREM,
    sample=_medial_pair,
)
def prop_X_37(a, b) -> Out:
    hypothesis("both lines are medial", is_medial(a) and is_medial(b))
    hypothesis("they are commensurable in square only", not commensurable(a, b))
    hypothesis("the rectangle they contain is rational", is_rational_line(a * b))
    whole = a + b
    claim("the whole is irrational", "X.37", not isinstance(whole, Fraction))
    claim("and it is a first bimedial", "X.37", classify(whole).name == "first bimedial")
    return Out(bimedial=whole)