Book I · Proposition 48

I.48

If in a triangle the square on one of the sides be equal to the squares on the remaining two sides of the triangle, the angle contained by the remaining two sides of the triangle is right.Heath, 1908

Every step, checked

• ABC is a genuine trianglegiven
• the square on AC equals those on AB and BCgiven
• erecting a perpendicular at B equal to BA gives, by I.47, a triangle with the same three sides; so by I.8 the angle ABC is rightby I.11, I.47, I.8

What it needs, and what needs it

Needs: I.8 I.11 I.47

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: 15 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 (×12)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×30)continuity

The proposition as code

@proposition(
    "I.48",
    THEOREM,
    sample=samples.right_triangle,
)
def prop_I_48(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("the square on AC equals those on AB and BC",
               len2(a, c) == len2(a, b) + len2(b, c))
    outline(a, b, c)

    # Erect BD at right angles to BC and equal to BA, and join DC. I.47 gives
    # DC the square that AC has, and I.8 then matches the two triangles.
    back_b = Point(2 * b.x - c.x, 2 * b.y - c.y)
    upright = prop_I_11(back_b, c, b).perpendicular
    reach = circle_with_radius2(b, len2(b, a), "circle centre B with radius BA")
    d = posit(meet(upright, reach)[1], "D")
    line(d, c, "join DC")
    because(prop_I_47, d, b, c)
    because(prop_I_8, a, b, c, d, b, c)

    claim("erecting a perpendicular at B equal to BA gives, by I.47, a triangle with the "
          "same three sides; so by I.8 the angle ABC is right", ["I.11", "I.47", "I.8"],
          right_angle(a, b, c))
    return Out()