Book I · Proposition 21

I.21

If on one of the sides of a triangle, from its extremities, there be constructed two straight lines meeting within the triangle, the straight lines so constructed will be less than the remaining two sides of the triangle, but will contain a greater angle.Heath, 1908

Every step, checked

• D lies inside the triangle ABCgiven
• BD together with DA is less than BC together with CAby I.20
• but the angle BDA is greater than the angle BCAby I.16

What it needs, and what needs it

Needs: I.16 I.20

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

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×4)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×10)continuity
• the argument reads a 'same_side' fact off the figure (×3)order

The proposition as code

@proposition(
    "I.21",
    THEOREM,
    sample=samples.triangle_with_interior_point,
)
def prop_I_21(a: Point, b: Point, c: Point, d: Point) -> Out:
    base = Line.through(a, b)
    hypothesis("D lies inside the triangle ABC",
               same_side(d, c, base)
               and same_side(d, a, Line.through(b, c))
               and same_side(d, b, Line.through(a, c)))
    outline(a, b, c)
    line(a, d)
    line(b, d)

    # BD is produced to meet AC at E, which is the point Euclid's two uses of
    # I.20 are about, and DE produced to A makes BDA exterior to BDE.
    crossing = meet_one(Line.through(b, d), Line.through(a, c))
    line(b, crossing, "BD produced to E")
    because(prop_I_20, a, b, crossing)
    because(prop_I_20, c, crossing, d)
    because(prop_I_16, c, crossing, d)

    claim("BD together with DA is less than BC together with CA", "I.20",
          length(b, d) + length(d, a) < length(b, c) + length(c, a))
    claim("but the angle BDA is greater than the angle BCA", "I.16",
          angle_at(b, d, a) > angle_at(b, c, a))
    return Out()