Book XI · Proposition 22
If there be three plane angles of which two, taken together in any manner, are greater than the remaining one, and they are contained by equal straight lines, it is possible to construct a triangle out of the straight lines joining the extremities of the equal straight lines.Heath, 1908
Needs: I.4
Rests on: C.N.4, Def.4
Depth: 1 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@proposition("XI.22", THEOREM, sample=samples3.tetrahedron)
def prop_XI_22(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
"""Three plane angles, any two exceeding the third, on equal arms: the joins
make a triangle."""
hypothesis("the arms are not in one plane", not coplanar(o, a, b, c))
# Euclid's figure has the containing lines equal, so the arms are cut to one
# length. The cut is I.3's move carried into space, and the length is
# squared throughout so no root is taken to make it.
reach = len2(o, a)
arms = []
for point, name in ((a, "A"), (b, "B"), (c, "C")):
scale = reach / len2(o, point)
step = vector_between(o, point)
# The equal arm is along the same ray; its square is ``reach`` by
# construction, and comparing squares is comparing lengths.
arms.append(posit3(Point3(o.x + step[0] * scale, o.y + step[1] * scale,
o.z + step[2] * scale), name + "'"))
for arm in arms:
line3(o, arm)
joins = [line3(arms[i], arms[j], "a join") for i, j in ((0, 1), (1, 2), (0, 2))]
angles = (angle_at3(a, o, b), angle_at3(b, o, c), angle_at3(a, o, c))
hypothesis("any two of the plane angles exceed the third",
all(_sum_exceeds(x, y, z) for x, y, z in
((angles[0], angles[1], angles[2]),
(angles[1], angles[2], angles[0]),
(angles[0], angles[2], angles[1]))))
sides = [len2(arms[0], arms[1]), len2(arms[1], arms[2]), len2(arms[0], arms[2])]
claim("the joins are the bases of the three triangles on equal arms", "I.4",
len(joins) == 3 and all(sign(side) > 0 for side in sides))
# A triangle can be made of three lengths when each falls short of the other
# two together. Squared lengths compare by squaring the inequality, which
# stays exact: (p + q)^2 > r^2 with all positive is p^2 + q^2 + 2pq > r^2.
claim("and a triangle can be made of the three joins", "XI.22",
all(_triangle_from(sides[i], sides[j], sides[k])
for i, j, k in ((0, 1, 2), (1, 2, 0), (0, 2, 1))))
return Out(arms=tuple(arms), joins=tuple(joins))