Book III · Proposition 13

III.13

A circle does not touch a circle at more points than one, whether it touch it internally or externally.Heath, 1908

Every step, checked

• the circles have positive radiigiven
• they touch at Agiven
• the centres are distinctgiven
• no second point of the greater circle lies on the lesserby III.11
• so circles that touch, touch at one point onlyby III.11

What it needs, and what needs it

Needs: III.11

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

Depth: 13 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.13",
    THEOREM,
    sample=lambda rng: _touching_circles(rng, internally=True),
)
def prop_III_13(o: Point, a: Point, p: Point) -> Out:
    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")
    hypothesis("they touch at A", on_circle(a, outer) and on_circle(a, inner))
    hypothesis("the centres are distinct", o != p)
    line(o, p, "the line joining the centres")

    because(prop_III_11, o, a, p)

    claim("no second point of the greater circle lies on the lesser", "III.11",
          not any(on_circle(point, inner) for point in _round(o, a) if point != a))
    claim("so circles that touch, touch at one point only", "III.11",
          len([point for point in _round(o, a) if on_circle(point, inner)]) <= 1)
    return Out(contact=a)