Book III · Proposition 14

III.14

In a circle equal straight lines are equally distant from the centre, and those which are equally distant from the centre are equal to one another.Heath, 1908

Equal chords keep their distance from the centre, and the converse. Both halves follow from the right-angled triangle on half the chord.

Every step, checked

• the four points lie on the circlegiven
• the chords are genuinegiven
• neither chord passes through the centregiven
• the line from the centre to the midpoint is perpendicular to the chordby III.3
• the square on the radius is the square on the half-chord together with the square on the distanceby I.47
• so equal chords are equally distant, and equidistant chords are equalby I.47

What it needs, and what needs it

Needs: I.10 I.47 III.3

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×32)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×62)continuity
• the 'eq_len' fact (occurrence 4) is true in some configurations and false in otherscase
• the 'eq_len' fact (occurrence 5) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.14",
    THEOREM,
    sample=_four_on_a_circle,
    note="Equal chords keep their distance from the centre, and the converse. "
    "Both halves follow from the right-angled triangle on half the chord.",
)
def prop_III_14(o: Point, a: Point, b: Point, c: Point, d: Point) -> Out:
    """AB and CD are two chords of the circle about O."""
    hypothesis("the four points lie on the circle",
               all(eq_len(o, p, o, a) for p in (b, c, d)))
    hypothesis("the chords are genuine", a != b and c != d, guard=True)
    # A chord through the centre is bisected by it, so the perpendicular Euclid
    # drops from the centre has no length and there is no line OE to draw. He
    # states no such proviso and his figure shows neither chord as a diameter.
    # The theorem survives the case -- a diameter is distance zero from the
    # centre, and all diameters are equal -- but this proof does not.
    hypothesis("neither chord passes through the centre",
               not collinear(a, o, b) and not collinear(c, o, d))
    circle(o, a, "the given circle")
    line(a, b, "the chord AB")
    line(c, d, "the chord CD")

    first = posit(prop_I_10(a, b).midpoint, "E")
    second = posit(prop_I_10(c, d).midpoint, "F")
    line(o, first)
    line(o, second)

    because(prop_III_3, o, a, b, c)
    because(prop_I_47, o, first, a)
    because(prop_I_47, o, second, c)

    claim("the line from the centre to the midpoint is perpendicular to the chord",
          "III.3", right_angle(o, first, a) and right_angle(o, second, c))
    claim("the square on the radius is the square on the half-chord together with "
          "the square on the distance", "I.47",
          len2(o, a) == len2(a, first) + len2(o, first))
    claim("so equal chords are equally distant, and equidistant chords are equal",
          "I.47", eq_len(a, b, c, d) == eq_len(o, first, o, second))
    return Out(distances=(first, second))