Book VI · Proposition 19

VI.19

Similar triangles are to one another in the duplicate ratio of the corresponding sides.Heath, 1908

Areas of similar triangles go as the squares on their sides. VI.20 generalises it to any figure, and VI.31 turns it into Pythagoras.

Every step, checked

• neither triangle is degenerategiven
• the triangles are similargiven
• the triangles are to one another in the duplicate ratio of BC to EFby VI.11, VI.15

What it needs, and what needs it

Needs: VI.11 VI.15

Used by: VI.20 VI.25

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: 17 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "VI.19",
    THEOREM,
    sample=_similar_triangles,
    note="Areas of similar triangles go as the squares on their sides. VI.20 "
    "generalises it to any figure, and VI.31 turns it into Pythagoras.",
)
def prop_VI_19(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("neither triangle is degenerate",
               not collinear(a, b, c) and not collinear(d, e, f))
    hypothesis("the triangles are similar", similar((a, b, c), (d, e, f)))
    outline(a, b, c)
    outline(d, e, f)
    # Euclid takes BG a third proportional to BC and EF, and VI.11 is what finds
    # it; the triangle on BG then equals DEF, which is where VI.15 comes in.
    because(prop_VI_11, b, c, length(e, f) / length(b, c))
    _third = posit(_at_distance(b, c, len2(e, f) / length(b, c)), "G")
    if not collinear(b, a, _third):
        because(prop_VI_15, b, a, _third, e, d, f)

    claim("the triangles are to one another in the duplicate ratio of BC to EF",
          ["VI.11", "VI.15"],
          _area(a, b, c) * len2(e, f) == _area(d, e, f) * len2(b, c))
    return Out()