Book VI · Proposition 32
If two triangles having two sides proportional to two sides be placed together at one angle so that their corresponding sides are also parallel, the remaining sides of the triangles will be in a straight line.Heath, 1908
Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4, Post.5
Depth: 11 steps of argument above the first principles. Parallel postulate: needed.
Nothing. It draws no intersections and reads nothing off the picture.
@proposition(
"VI.32",
THEOREM,
sample=_parallelogram_with_similar_corner,
)
def prop_VI_32(a: Point, b: Point, d: Point, part) -> Out:
"""Two similar triangles set together at a corner, with sides parallel."""
hypothesis("the figure is genuine", not collinear(a, b, d), guard=True)
hypothesis("the division is a proper one", sign(part) > 0 and sign(1 - part) > 0, guard=True)
# Two triangles sharing the vertex A, the second the first scaled about it,
# so corresponding sides are parallel and the outer sides fall in a line.
e = posit(Point(a.x + (b.x - a.x) + (d.x - a.x), a.y + (b.y - a.y) + (d.y - a.y)), "E")
far = posit(Point(a.x - part * (b.x - a.x), a.y - part * (b.y - a.y)), "F")
outline(b, a, d)
outline(d, e, close=False)
line(far, b, "the side FB")
# I.33 reads its alternate angles off one diagonal, and which pair those
# are depends on the way round the two equal sides were named: AB with ED,
# taken in that order, is the pair whose joins this figure makes.
because(prop_I_33, a, b, e, d)
# FA and AB stand on opposite sides of A and make two right angles together,
# which is I.14's condition for their being one straight line.
because(prop_I_14, far, a, b, d)
claim("the corresponding sides are parallel", "I.33",
parallel(Line.through(a, b), Line.through(d, e)))
claim("so the remaining sides fall in one straight line", "I.14",
collinear(far, a, b))
return Out()