Freek № 57: Heron's Formula

This file proves Theorem 57 from the 100 Theorems List, also known as Heron's formula, which gives the area of a triangle based only on its three sides' lengths.

References

• https://en.wikipedia.org/wiki/Herons_formula

theorem Theorems100.heron {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {p1 : P} {p2 : P} {p3 : P} (h1 : p1 ≠ p2) (h2 : p3 ≠ p2) : let a := dist p1 p2; let b := dist p3 p2; let c := dist p1 p3; let s := (a + b + c) / 2; 1 / 2 * a * b * Real.sin (EuclideanGeometry.angle p1 p2 p3) = √(s * (s - a) * (s - b) * (s - c))

Heron's formula: The area of a triangle with side lengths a, b, and c is √(s * (s - a) * (s - b) * (s - c)) where s = (a + b + c) / 2 is the semiperimeter. We show this by equating this formula to a * b * sin γ, where γ is the angle opposite the side c.