Book II · Proposition 13

II.13

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

The source used here misprints this enunciation — it reads “acutc angle” where Heath has “acute angle” ('acutc' scanned for 'acute'). The full errata →

The other sign of the law of cosines. Heath's enunciation is not shown here: the only copy of it available to this project scans 'acute' as 'acutc', and it is dropped rather than mended.

Every step, checked

• ABC is a genuine trianglegiven
• the angle at B is acutegiven
• the perpendicular falls within CBgiven
• AD is perpendicular to CBby I.12
• the square on the side subtending the acute angle falls short of the squares on the other two by twice the rectangle contained by CB and BDby I.47, II.7

What it needs, and what needs it

Needs: I.12 I.47 II.7

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.13",
    THEOREM,
    sample=samples.acute_triangle,
    note="The other sign of the law of cosines. Heath's enunciation is not shown "
    "here: the only copy of it available to this project scans 'acute' as "
    "'acutc', and it is dropped rather than mended.",
)
def prop_II_13(a: Point, b: Point, c: Point) -> Out:
    """The angle at B is acute; the perpendicular from A falls inside CB."""
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("the angle at B is acute", angle_at(a, b, c) < RIGHT)
    outline(a, b, c)

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

    hypothesis("the perpendicular falls within CB", between(c, d, b))
    because(prop_I_12, c, b, a)
    because(prop_I_47, a, d, c)
    because(prop_I_47, a, d, b)
    because(prop_II_7, c, d, b)

    claim("AD is perpendicular to CB", "I.12", right_angle(a, d, c))
    rectangle = length(c, b) * length(b, d)
    claim("the square on the side subtending the acute angle falls short of the "
          "squares on the other two by twice the rectangle contained by CB and BD",
          ["I.47", "II.7"],
          len2(a, c) + 2 * rectangle == len2(a, b) + len2(c, b))
    return Out(foot=d)