Book III · Proposition 7

III.7

If on the diameter of a circle a point be taken which is not the centre of the circle, and from the point straight lines fall upon the circle, that will be greatest on which the centre is, the remainder of the same diameter will be least, and of the rest the nearer to the straight line through the centre is always greater than the more remote, and only two equal straight lines will fall from the point on the circle, one on each side of the least straight line.Heath, 1908

The first of Euclid's two 'nearer is greater' propositions, and the one that needs an interior point.

6 lines and circles drawn, of which 13 helper constructions drew the fainter ones

Every step, checked

the circle has positive radiusgiven
F is not the centregiven
the line on which the centre is, is the greatestby I.20
and the remainder of that diameter is the leastby I.20
of the rest, the nearer to the line through the centre is the greaterby I.24

What it needs, and what needs it

Needs: I.20 I.24

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

Depth: 12 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 (×3)continuity
a line-circle intersection is used, though no postulate asserts that a line meets a circle (×15)continuity

The proposition as code

@proposition(
    "III.7",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 1)
    + (Fraction(rng.randint(1, 3), 4),),
    note="The first of Euclid's two 'nearer is greater' propositions, and the "
    "one that needs an interior point.",
)
def prop_III_7(o: Point, a: Point, part) -> Out:
    """F is on the diameter DA, between the centre and A."""
    hypothesis("the circle has positive radius", o != a)
    hypothesis("F is not the centre", sign(part) > 0)
    circle(o, a, "the given circle")
    far = posit(Point(o.x - (a.x - o.x), o.y - (a.y - o.y)), "D")
    f = posit(Point(o.x + part * (a.x - o.x), o.y + part * (a.y - o.y)), "F")
    line(far, a, "the diameter DA")

    # F lies between O and A, so it is FD that has the centre on it and FA that
    # is the remainder. Points are taken at angles increasing away from A, which
    # is the order "nearer to the line through the centre" puts them in.
    reach = (a.x - o.x, a.y - o.y)
    turned = []
    for step in range(1, 5):
        half = Fraction(step, 4)
        cosine, sine = (1 - half * half) / (1 + half * half), 2 * half / (1 + half * half)
        turned.append(posit(
            Point(o.x + reach[0] * cosine - reach[1] * sine,
                  o.y + reach[0] * sine + reach[1] * cosine),
            f"P{step}",
        ))
    for point in turned:
        line(f, point)

    # Each line from F is the base of a triangle on the radius: I.20 bounds it,
    # and I.24 compares two of them, the wider angle at the centre giving the
    # longer base.
    for point in turned:
        because(prop_I_20, f, o, point)
    for nearer, further in zip(turned, turned[1:]):
        because(prop_I_24, o, f, further, o, f, nearer)

    claim("the line on which the centre is, is the greatest", "I.20",
          all(sign(length(f, far) - length(f, point)) > 0 for point in turned + [a]))
    claim("and the remainder of that diameter is the least", "I.20",
          all(sign(length(f, point) - length(f, a)) > 0 for point in turned + [far]))
    claim("of the rest, the nearer to the line through the centre is the greater",
          "I.24",
          all(sign(length(f, turned[i + 1]) - length(f, turned[i])) > 0
              for i in range(len(turned) - 1)))
    return Out(greatest=far, least=a)