Book I · Proposition 47

I.47

In right-angled triangles the square on the side subtending the right angle is equal to the squares on the sides containing the right angle.Heath, 1908

Pythagoras. Euclid proves it by cutting the large square into two rectangles, each equal to one of the small squares -- the windmill figure.

Every step, checked

• the angle ABC is rightgiven
• ABC is a genuine trianglegiven
• the squares are described on the three sides, each falling away from the triangleby I.46
• the parallel through B meets AC within it, and the far side beyondby I.31
• each rectangle is double a triangle that is half one of the smaller squares, so the two are equalby I.4, I.41
• therefore the square on AC equals the squares on AB and BC togetherby C.N.2

What it needs, and what needs it

Needs: I.4 I.31 I.41 I.46

Used by: I.48 II.9 II.10 II.11 II.12 II.13 II.14 III.14 III.15 III.35 III.36 IV.12 VI.31 XIII.10 XIII.12

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.22, Def.4, Post.5

Depth: 14 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×10)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×25)continuity
• the argument reads a 'between' fact off the figure (×2)order

The proposition as code

@proposition(
    "I.47",
    THEOREM,
    sample=samples.right_triangle,
    note="Pythagoras. Euclid proves it by cutting the large square into two rectangles, "
    "each equal to one of the small squares -- the windmill figure.",
)
def prop_I_47(a: Point, b: Point, c: Point) -> Out:
    """The right angle is at B."""
    hypothesis("the angle ABC is right", right_angle(a, b, c))
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)

    on_hypotenuse = _square_outward(a, c, b)
    on_first = _square_outward(a, b, c)
    on_second = _square_outward(c, b, a)
    _, _, far_c, far_a = on_hypotenuse

    claim("the squares are described on the three sides, each falling away from "
          "the triangle", "I.46",
          _area(*on_hypotenuse) == len2(a, c)
          and _area(*on_first) == len2(a, b)
          and _area(*on_second) == len2(c, b))

    # Euclid draws the parallel through the right angle to a side of the square
    # on the hypotenuse.  It is the perpendicular to AC, and it cuts that square
    # into the two rectangles the proof is about.
    divider = _parallel_through(b, a, far_a)
    foot = posit(meet_one(divider, Line.through(a, c)), "L")
    across = posit(meet_one(divider, Line.through(far_a, far_c)), "M")
    claim("the parallel through B meets AC within it, and the far side beyond",
          "I.31", between(a, foot, c) and between(far_a, across, far_c))

    halves = []
    for near, far, corner, square in ((a, c, far_a, on_first),
                                      (c, a, far_c, on_second)):
        outer, inner = square[3], square[2]
        # The two triangles of the windmill: one on a side of the square on the
        # hypotenuse, one on a side of the smaller square.
        because(prop_I_4, near, b, corner, near, outer, far)
        # Each is half of its own figure, being on the same base and between the
        # same parallels.
        because(prop_I_41, near, corner, across, foot, b)
        because(prop_I_41, outer, near, b, inner, far)
        halves.append(_area(near, corner, across, foot))

    claim("each rectangle is double a triangle that is half one of the smaller "
          "squares, so the two are equal", ["I.4", "I.41"],
          halves[0] == _area(*on_first) and halves[1] == _area(*on_second))
    claim("therefore the square on AC equals the squares on AB and BC together", "C.N.2",
          _area(*on_hypotenuse) == halves[0] + halves[1])
    return Out(squares=(on_hypotenuse, on_first, on_second),
               rectangles=(halves[0], halves[1]), foot=foot)