Book VI · Proposition 4

VI.4

In equiangular triangles the sides about the equal angles are proportional, and those are corresponding sides which subtend the equal angles.Heath, 1908

Every step, checked

• the triangles are equiangulargiven
• the sides about the equal angles are proportionalby VI.2, I.32
• in particular AB is to BC as DE is to EFby VI.2

What it needs, and what needs it

Needs: I.23 I.32 VI.2

Used by: VI.6 VI.8 VI.20 VI.31

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: 15 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 meet (×2)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×2)continuity

The proposition as code

@proposition(
    "VI.4",
    THEOREM,
    sample=_equiangular_triangles,
)
def prop_VI_4(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("the triangles are equiangular",
               eq_angle(a, b, c, d, e, f) and eq_angle(b, c, a, e, f, d))
    outline(a, b, c)
    outline(d, e, f)
    because(prop_I_32, a, b, c)
    # Euclid sets DEF down again with E on C and EF running on beyond, so that
    # BC and CF' lie in one straight line; BA and F'D' produced then meet at G,
    # and AC is parallel to GF'. VI.2 speaks of the triangle GBF' that AC cuts.
    _carried = _carried_over(e, f, d, c, _along(b, c, 2), beside=a)
    _f, _d = _carried[1], _carried[2]
    _far, _near = Line.through(b, a), Line.through(_f, _d)
    if not parallel(_far, _near):
        _g = posit(meet_one(_far, _near), "G")
        if (on_line(a, Line.through(b, _g)) and a != _g and b != _g
                and parallel(Line.through(a, c), Line.through(_g, _f))):
            because(prop_VI_2, b, _g, _f, a, c)

    claim("the sides about the equal angles are proportional", ["VI.2", "I.32"],
          similar((a, b, c), (d, e, f)))
    claim("in particular AB is to BC as DE is to EF", "VI.2",
          len2(a, b) * len2(e, f) == len2(d, e) * len2(b, c))
    return Out()