Book III · Proposition 16

III.16

The straight line drawn at right angles to the diameter of a circle from its extremity will fall outside the circle, and into the space between the straight line and the circumference another straight line cannot be interposed; further the angle of the semicircle is greater, and the remaining angle less, than any acute rectilineal angle.Heath, 1908

The tangent, reached from the other side: the perpendicular at the end of a diameter meets the circle once and lies wholly outside it.

Every step, checked

• the circle has positive radiusgiven
• the perpendicular meets the circle at A and nowhere elseby I.17
• and every other point of it falls outside the circleby I.19

What it needs, and what needs it

Needs: I.17 I.19

Used by: III.17 III.37 IV.3 IV.4 IV.7 IV.8 IV.12 IV.13

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

Depth: 11 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.16",
    THEOREM,
    sample=lambda rng: samples.points_round_a_circle(rng, 1),
    note="The tangent, reached from the other side: the perpendicular at the end "
    "of a diameter meets the circle once and lies wholly outside it.",
)
def prop_III_16(o: Point, a: Point) -> Out:
    hypothesis("the circle has positive radius", o != a)
    around = circle(o, a, "the given circle")
    far = posit(Point(o.x - (a.x - o.x), o.y - (a.y - o.y)), "B")
    line(a, far, "the diameter AB")
    upright = _tangent_at(o, a, "the perpendicular at A")

    steps = [Fraction(k, 4) for k in range(1, 6)]
    across = _across(o, a)
    along = [Point(a.x + step * across[0], a.y + step * across[1]) for step in steps]

    # OAP is right-angled at A, so the angle there is the greatest of the three:
    # I.17 bounds the pair and I.19 turns the angles into the sides.
    for point in along:
        because(prop_I_17, o, a, point)
        because(prop_I_19, o, a, point)

    claim("the perpendicular meets the circle at A and nowhere else", "I.17",
          on_circle(a, around) and not any(on_circle(point, around) for point in along))
    claim("and every other point of it falls outside the circle", "I.19",
          all(not inside_circle(point, around) for point in along))
    return Out(tangent=upright)