Book III · Proposition 11

III.11

If two circles touch one another internally, and their centres be taken, the straight line joining their centres, if it be also produced, will fall on the point of contact of the circles.Heath, 1908

Every step, checked

• the circles have positive radiigiven
• they touch at Agiven
• the centres are distinctgiven
• the point of contact lies on the line of centres producedby I.20
• and the distance between the centres is the difference of the radiiby C.N.3

What it needs, and what needs it

Needs: I.20

Used by: III.13

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

Depth: 12 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "III.11",
    THEOREM,
    sample=lambda rng: _touching_circles(rng, internally=True),
)
def prop_III_11(o: Point, a: Point, p: Point) -> Out:
    """The circle about O through A, and a smaller one about P touching inside."""
    hypothesis("the circles have positive radii", o != a and o != p)
    outer = circle(o, a, "the greater circle")
    inner = circle(p, a, "the lesser, touching it within")
    hypothesis("they touch at A", on_circle(a, outer) and on_circle(a, inner))
    hypothesis("the centres are distinct", o != p)
    joined = line(o, p, "the line joining the centres")

    claim("the point of contact lies on the line of centres produced", "I.20",
          on_line(a, joined))
    claim("and the distance between the centres is the difference of the radii",
          "C.N.3", length(o, p) == length(o, a) - length(p, a))
    return Out(contact=a)