Book III · Proposition 15

III.15

Of straight lines in a circle the diameter is greatest, and of the rest the nearer to the centre is always greater than the more remote.Heath, 1908

Every step, checked

• the points lie on the circlegiven
• the chords are genuinegiven
• the diameter is the greatest of themby I.20
• and of the rest, the nearer to the centre is the greaterby I.47

What it needs, and what needs it

Needs: I.10 I.20 I.47

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

The proposition as code

@proposition(
    "III.15",
    THEOREM,
    sample=_three_on_a_circle,
)
def prop_III_15(o: Point, a: Point, b: Point, c: Point) -> Out:
    """AB is a chord; the diameter through A is compared with it."""
    hypothesis("the points lie on the circle", eq_len(o, a, o, b) and eq_len(o, a, o, c))
    hypothesis("the chords are genuine", a != b and a != c, guard=True)
    circle(o, a, "the given circle")
    far = posit(Point(o.x - (a.x - o.x), o.y - (a.y - o.y)), "D")
    line(a, far, "the diameter AD")
    line(a, b, "the chord AB")
    line(a, c, "the chord AC")

    near = posit(prop_I_10(a, b).midpoint, "E")
    remote = posit(prop_I_10(a, c).midpoint, "F")
    # AD is a diameter and AB a chord: the triangle on the centre bounds one
    # against the other by I.20, and I.47 turns the distance from the centre
    # into the length of the chord.
    because(prop_I_20, a, o, b)
    because(prop_I_47, a, near, o)
    because(prop_I_47, a, remote, o)

    claim("the diameter is the greatest of them", "I.20",
          sign(length(a, far) - length(a, b)) >= 0
          and sign(length(a, far) - length(a, c)) >= 0)
    claim("and of the rest, the nearer to the centre is the greater", "I.47",
          (sign(length(o, near) - length(o, remote)) < 0)
          == (sign(length(a, b) - length(a, c)) > 0))
    return Out(diameter=(a, far))