Book III · Proposition 37

III.37

If a point be taken outside a circle and from the point there fall on the circle two straight lines, if one of them cut the circle, and the other fall on it, and if further 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 be equal to the square on the straight line which falls on the circle, the straight line which falls on it will touch the circle.Heath, 1908

Every step, checked

• the rectangle equals the square on PTby III.36
• so PT touches the circle: the radius to T meets it at right anglesby III.18
• and no point of PT beyond the contact falls inside the circleby III.16

What it needs, and what needs it

Needs: III.16 III.18 III.36

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

The proposition as code

@proposition(
    "III.37",
    THEOREM,
    sample=_secant_and_tangent,
)
def prop_III_37(o: Point, a: Point, beyond, turn) -> Out:
    """The converse of III.36: the rectangle identifies the tangent."""
    result = prop_III_36(o, a, beyond, turn)
    touch = result.tangent
    near, far = result.secant
    outside = posit(Point(o.x + beyond * (a.x - o.x), o.y + beyond * (a.y - o.y)), "P")

    because(prop_III_36, o, a, beyond, turn)
    because(prop_III_18, o, touch, Fraction(1))
    because(prop_III_16, o, touch)

    claim("the rectangle equals the square on PT", "III.36",
          length(outside, near) * length(outside, far) == len2(outside, touch))
    claim("so PT touches the circle: the radius to T meets it at right angles",
          "III.18", right_angle(o, touch, outside))
    claim("and no point of PT beyond the contact falls inside the circle", "III.16",
          not any(inside_circle(
              Point(touch.x + Fraction(k, 4) * (outside.x - touch.x),
                    touch.y + Fraction(k, 4) * (outside.y - touch.y)),
              circle(o, a)) for k in range(1, 5)))
    return Out(tangent=touch)