Book III · Proposition 4

III.4

If in a circle two straight lines cut one another which are not through the centre, they do not bisect one another.Heath, 1908

Every step, checked

• the four points lie on one circlegiven
• neither chord passes through the centregiven
• the chords are not parallelgiven
• all four ends lie on the circle, so both lines are chords of itby Def.15
• the crossing falls inside the circleby III.2
• were E to bisect both, the lines from the centre would be perpendicular to each and the centre would lie on bothby III.3

What it needs, and what needs it

Needs: III.2 III.3

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

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

The proposition as code

@proposition(
    "III.4",
    THEOREM,
    sample=_four_on_a_circle,
)
def prop_III_4(o: Point, a: Point, b: Point, c: Point, d: Point) -> Out:
    """AC and BD are chords, neither through the centre, crossing inside."""
    hypothesis("the four points lie on one circle",
               all(eq_len(o, p, o, a) for p in (b, c, d)))
    hypothesis("neither chord passes through the centre",
               not on_line(o, Line.through(a, c)) and not on_line(o, Line.through(b, d)))
    circle(o, a, "the given circle")
    first, second = line(a, c, "AC"), line(b, d, "BD")
    hypothesis("the chords are not parallel", not parallel(first, second))
    crossing = posit(meet_one(first, second), "E")

    because(prop_III_2, o, a, c)
    because(prop_III_3, o, a, b, c)

    claim("all four ends lie on the circle, so both lines are chords of it",
          "Def.15",
          all(on_circle(point, circle(o, a)) for point in (a, b, c, d)))
    claim("the crossing falls inside the circle", "III.2", inside_circle(crossing, circle(o, a)))
    claim("were E to bisect both, the lines from the centre would be "
          "perpendicular to each and the centre would lie on both", "III.3",
          not (eq_len(a, crossing, crossing, c) and eq_len(b, crossing, crossing, d)))
    return Out(crossing=crossing)