Book II · Proposition 12

II.12

In obtuse-angled triangles the square on the side subtending the obtuse angle is greater than the squares on the sides containing the obtuse angle by twice the rectangle contained by one of the sides about the obtuse angle, namely that on which the perpendicular falls, and the straight line cut off outside by the perpendicular towards the obtuse angle.Heath, 1908

The law of cosines, with the sign for an obtuse angle. Euclid has no cosine, so the correction term is a rectangle he can point at.

Every step, checked

• ABC is a genuine trianglegiven
• the angle at B is obtusegiven
• the perpendicular falls outside the triangle, beyond Bgiven
• AD is perpendicular to CDby I.12
• the square on the side subtending the obtuse angle exceeds the squares on the other two by twice the rectangle contained by CB and BDby I.47, II.4

What it needs, and what needs it

Needs: I.12 I.47 II.4

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 (×24)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×55)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "II.12",
    THEOREM,
    sample=samples.obtuse_triangle,
    note="The law of cosines, with the sign for an obtuse angle. Euclid has no "
    "cosine, so the correction term is a rectangle he can point at.",
)
def prop_II_12(a: Point, b: Point, c: Point) -> Out:
    """The obtuse angle is at B; the perpendicular from A falls on CB produced."""
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("the angle at B is obtuse", angle_at(a, b, c) > RIGHT)
    outline(a, b, c)

    d = posit(_foot_of_the_perpendicular(a, c, b), "D")
    line(c, d, "CB produced to D")
    line(a, d, "the perpendicular AD")

    hypothesis("the perpendicular falls outside the triangle, beyond B", between(c, b, d))
    because(prop_I_12, c, b, a)
    because(prop_I_47, a, d, c)
    because(prop_I_47, a, d, b)
    because(prop_II_4, c, b, d)

    claim("AD is perpendicular to CD", "I.12", right_angle(a, d, c))
    # CB and BD run the same way out of B, so the rectangle they contain is the
    # dot product -- exact, and without a square root anywhere.
    rectangle = length(c, b) * length(b, d)
    claim("the square on the side subtending the obtuse angle exceeds the squares on "
          "the other two by twice the rectangle contained by CB and BD",
          ["I.47", "II.4"],
          len2(a, c) == len2(a, b) + len2(c, b) + 2 * rectangle)
    return Out(foot=d)