Book VI · Proposition 1

VI.1

Triangles and parallelograms which are under the same height are to one another as their bases.Heath, 1908
ABCDG
14 lines and circles drawn, of which 5 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.38

Used by: VI.14 VI.23

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.

What it takes on trust

The proposition as code

@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))