Book III · Proposition 26

III.26

In equal circles equal angles stand on equal circumferences, whether they stand at the centres or at the circumferences.Heath, 1908

Every step, checked

• the points lie on the circlegiven
• A and B are distinctgiven
• every point named lies on the circle it belongs toby Def.15
• the circles are equalby Def.15
• the angles at the centres are equalby I.8
• so the arcs they stand on are equal, their chords being equalby I.4

What it needs, and what needs it

Needs: I.4 I.8

Used by: III.28 VI.33

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

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

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "III.26",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 3)
    + (samples.isometry(rng),),
)
def prop_III_26(o: Point, a: Point, b: Point, c: Point, move) -> Out:
    """Equal circles, and equal angles standing at their centres."""
    hypothesis("the points lie on the circle",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("A and B are distinct", a != b)
    first = circle(o, a, "the first circle")
    p, d, e = posit(move(o), "P"), posit(move(a), "D"), posit(move(b), "E")
    second = circle(p, d, "the second, equal to it")
    for pair in ((o, a), (o, b), (p, d), (p, e)):
        line(*pair, "a radius")

    claim("every point named lies on the circle it belongs to", "Def.15",
          on_circle(a, first) and on_circle(b, first)
          and on_circle(d, second) and on_circle(e, second))
    claim("the circles are equal", "Def.15", eq_len(o, a, p, d))
    because(prop_I_8, o, a, b, p, d, e)
    because(prop_I_4, o, a, b, p, d, e)

    claim("the angles at the centres are equal", "I.8", eq_angle(a, o, b, d, p, e))
    claim("so the arcs they stand on are equal, their chords being equal", "I.4",
          eq_len(a, b, d, e))
    return Out()