Book X · Proposition 39

X.39

If two straight lines incommensurable in square which make the sum of the squares on them rational, but the rectangle contained by them medial, be added together, the whole straight line is irrational : and let it be called major.Heath, 1908

The major line. Its two terms are incommensurable even in square, which is what puts it beyond the bimedials.

Every step, checked

• the two are incommensurable in squaregiven
• the sum of the squares on them is rationalgiven
• the rectangle they contain is medialgiven
• the whole is irrationalby X.39
• and it is called majorby X.39

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.39", THEOREM, sample=_kind_sample("major"),
             note="The major line. Its two terms are incommensurable even in "
             "square, which is what puts it beyond the bimedials.")
def prop_X_39(a, b) -> Out:
    hypothesis("the two are incommensurable in square", not commensurable_in_square(a, b))
    hypothesis("the sum of the squares on them is rational", is_rational_area(a * a + b * b))
    hypothesis("the rectangle they contain is medial", is_medial_area(a * b))
    whole = a + b
    claim("the whole is irrational", "X.39", not isinstance(whole, Fraction))
    claim("and it is called major", "X.39", classify(whole).name == "major")
    return Out(major=whole)