Book VI · Proposition 8

VI.8

If in a right-angled triangle a perpendicular be drawn from the right angle to the base, the triangles adjoining the perpendicular are similar both to the whole and to one another.Heath, 1908

Dropping the perpendicular from the right angle splits the triangle into two copies of itself -- and gives VI.13's mean proportional at once.

Every step, checked

• the angle at B is rightgiven
• ABC is a genuine trianglegiven
• BD is perpendicular to the baseby I.12
• each adjoining triangle is similar to the wholeby VI.4
• and so to one anotherby VI.4
• whence BD is the mean proportional between the segmentsby VI.4

What it needs, and what needs it

Needs: I.12 VI.4

Used by: VI.13

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

The proposition as code

@proposition(
    "VI.8",
    THEOREM,
    sample=samples.right_triangle,
    note="Dropping the perpendicular from the right angle splits the triangle "
    "into two copies of itself -- and gives VI.13's mean proportional at once.",
)
def prop_VI_8(a: Point, b: Point, c: Point) -> Out:
    """The right angle is at B; the perpendicular falls from B to AC."""
    hypothesis("the angle at B is right", right_angle(a, b, c))
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    outline(a, b, c)

    ux, uy = c.x - a.x, c.y - a.y
    along = ((b.x - a.x) * ux + (b.y - a.y) * uy) / (ux * ux + uy * uy)
    foot = posit(Point(a.x + along * ux, a.y + along * uy), "D")
    line(b, foot, "the perpendicular BD")

    because(prop_I_12, a, c, b)
    because(prop_VI_4, a, foot, b, a, b, c)

    claim("BD is perpendicular to the base", "I.12", right_angle(b, foot, a))
    claim("each adjoining triangle is similar to the whole", "VI.4",
          similar((a, foot, b), (a, b, c)) and similar((b, foot, c), (a, b, c)))
    claim("and so to one another", "VI.4", similar((a, foot, b), (b, foot, c)))
    claim("whence BD is the mean proportional between the segments", "VI.4",
          len2(b, foot) == length(a, foot) * length(foot, c))
    return Out(foot=foot)