Book III · Proposition 20

III.20

In a circle the angle at the centre is double of the angle at the circumference, when the angles have the same circumference as base.Heath, 1908

Every step, checked

• A, B and C lie on the circle centred at Ogiven
• the three points are distinctgiven
• ABC is a genuine trianglegiven
• the radii make isosceles triangles, whose exterior angles are double the base anglesby I.5, I.32

What it needs, and what needs it

Needs: I.5 I.32

Used by: III.21 III.27 III.31 III.34 IV.2 VI.33

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

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

The proposition as code

@proposition(
    "III.20",
    THEOREM,
    sample=_points_on_a_circle,
)
def prop_III_20(o: Point, a: Point, b: Point, c: Point) -> Out:
    hypothesis("A, B and C lie on the circle centred at O",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("the three points are distinct", a != b and b != c and a != c)
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    circle(o, a, "the circle")
    outline(a, b, c)
    line(o, a, "a radius")
    line(o, c, "a radius")

    at_centre = angle_at(a, o, c)
    at_circumference = angle_at(a, b, c)
    # OAB and OBC are isosceles on the radii, and the exterior angle of each is
    # the sum of the two interior and opposite: I.5 and I.32 between them.
    if not collinear(o, a, b):
        because(prop_I_5, o, a, b)
        because(prop_I_32, o, a, b)
    if not collinear(o, b, c):
        because(prop_I_5, o, b, c)
        because(prop_I_32, o, b, c)

    # Euclid's angle at the centre stands on the same arc as the angle at the
    # circumference, and when B is on the lesser arc that is the reflex angle --
    # the case Heath draws as the third figure. ``angle_at`` returns the angle
    # itself, never the reflex, so which of the two is meant has to be settled
    # here: B and O fall on the same side of AC exactly when it is the plain one.
    doubled = at_circumference + at_circumference
    standing_on_the_greater_arc = same_side(o, b, Line.through(a, c))
    claim("the radii make isosceles triangles, whose exterior angles are double the "
          "base angles", ["I.5", "I.32"],
          doubled == (at_centre if standing_on_the_greater_arc
                      else STRAIGHT + STRAIGHT - at_centre))
    return Out(centre_angle=at_centre, circumference_angle=at_circumference)