Book XIII · Proposition 7

XIII.7

If three angles of an equilateral pentagon, taken either in order or not in order, be equal, the pentagon will be equiangular.Heath, 1908

Searching the equilateral pentagons numerically turns up none with three equal angles and a fourth unequal, save those with a vanishing angle, where two vertices have run together and no pentagon is left. Euclid's word for the figure rules those out; the guard below says so.

Every step, checked

• the pentagon is equilateralgiven
• no angle of it has vanishedgiven
• three of its angles are equal, taken in order or notgiven
• the lines subtending the equal angles are equal, the sides containing them being equalby I.4
• so the triangles standing on them are isosceles and their base angles equalby I.5
• therefore the pentagon is equiangularby I.5, C.N.2

What it needs, and what needs it

Needs: I.4 I.5

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

Depth: 4 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 proposition as code

@proposition(
    "XIII.7",
    THEOREM,
    sample=_equilateral_pentagon,
    note="Searching the equilateral pentagons numerically turns up none with "
    "three equal angles and a fourth unequal, save those with a vanishing "
    "angle, where two vertices have run together and no pentagon is left. "
    "Euclid's word for the figure rules those out; the guard below says so.",
)
def prop_XIII_7(a: Point, b: Point, c: Point, d: Point, e: Point) -> Out:
    corners = (a, b, c, d, e)
    angles = [angle_at(corners[i - 1], corners[i], corners[(i + 1) % 5])
              for i in range(5)]
    hypothesis("the pentagon is equilateral", all(
        eq_len(corners[i], corners[(i + 1) % 5], a, b) for i in range(5)))
    hypothesis("no angle of it has vanished", all(
        not collinear(corners[i - 1], corners[i], corners[(i + 1) % 5])
        for i in range(5)), guard=True)
    hypothesis("three of its angles are equal, taken in order or not",
               max(sum(1 for other in angles if other == one)
                   for one in angles) >= 3)
    outline(*corners)

    # The equal sides here are the pentagon's own, so the isosceles triangles
    # stand on its vertices: ABC has BA = BC, and I.4 compares it with BCD,
    # which has the equal included angle. Both appeals were written on AB = AC,
    # a length no pentagon has, and neither ever ran.
    because(prop_I_5, b, a, c)
    because(prop_I_4, b, a, c, c, b, d)

    claim("the lines subtending the equal angles are equal, the sides "
          "containing them being equal", "I.4",
          eq_len(b, e, a, c) and eq_len(a, c, b, d))
    claim("so the triangles standing on them are isosceles and their base "
          "angles equal", "I.5",
          eq_angle(b, e, d, b, d, e) and eq_angle(a, c, d, a, d, c))
    claim("therefore the pentagon is equiangular", ["I.5", "C.N.2"],
          all(angle == angles[0] for angle in angles))
    return Out(pentagon=corners, angles=tuple(angles))