Book III · Proposition 9

III.9

If a point be taken within a circle, and more than two equal straight lines fall from the point on the circle, the point taken is the centre of the circle.Heath, 1908

The converse of the definition of a circle, and the reason III.1 can speak of *the* centre.

Every step, checked

• three distinct points of the circle are equally distant from Ogiven
• the point equally distant from three points of a circle is uniqueby I.10, I.11
• and it is the centreby Def.15

What it needs, and what needs it

Needs: I.10 I.11

Used by: III.10

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×10)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×12)continuity

The proposition as code

@proposition(
    "III.9",
    THEOREM,
    sample=_three_on_a_circle,
    note="The converse of the definition of a circle, and the reason III.1 can "
    "speak of *the* centre.",
)
def prop_III_9(o: Point, a: Point, b: Point, c: Point) -> Out:
    """From the point O fall three equal lines on the circle."""
    hypothesis("three distinct points of the circle are equally distant from O",
               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)
    for point in (a, b, c):
        line(o, point)

    because(prop_I_10, a, b)
    because(prop_I_11, a, b, prop_I_10(a, b).midpoint)

    claim("the point equally distant from three points of a circle is unique",
          ["I.10", "I.11"], _centre_of(a, b, c) == o)
    claim("and it is the centre", "Def.15", eq_len(o, a, o, b) and eq_len(o, b, o, c))
    return Out(centre=o)