Book I · Proposition 5

I.5

In isosceles triangles the angles at the base are equal to one another, and, if the equal straight lines be produced further, the angles under the base will be equal to one another.Heath, 1908

The pons asinorum. Euclid's proof produces the equal sides and applies I.4 twice.

Every step, checked

• AB = ACgiven
• F lies on AB produced and G on AC produced, with AF equal to AGby I.3
• so FC equals GB, and the angle ACF the angle ABGby I.4
• BF = CG, the remainders of equalsby C.N.3
• so the angles FBC and GCB under the base are equalby I.4
• therefore angle ABC = angle ACB, the angles at the baseby C.N.3

What it needs, and what needs it

Needs: I.3 I.4

Used by: I.7 I.18 I.19 I.20 III.20 XIII.7

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.15, Def.4

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

What it takes on trust

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

The proposition as code

@proposition(
    "I.5",
    THEOREM,
    sample=samples.isosceles,
    note="The pons asinorum. Euclid's proof produces the equal sides and applies I.4 twice.",
)
def prop_I_5(a: Point, b: Point, c: Point) -> Out:
    hypothesis("AB = AC", eq_len(a, b, a, c))

    # Produce the two sides to D and E, take F at random on BD, and cut AG off
    # equal to AF -- which is I.3's own business, so I.3 does it.
    produced = circle_with_radius2(a, len2(a, b) * 3, "circle centre A through D and E")
    d = posit(meet(line(a, b), produced)[1], "D")
    e = posit(meet(line(a, c), produced)[1], "E")
    taken = circle_with_radius2(a, len2(a, b) * 2, "circle centre A through F")
    f = posit(meet(line(a, d), taken)[1], "F")
    # The lesser line is named FA rather than AF: I.3 places it at A by I.2,
    # and I.2 joins the point to an end of the line, so handing it a line that
    # already starts at A asks Postulate 1 for a line to itself.
    g = posit(prop_I_3(a, e, f, a).cut, "G")
    line(f, c)
    line(g, b)

    claim("F lies on AB produced and G on AC produced, with AF equal to AG", "I.3",
          between(a, b, f) and between(a, c, g) and eq_len(a, f, a, g))

    because(prop_I_4, a, f, c, a, g, b)
    claim("so FC equals GB, and the angle ACF the angle ABG", "I.4",
          eq_len(f, c, g, b) and eq_angle(a, c, f, a, b, g))
    claim("BF = CG, the remainders of equals", "C.N.3", eq_len(b, f, c, g))

    because(prop_I_4, f, b, c, g, c, b)
    claim("so the angles FBC and GCB under the base are equal", "I.4",
          eq_angle(f, b, c, g, c, b))
    claim("therefore angle ABC = angle ACB, the angles at the base", "C.N.3",
          eq_angle(a, b, c, a, c, b))
    return Out()