Viviani's theorem

TheoremViviani's theorem#✓fully proved

Let \(A\), \(B\), \(C\) be points of the Euclidean plane \(\mathbb{R}^2\) with \(AB = BC = CA\), and let \(P\) be a point of the interior of the convex hull of \(\lbrace A, B, C \rbrace\). Then the sum of the distances from \(P\) to the lines \(AB\), \(BC\) and \(CA\) equals the distance from \(A\) to the line \(BC\), the altitude of the triangle.

No positivity hypothesis on the side length is needed: since \(P\) is an interior point, the points \(A\), \(B\), \(C\) are affinely independent, so the triangle is nondegenerate.

Proof: Following the barycentric-coordinate area decomposition in Wikipedia, "Viviani's theorem" (Proof section), we express the three distances as barycentric weights times a common height.

theorem viviani_general : ∀ (A B C P : EuclideanSpace ℝ (Fin 2)),
  dist A B = dist B C → dist B C = dist C A →
  P ∈ interior (convexHull ℝ {A, B, C}) →
  Metric.infDist P ↑(affineSpan ℝ {A, B}) +
    Metric.infDist P ↑(affineSpan ℝ {B, C}) +
    Metric.infDist P ↑(affineSpan ℝ {C, A}) =
    Metric.infDist A ↑(affineSpan ℝ {B, C})

Sources

• https://en.wikipedia.org/wiki/Viviani%27s_theorem.

Used by 1

Used byViviani's theorem with a positive side length

TheoremViviani's theorem with a positive side length#✓fully proved

Let \(A\), \(B\), \(C\) be points of the Euclidean plane \(\mathbb{R}^2\) with \(AB = BC = CA\) and \(AB > 0\), and let \(P\) be a point of the interior of the convex hull of \(\lbrace A, B, C \rbrace\). Then the sum of the distances from \(P\) to the lines \(AB\), \(BC\) and \(CA\) equals the distance from \(A\) to the line \(BC\), the altitude of the triangle.

The hypothesis \(AB > 0\) is not needed: Viviani's theorem gives the same conclusion without it.

theorem viviani : ∀ (A B C P : EuclideanSpace ℝ (Fin 2)),
  dist A B = dist B C → dist B C = dist C A → 0 < dist A B →
  P ∈ interior (convexHull ℝ {A, B, C}) →
  Metric.infDist P ↑(affineSpan ℝ {A, B}) +
    Metric.infDist P ↑(affineSpan ℝ {B, C}) +
    Metric.infDist P ↑(affineSpan ℝ {C, A}) =
    Metric.infDist A ↑(affineSpan ℝ {B, C})

Uses 1

Proof usesViviani's theorem

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.