Book VI · Proposition 2

VI.2

If a straight line be drawn parallel to one of the sides of a triangle, it will cut the sides of the triangle proportionally; and, if the sides of the triangle be cut proportionally, the line joining the points of section will be parallel to the remaining side of the triangle.Heath, 1908

The intercept theorem, and the workhorse of the rest of Book VI.

Every step, checked

• D lies on AB and E on ACgiven
• DE is parallel to BCgiven
• the triangles BDE and CDE are equal, being on the same base and in the same parallelsby I.38
• so AD is to DB as AE is to ECby I.38, V.Def.5

What it needs, and what needs it

Needs: I.37 I.38

Used by: VI.3 VI.4 VI.9 VI.10 VI.11 VI.12

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

• 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(
    "VI.2",
    THEOREM,
    sample=_triangle_with_parallel,
    note="The intercept theorem, and the workhorse of the rest of Book VI.",
)
def prop_VI_2(a: Point, b: Point, c: Point, d: Point, e: Point) -> Out:
    hypothesis("D lies on AB and E on AC",
               on_line(d, Line.through(a, b)) and on_line(e, Line.through(a, c)))
    hypothesis("DE is parallel to BC", parallel(Line.through(d, e), Line.through(b, c)))
    outline(a, b, c)
    line(d, e, "DE")
    because(prop_I_37, d, e, b, c)
    # The same base is the limiting case of equal bases, which is the case I.38
    # is stated for and the one Euclid cites here. I.38 names the parallel by
    # drawing it through the apex, so an apex sitting on DE leaves it nothing to
    # draw -- which happens when this proposition is reached from VI.11 with the
    # section falling on B.
    if not on_line(b, Line.through(d, e)) and not on_line(c, Line.through(d, e)):
        because(prop_I_38, d, e, b, d, e, c)

    claim("the triangles BDE and CDE are equal, being on the same base and in the "
          "same parallels", "I.38", _area(b, d, e) == _area(c, d, e))
    claim("so AD is to DB as AE is to EC", ["I.38", "V.Def.5"],
          length(a, d) * length(e, c) == length(d, b) * length(a, e))
    return Out()