Book III · Proposition 3

III.3

If in a circle a straight line through the centre bisect a straight line not through the centre, it also cuts it at right angles; and if it cut it at right angles, it also bisects it.Heath, 1908

Every step, checked

• A, B and C lie on the circle centred at Ogiven
• the chord AC does not pass through the centregiven
• OA and OC are equal, being radiiby Def.15
• the triangles OAM and OCM have three sides equalby I.8
• so the adjacent angles at M are equal, and each is rightby Def.10

What it needs, and what needs it

Needs: I.8 I.10

Used by: III.4 III.14

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 (×4)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity

The proposition as code

@proposition(
    "III.3",
    THEOREM,
    sample=_points_on_a_circle,
)
def prop_III_3(o: Point, a: Point, b: Point, c: Point) -> Out:
    hypothesis("A, B and C lie on the circle centred at O",
               eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("the chord AC does not pass through the centre", not collinear(o, a, c))
    circle(o, a, "the given circle")
    line(a, c, "the chord AC")
    middle = posit(prop_I_10(a, c).midpoint, "M")
    line(o, middle, "the line from the centre to the midpoint")

    because(prop_I_8, o, a, middle, o, c, middle)

    claim("OA and OC are equal, being radii", "Def.15", eq_len(o, a, o, c))
    claim("the triangles OAM and OCM have three sides equal", "I.8",
          eq_len(a, middle, middle, c))
    claim("so the adjacent angles at M are equal, and each is right", "Def.10",
          right_angle(o, middle, a) and right_angle(o, middle, c))
    return Out(foot=middle)