Book III · Proposition 10
A circle does not cut a circle at more points than two.Heath, 1908
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.
@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()