Book III · Proposition 2

III.2

If on the circumference of a circle two points be taken at random, the straight line joining the points will fall within the circle.Heath, 1908

Every step, checked

• A and B lie on the circle and are distinctgiven
• the midpoint of the join lies inside the circleby Def.15
• and so does every point of it strictly between the endsby I.18

What it needs, and what needs it

Needs: I.10 I.18

Used by: III.4

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

Depth: 10 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 (×5)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×7)continuity
• the 'collinear' fact (occurrence 1) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "III.2",
    THEOREM,
    sample=_two_on_a_circle,
)
def prop_III_2(o: Point, a: Point, b: Point) -> Out:
    hypothesis("A and B lie on the circle and are distinct",
               eq_len(o, a, o, b) and a != b)
    around = circle(o, a, "the given circle")
    chord = line(a, b, "the joining line AB")
    middle = posit(prop_I_10(a, b).midpoint, "M")

    # OM is shorter than the radius, which is what I.18 reads off the triangle;
    # a chord through the centre leaves no triangle to read it off.
    if not collinear(o, a, b):
        because(prop_I_18, o, middle, a)

    claim("the midpoint of the join lies inside the circle", "Def.15",
          inside_circle(middle, around))
    claim("and so does every point of it strictly between the ends", "I.18",
          all(inside_circle(Point(a.x + Fraction(k, 8) * (b.x - a.x),
                                  a.y + Fraction(k, 8) * (b.y - a.y)), around)
              for k in range(1, 8)))
    return Out(chord=chord)