Book VI · Proposition 31

VI.31

In right-angled triangles the figure on the side subtending the right angle is equal to the similar and similarly described figures on the sides containing the right angle.Heath, 1908

Pythagoras generalised: the figures need not be squares, only similar. Here they are similar triangles, so I.47 is a special case.

ABC
6 lines and circles drawn, of which 32 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.47 VI.4 VI.20

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, Def.5, Post.5, V.Def.5, VI.Def.1

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

What it takes on trust

The proposition as code

@proposition(
    "VI.31",
    THEOREM,
    sample=samples.right_triangle,
    note="Pythagoras generalised: the figures need not be squares, only similar. "
    "Here they are similar triangles, so I.47 is a special case.",
)
def prop_VI_31(a: Point, b: Point, c: Point) -> Out:
    """The right angle is at B; similar triangles are erected on the three sides."""
    hypothesis("the angle ABC is right", right_angle(a, b, c))
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)

    def similar_on(first: Point, second: Point) -> tuple[Point, Point, Point]:
        """Erect on the segment a triangle similar to ABC, on a fixed side."""
        dx, dy = second.x - first.x, second.y - first.y
        # the shape of ABC expressed in the frame of its own hypotenuse
        hx, hy = c.x - a.x, c.y - a.y
        scale = len2(a, c)
        px, py = b.x - a.x, b.y - a.y
        u = (px * hx + py * hy) / scale
        v = (px * hy - py * hx) / scale
        apex = Point(first.x + u * dx - v * dy, first.y + u * dy + v * dx)
        return first, apex, second

    on_hypotenuse = similar_on(a, c)
    on_first = similar_on(a, b)
    on_second = similar_on(b, c)
    for triangle in (on_hypotenuse, on_first, on_second):
        line(triangle[0], triangle[1])
        line(triangle[1], triangle[2])

    claim("the three figures are similar to one another", "VI.4",
          similar(on_first, on_hypotenuse) and similar(on_second, on_hypotenuse))
    claim("similar figures are to one another as the squares on their sides", "VI.20",
          _area(*on_first) * len2(a, c) == _area(*on_hypotenuse) * len2(a, b))
    because(prop_I_47, a, b, c)

    claim("so the figure on the hypotenuse equals the two on the legs", ["I.47", "VI.20"],
          _area(*on_hypotenuse) == _area(*on_first) + _area(*on_second))
    return Out(figures=(on_hypotenuse, on_first, on_second))