Book X · Proposition 41

X.41

If two straight lines incommensurable in square which make the sum of the squares on them medial, and the rectangle contained by them medial and also incommensurable with the sum of the squares on them, be added together, the whole straight line is irrational; and let it be called the side of the sum of two medial areas.Heath, 1908

Every step, checked

• the two are incommensurable in squaregiven
• the sum of the squares is medialgiven
• the rectangle is medialgiven
• the two areas are incommensurablegiven
• the whole is irrationalby X.41
• and it is the side of the sum of two medial areasby X.41

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.41", THEOREM, sample=_kind_sample("two medials"))
def prop_X_41(a, b) -> Out:
    hypothesis("the two are incommensurable in square", not commensurable_in_square(a, b))
    hypothesis("the sum of the squares is medial", is_medial_area(a * a + b * b))
    hypothesis("the rectangle is medial", is_medial_area(a * b))
    hypothesis("the two areas are incommensurable",
               not commensurable(a * a + b * b, a * b))
    whole = a + b
    claim("the whole is irrational", "X.41", not isinstance(whole, Fraction))
    claim("and it is the side of the sum of two medial areas", "X.41",
          classify(whole).name == "the side of the sum of two medial areas")
    return Out(side=whole)