Book VI · Proposition 33

VI.33

In equal circles angles have the same ratio as the circumferences on which they stand, whether they stand at the centres or at the circumferences.Heath, 1908

Angles are as the arcs they stand on -- the proportionality that lets an angle be measured by an arc at all.

OABCPDE
6 lines and circles drawn, of which 2 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: III.20 III.26

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

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

What it takes on trust

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

The proposition as code

@proposition(
    "VI.33",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 3) + (samples.isometry(rng),),
    note="Angles are as the arcs they stand on -- the proportionality that lets "
    "an angle be measured by an arc at all.",
)
def prop_VI_33(o: Point, a: Point, b: Point, c: Point, move) -> Out:
    """Equal circles, and angles at their centres."""
    hypothesis("the points lie on the circle",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("the points are distinct", a != b and b != c)
    circle_with_radius2(o, len2(o, a), "the first circle")
    p, d, e = posit(move(o), "P"), posit(move(a), "D"), posit(move(b), "E")
    circle_with_radius2(p, len2(p, d), "the second, equal to it")
    for pair in ((o, a), (o, b), (p, d), (p, e)):
        line(*pair, "a radius")

    claim("the circles are equal", "Def.15", eq_len(o, a, p, d))
    because(prop_III_26, o, a, b, c, move)
    if not collinear(a, c, b) and angle_at(a, o, b) == angle_at(a, c, b).doubled():
        because(prop_III_20, o, a, c, b)

    claim("equal angles at the centres stand on equal arcs, so angle is as arc",
          "III.26", eq_angle(a, o, b, d, p, e) == eq_len(a, b, d, e))
    claim("and the angle at the circumference is half that at the centre, so the "
          "same proportion holds there", "III.20",
          angle_at(a, o, b) == angle_at(a, c, b).doubled()
          or angle_at(a, o, b) == STRAIGHT + STRAIGHT - angle_at(a, c, b).doubled())
    return Out()