Book III · Proposition 35

III.35

If in a circle two straight lines cut one another, the rectangle contained by the segments of the one is equal to the rectangle contained by the segments of the other.Heath, 1908

The power of a point, inside. The product is the same for every chord through the point, which is what makes it a property of the point.

Every step, checked

• the four points lie on the circlegiven
• the chords are not parallelgiven
• they cut one another within the circlegiven
• the rectangle contained by the segments of one chord equals that contained by the segments of the otherby II.5, III.31
• and both equal the square on the radius less the square on OEby I.47

What it needs, and what needs it

Needs: I.10 I.47 II.5 III.31

Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.17, 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 (×36)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×66)continuity
• the argument reads a 'between' fact off the figure (×2)order

The proposition as code

@proposition(
    "III.35",
    THEOREM,
    sample=_four_on_a_circle,
    note="The power of a point, inside. The product is the same for every chord "
    "through the point, which is what makes it a property of the point.",
)
def prop_III_35(o: Point, a: Point, b: Point, c: Point, d: Point) -> Out:
    """The chords AC and BD cut one another inside the circle at E."""
    hypothesis("the four points lie on the circle",
               all(eq_len(o, p, o, a) for p in (b, c, d)))
    circle(o, a, "the given circle")
    first, second = line(a, c, "the chord AC"), line(b, d, "the chord BD")
    hypothesis("the chords are not parallel", not parallel(first, second))
    crossing = posit(meet_one(first, second), "E")
    hypothesis("they cut one another within the circle",
               between(a, crossing, c) and between(b, crossing, d))

    # Each chord is bisected by the perpendicular from the centre, so II.5
    # applies to it; and the angle on the diameter is right, which is III.31.
    first_mid = prop_I_10(a, c).midpoint
    second_mid = prop_I_10(b, d).midpoint
    because(prop_II_5, a, crossing, c)
    because(prop_II_5, b, crossing, d)
    because(prop_I_47, a, first_mid, o)
    because(prop_I_47, b, second_mid, o)
    opposite = posit(Point(2 * o.x - a.x, 2 * o.y - a.y), "A'")
    if not collinear(a, c, opposite):
        because(prop_III_31, o, a, opposite, c)

    claim("the rectangle contained by the segments of one chord equals that "
          "contained by the segments of the other", ["II.5", "III.31"],
          length(a, crossing) * length(crossing, c)
          == length(b, crossing) * length(crossing, d))
    claim("and both equal the square on the radius less the square on OE", "I.47",
          length(a, crossing) * length(crossing, c) == len2(o, a) - len2(o, crossing))
    return Out(crossing=crossing)