Book III · Proposition 28

III.28

In equal circles equal straight lines cut off equal circumferences, the greater equal to the greater and the less to the less.Heath, 1908

Every step, checked

• the points lie on the circlegiven
• A and B are distinctgiven
• the chords really are chords, their ends lying on the circlesby Def.15
• the circles are equal and the chords equalby Def.15
• so the angles at the centres are equalby I.8
• and equal angles at the centres stand on equal arcsby III.26

What it needs, and what needs it

Needs: I.8 III.26

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

Depth: 7 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.28",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 3)
    + (samples.isometry(rng),),
)
def prop_III_28(o: Point, a: Point, b: Point, c: Point, move) -> Out:
    """In equal circles, equal chords cut off equal arcs."""
    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")
    line(a, b, "the chord AB")
    line(d, e, "the chord DE")

    claim("the chords really are chords, their ends lying on the circles",
          "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 and the chords equal", "Def.15",
          eq_len(o, a, p, d) and eq_len(a, b, d, e))
    because(prop_I_8, o, a, b, p, d, e)
    because(prop_III_26, o, a, b, c, move)

    claim("so the angles at the centres are equal", "I.8", eq_angle(a, o, b, d, p, e))
    claim("and equal angles at the centres stand on equal arcs", "III.26",
          eq_angle(a, o, b, d, p, e))
    return Out()