Book VI · Proposition 1
Triangles and parallelograms which are under the same height are to one another as their bases.Heath, 1908
Needs: I.38
Rests on: C.N.1, C.N.2, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4, Post.5, V.Def.5
Depth: 14 steps of argument above the first principles. Parallel postulate: needed.
@proposition(
"VI.1",
THEOREM,
sample=_cut_base,
)
def prop_VI_1(a: Point, b: Point, c: Point, d: Point) -> Out:
hypothesis("B, C and D lie in a straight line", collinear(b, c, d))
hypothesis("A is off that line", not collinear(a, b, c))
line(a, b)
line(a, c)
line(a, d)
# Euclid lays equal multiples of each base off along the line and compares
# the triangles standing on them, which is where I.38 enters and where
# Definition 5 gets its equimultiples. One step of the laying-off executes
# the appeal: GB is BC carried across B, so AGB and ABC stand on equal bases
# in one straight line and on the one apex A.
beyond = posit(Point(2 * b.x - c.x, 2 * b.y - c.y), "G")
outline(a, beyond, b)
because(prop_I_38, beyond, b, a, b, c, a)
claim("carrying a base across gives an equal triangle on the same apex", "I.38",
_area(a, beyond, b) == _area(a, b, c))
claim("the triangles ABC and ACD are as the bases BC and CD", ["I.38", "V.Def.5"],
_area(a, b, c) * length(c, d) == _area(a, c, d) * length(b, c))
# Euclid's enunciation is "triangles *and parallelograms* which are under
# the same height", and the parallelogram half is what VI.14 and VI.23
# appeal to. Each triangle is half the parallelogram completed on its own
# base under the same height, so the ratio carries over unchanged.
first = _parallelogram_on(b, c, a)
second = _parallelogram_on(c, d, a)
outline(*first)
outline(*second)
claim("and the parallelograms on those bases, under the same height, "
"likewise", ["I.38", "V.Def.5"],
_area(*first) * length(c, d) == _area(*second) * length(b, c))
return Out(triangles=((a, b, c), (a, c, d)),
parallelograms=(first, second))