Book III · Proposition 36

III.36

If a point be taken outside a circle and from it there fall on the circle two straight lines, and if one of them cut the circle and the other touch it, the rectangle contained by the whole of the straight line which cuts the circle and the straight line intercepted on it outside between the point and the convex circumference will be equal to the square on the tangent.Heath, 1908

The power of a point, outside: the tangent is the mean proportional between the whole secant and the part outside.

Every step, checked

• the circle has positive radiusgiven
• the point is outside the circlegiven
• the secant really cuts the circlegiven
• the tangent touches the circle at right angles to the radiusby III.18
• the rectangle contained by the whole secant and the part outside equals the square on the tangentby II.6, I.47

What it needs, and what needs it

Needs: I.10 I.47 II.6 III.18

Used by: III.37

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

The proposition as code

@proposition(
    "III.36",
    THEOREM,
    sample=_secant_and_tangent,
    note="The power of a point, outside: the tangent is the mean proportional "
    "between the whole secant and the part outside.",
)
def prop_III_36(o: Point, a: Point, beyond, turn) -> Out:
    hypothesis("the circle has positive radius", o != a)
    hypothesis("the point is outside the circle", sign(beyond - 1) > 0)
    around = circle(o, a, "the given circle")
    outside = posit(Point(o.x + beyond * (a.x - o.x), o.y + beyond * (a.y - o.y)), "P")

    middle = posit(prop_I_10(o, outside).midpoint, "M")
    helper = circle_with_radius2(middle, len2(middle, o), "the circle on OP")
    touch = posit(meet(helper, around)[0], "T")
    line(outside, touch, "the tangent PT")

    # A secant through P, taken at a rational slant so both crossings are exact.
    slant = Line.through(outside, posit(_turn(o, a, angle_at(a, o, Point(
        o.x + (a.x - o.x) * (1 - turn * turn) / (1 + turn * turn)
        - (a.y - o.y) * 2 * turn / (1 + turn * turn),
        o.y + (a.x - o.x) * 2 * turn / (1 + turn * turn)
        + (a.y - o.y) * (1 - turn * turn) / (1 + turn * turn)))), "Q"))
    crossings = meet(slant, around)
    hypothesis("the secant really cuts the circle", len(crossings) == 2)
    near = posit(min(crossings, key=lambda p: to_float(len2(outside, p))), "C")
    far = posit(max(crossings, key=lambda p: to_float(len2(outside, p))), "D")
    line(outside, far, "the secant PD")

    # CD is the chord, bisected by the perpendicular from the centre and
    # produced to P, which is II.6's configuration; PTO is right-angled at T.
    because(prop_III_18, o, touch, Fraction(1))
    because(prop_II_6, far, near, outside)
    because(prop_I_47, outside, touch, o)

    claim("the tangent touches the circle at right angles to the radius", "III.18",
          on_circle(touch, around) and right_angle(o, touch, outside))
    claim("the rectangle contained by the whole secant and the part outside "
          "equals the square on the tangent", ["II.6", "I.47"],
          length(outside, near) * length(outside, far) == len2(outside, touch))
    return Out(tangent=touch, secant=(near, far))