Book I · Proposition 22

I.22

Out of three straight lines, which are equal to three given straight lines, to construct a triangle: thus it is necessary that two of the straight lines taken together in any manner should be greater than the remaining one.Heath, 1908

The proviso is I.20, and Euclid states it as a necessary condition without proving it sufficient -- another place where continuity is doing silent work.

Every step, checked

• the three given lines satisfy the triangle inequalitygiven
• P and Q are distinctgiven
• PG equals the third given line CAby Def.15
• FG equals the second given line BCby Def.15
• PF equals the first given line ABby Def.15
• so the triangle PFG is built from the three given linesby I.8

What it needs, and what needs it

Needs: I.8

Used by: I.23

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

Depth: 6 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 meetcontinuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity

The proposition as code

@proposition(
    "I.22",
    CONSTRUCTION,
    sample=_three_lengths,
    note="The proviso is I.20, and Euclid states it as a necessary condition without "
    "proving it sufficient -- another place where continuity is doing silent work.",
)
def prop_I_22(
    a: Point,
    b: Point,
    c: Point,
    p: Point,
    q: Point,
    beside: "Point | None" = None,
    apart_from: "Point | None" = None,
) -> Out:
    """Build a triangle on the ray PQ whose sides equal AB, BC and CA.

    The two circles meet on both sides of PQ, and either intersection answers
    the problem.  ``beside`` and ``apart_from`` say which one is wanted -- a
    choice Euclid makes silently by drawing the figure one way round.
    """
    first, second, third = len2(a, b), len2(b, c), len2(c, a)
    hypothesis("the three given lines satisfy the triangle inequality",
               length(a, b) + length(b, c) > length(c, a)
               and length(b, c) + length(c, a) > length(a, b)
               and length(c, a) + length(a, b) > length(b, c))
    hypothesis("P and Q are distinct", p != q)
    outline(a, b, c)  # the three given lines

    ray = line(p, q, "the ray PQ")
    around_p = circle_with_radius2(p, first, "circle radius AB about P")
    foot = posit(meet(ray, around_p)[1], "F")
    around_f = circle_with_radius2(foot, second, "circle radius BC about F")
    closing = circle_with_radius2(p, third, "circle radius CA about P")
    candidates = meet(around_f, closing)
    apex = posit(_choose_side(candidates, Line.through(p, q), beside, apart_from), "G")

    claim("PG equals the third given line CA", "Def.15", eq_len(p, apex, c, a))
    claim("FG equals the second given line BC", "Def.15", eq_len(foot, apex, b, c))
    claim("PF equals the first given line AB", "Def.15", eq_len(p, foot, a, b))
    because(prop_I_8, p, foot, apex, a, b, c)
    claim("so the triangle PFG is built from the three given lines", "I.8",
          congruent_sss((p, foot, apex), (a, b, c)))
    return Out(triangle=(p, foot, apex))