Book III · Proposition 10

III.10

A circle does not cut a circle at more points than two.Heath, 1908
OABC
13 lines and circles drawn, of which 8 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: III.9

Used by: III.23

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

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

What it takes on trust

The proposition as code

@proposition(
    "III.10",
    THEOREM,
    sample=_three_on_a_circle,
)
def prop_III_10(o: Point, a: Point, b: Point, c: Point) -> Out:
    """Three points cannot lie on two different circles."""
    hypothesis("A, B and C are three distinct points of a circle",
               eq_len(o, a, o, b) and eq_len(o, a, o, c) and not collinear(a, b, c))
    circle(o, a, "the given circle")
    outline(a, b, c)

    # Any circle through all three has the centre found from them, and so has
    # this centre and this radius: it *is* this circle. Two distinct circles
    # therefore cannot share three points, and cutting in three is impossible.
    because(prop_III_9, o, a, b, c)

    claim("three points of a circle determine its centre", "III.9",
          _centre_of(a, b, c) == o)
    claim("and with the centre the radius, so any circle through all three is "
          "this same circle", "Def.15",
          eq_len(_centre_of(a, b, c), a, o, a))
    claim("so two circles sharing three points coincide everywhere", "Def.15",
          all(on_circle(point, circle(_centre_of(a, b, c), a)) for point in _round(o, a)))
    return Out()