Triangle geometry

Theorems about triangles, their centers, cevians, inscribed and circumscribed circles, and triangle inequalities.

• Angle bisector theorem
• Carnot's theorem
• Erdős–Mordell inequality
• Hinge theorem
• Menelaus's theorem
• Morley's trisector theorem
• Napoleon's theorem
• Pompeiu's theorem
• Van Schooten's theorem
• Viviani's theorem

TheoremConway circle theorem#✓fully proved

Let \(A\), \(B\), \(C\) be affinely independent points of the Euclidean plane, and write \(a = d(B, C)\), \(b = d(A, C)\), \(c = d(A, B)\) for the side lengths, where \(d\) is the Euclidean distance. Extend each side beyond each of its endpoints by the length of the side opposite that endpoint; this gives the six points

\[A + \tfrac{a}{c}(A - B),\quad B + \tfrac{b}{c}(B - A),\quad B + \tfrac{b}{a}(B - C),\]

\[C + \tfrac{c}{a}(C - B),\quad C + \tfrac{c}{b}(C - A),\quad A + \tfrac{a}{b}(A - C).\]

Then there are a point \(O\) and a real number \(r\) such that all six points are at distance \(r\) from \(O\).

theorem conway_circle_theorem (A B C : EuclideanSpace ℝ (Fin 2))
    (hABC : AffineIndependent ℝ (![A, B, C] : Fin 3 → EuclideanSpace ℝ (Fin 2))) :
    ∃ (O : EuclideanSpace ℝ (Fin 2)) (r : ℝ),
      A + (dist B C / dist A B) • (A - B) ∈ Metric.sphere O r ∧
      B + (dist A C / dist A B) • (B - A) ∈ Metric.sphere O r ∧
      B + (dist A C / dist B C) • (B - C) ∈ Metric.sphere O r ∧
      C + (dist A B / dist B C) • (C - B) ∈ Metric.sphere O r ∧
      C + (dist A B / dist A C) • (C - A) ∈ Metric.sphere O r ∧
      A + (dist B C / dist A C) • (A - C) ∈ Metric.sphere O r

Sources

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

TheoremEuler's theorem on the circumcenter–incenter distance#✓fully proved

Let \(P_0, P_1, P_2\) be affinely independent points of the Euclidean plane, \(d\) the Euclidean distance and \(\langle x, y \rangle\) the inner product. Let \(O\) be a point and \(R \ge 0\) with \(d(O, P_i) = R\) for each \(i\), so that \(O\) is the circumcenter and \(R\) the circumradius. Let \(I = w_0 P_0 + w_1 P_1 + w_2 P_2\) with \(w_0, w_1, w_2 > 0\) and \(w_0 + w_1 + w_2 = 1\), and let \(r \ge 0\). Suppose there are points \(F_0\) on the line \(P_0 P_1\), \(F_1\) on the line \(P_1 P_2\) and \(F_2\) on the line \(P_2 P_0\) with \(d(I, F_k) = r\) for each \(k\) and \(\langle F_0 - I, P_1 - P_0 \rangle = \langle F_1 - I, P_2 - P_1 \rangle = \langle F_2 - I, P_0 - P_2 \rangle = 0\), so that \(I\) is an interior point at distance \(r\) from all three side lines, that is, the incenter, and \(r\) is the inradius. Then \(d(O, I)^2 = R(R - 2r)\) and \(R \ge 2r\).

MetaMathlibExt.euler_oi · 20 lines

theorem euler_oi :
    ∀ (P : Fin 3 → EuclideanSpace ℝ (Fin 2)) (O I F0 F1 F2 : EuclideanSpace ℝ (Fin 2))
      (R r w0 w1 w2 : ℝ),
      AffineIndependent ℝ P →
      (∀ i, dist O (P i) = R) →
      0 ≤ R →
      0 ≤ r →
      F0 ∈ affineSpan ℝ {P 0, P 1} →
      F1 ∈ affineSpan ℝ {P 1, P 2} →
      F2 ∈ affineSpan ℝ {P 2, P 0} →
      dist I F0 = r →
      dist I F1 = r →
      dist I F2 = r →
      ⟪F0 - I, P 1 - P 0⟫_ℝ = 0 →
      ⟪F1 - I, P 2 - P 1⟫_ℝ = 0 →
      ⟪F2 - I, P 0 - P 2⟫_ℝ = 0 →
      0 < w0 → 0 < w1 → 0 < w2 →
      w0 + w1 + w2 = 1 →
      w0 • P 0 + w1 • P 1 + w2 • P 2 = I →
      (dist O I) ^ 2 = R * (R - 2 * r) ∧ R ≥ 2 * r

Sources

• https://en.wikipedia.org/wiki/Euler%27s_theorem_in_geometry

TheoremFeuerbach's theorem#✓fully proved

Let \(T\) be a triangle in a two-dimensional Euclidean affine space, with incircle \(\omega\), nine-point circle \(N\), and excircle \(\omega_i\) opposite its \(i\)-th vertex for each \(i\). If \(T\) is not equilateral, then there is a point \(F\) at which \(\omega\) is internally tangent to \(N\) (that is, \(F\) lies on both circles and the center of \(\omega\) lies on the segment from the center of \(N\) to \(F\)), and \(F\) is the only common point of \(\omega\) and \(N\). For every triangle \(T\) and every \(i\), the nine-point circle \(N\) is externally tangent to \(\omega_i\).

theorem Feuerbach_theorem {V P : Type*} [NormedAddCommGroup V]
    [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
    [Fact (Module.finrank ℝ V = 2)] (s : Affine.Triangle ℝ P) :
    (¬ (dist (s.points 0) (s.points 1) = dist (s.points 1) (s.points 2) ∧
      dist (s.points 1) (s.points 2) = dist (s.points 2) (s.points 0)) →
    (∃ F, s.insphere.IsIntTangentAt s.ninePointCircle F ∧
      ∀ G, G ∈ s.insphere → G ∈ s.ninePointCircle → G = F)) ∧
      ∀ i, s.ninePointCircle.IsExtTangent (s.exsphere {i})

Sources

• K. W. Feuerbach, 1822; https://en.wikipedia.org/wiki/Feuerbach_point

TheoremIntercept theorem#✓fully proved

Let \(A, B, C, D, E\) be points of the Euclidean plane \(\mathbb{R}^2\), and write \(XY\) for the distance between points \(X\) and \(Y\). Suppose that \(C - A\) is not a real multiple of \(B - A\); that \(AD + DB = AB\) with \(AD > 0\) and \(DB > 0\), so \(D\) lies strictly between \(A\) and \(B\); that \(AE + EC = AC\) with \(AE > 0\) and \(EC > 0\), so \(E\) lies strictly between \(A\) and \(C\); and that \(E - D = r(C - B)\) for some real \(r \ne 0\), so \(DE\) is parallel to \(BC\). Then \(AD / DB = AE / EC\).

theorem intercept_theorem : ∀ (A B C D E : EuclideanSpace ℝ (Fin 2)),
  dist A D + dist D B = dist A B →
  0 < dist A D →
  0 < dist D B →
  dist A E + dist E C = dist A C →
  0 < dist A E →
  0 < dist E C →
  (¬ ∃ t : ℝ, C - A = t • (B - A)) →
  (∃ r : ℝ, r ≠ 0 ∧ E - D = r • (C - B)) →
  dist A D / dist D B = dist A E / dist E C

Sources

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

TheoremMarden's theorem#✓fully proved

Let \(a, b, c\) be complex numbers such that \((b - a)/(c - a)\) has nonzero imaginary part, so that they are the vertices of a nondegenerate triangle, and let \(p(z) = (z - a)(z - b)(z - c)\). Then there are complex numbers \(f_1, f_2\) and a real number \(L\) such that the roots of \(p'\), counted with multiplicity, are exactly \(f_1\) and \(f_2\), and such that the function \(\sigma(z) = |z - f_1| + |z - f_2|\) satisfies \(\sigma((a + b)/2) = \sigma((b + c)/2) = \sigma((c + a)/2) = L\) and, for every real \(t \ne 0\), \(\sigma((a + b)/2 + t(b - a)) > L\), \(\sigma((b + c)/2 + t(c - b)) > L\) and \(\sigma((c + a)/2 + t(a - c)) > L\).

Thus the ellipse \(\sigma(z) = L\) with foci \(f_1\) and \(f_2\) (a circle when \(f_1 = f_2\)) passes through the midpoints of the three sides and touches each side line only at its midpoint: it is the Steiner inellipse, and its foci are the roots of \(p'\).

Proof: The statement is Marden's theorem (M. Marden, Geometry of Polynomials, 2nd ed., Math. Surveys No. 3, AMS, 1966; D. Kalman, An Elementary Proof of Marden's Theorem, Amer. Math. Monthly 115(4) (2008), 330-338, https://doi.org/10.1080/00029890.2008.11920532). Following Wikipedia, Marden's theorem, we use Vieta's relations, the midpoint identity for the derivative, and the ellipse reflection property expressed by a strict triangle inequality.

MetaMathlibExt.marden · 19 lines

theorem marden : ∀ (a b c : ℂ),
    ((b - a) / (c - a)).im ≠ 0 →
    ∃ (f1 f2 : ℂ) (L : ℝ),
      Polynomial.roots (Polynomial.derivative
        ((Polynomial.X - Polynomial.C a) *
          (Polynomial.X - Polynomial.C b) *
          (Polynomial.X - Polynomial.C c))) = {f1, f2} ∧
      ‖(a + b) / 2 - f1‖ + ‖(a + b) / 2 - f2‖ = L ∧
      ‖(b + c) / 2 - f1‖ + ‖(b + c) / 2 - f2‖ = L ∧
      ‖(c + a) / 2 - f1‖ + ‖(c + a) / 2 - f2‖ = L ∧
      (∀ t : ℝ, t ≠ 0 →
        L < ‖(a + b) / 2 + (t : ℂ) * (b - a) - f1‖ +
          ‖(a + b) / 2 + (t : ℂ) * (b - a) - f2‖) ∧
      (∀ t : ℝ, t ≠ 0 →
        L < ‖(b + c) / 2 + (t : ℂ) * (c - b) - f1‖ +
          ‖(b + c) / 2 + (t : ℂ) * (c - b) - f2‖) ∧
      (∀ t : ℝ, t ≠ 0 →
        L < ‖(c + a) / 2 + (t : ℂ) * (a - c) - f1‖ +
          ‖(c + a) / 2 + (t : ℂ) * (a - c) - f2‖)

Sources

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

TheoremRouth's theorem#✓fully proved

Let \(A, B, C\) be points of the Euclidean plane \(\mathbb{R}^2\) whose triangle (the convex hull of \(\{A, B, C\}\)) has nonzero area, and let \(x, y, z\) be positive reals with \(xyz \ne 1\). Let \(D = \frac{x}{x+1} B + \frac{1}{x+1} C\), \(E = \frac{1}{y+1} A + \frac{y}{y+1} C\) and \(F = \frac{z}{z+1} A + \frac{1}{z+1} B\), the points of the sides \(BC\), \(CA\), \(AB\) with \(DC/DB = x\), \(EA/EC = y\) and \(FB/FA = z\). If \(P\) lies on the segments \(BE\) and \(CF\), \(Q\) lies on the segments \(CF\) and \(AD\), and \(R\) lies on the segments \(AD\) and \(BE\), then the area of the triangle \(PQR\) (the convex hull of \(\{P, Q, R\}\)) is

\[\frac{(xyz - 1)^2}{(xy + y + 1)(yz + z + 1)(zx + x + 1)}\]

times the area of \(ABC\). Areas are Lebesgue measures.

MetaMathlibExt.routh · 19 lines

theorem routh :
    ∀ (A B C D E F P Q R : EuclideanSpace ℝ (Fin 2)) (x y z : ℝ),
      0 < x →
      0 < y →
      0 < z →
      x * y * z ≠ 1 →
      MeasureTheory.volume (convexHull ℝ ({A, B, C} : Set (EuclideanSpace ℝ (Fin 2)))) ≠ 0 →
      D = (x / (x + 1)) • B + (1 / (x + 1)) • C →
      E = (1 / (y + 1)) • A + (y / (y + 1)) • C →
      F = (z / (z + 1)) • A + (1 / (z + 1)) • B →
      P ∈ convexHull ℝ ({B, E} : Set (EuclideanSpace ℝ (Fin 2))) →
      P ∈ convexHull ℝ ({C, F} : Set (EuclideanSpace ℝ (Fin 2))) →
      Q ∈ convexHull ℝ ({C, F} : Set (EuclideanSpace ℝ (Fin 2))) →
      Q ∈ convexHull ℝ ({A, D} : Set (EuclideanSpace ℝ (Fin 2))) →
      R ∈ convexHull ℝ ({A, D} : Set (EuclideanSpace ℝ (Fin 2))) →
      R ∈ convexHull ℝ ({B, E} : Set (EuclideanSpace ℝ (Fin 2))) →
      (MeasureTheory.volume (convexHull ℝ ({P, Q, R} : Set (EuclideanSpace ℝ (Fin 2))))).toReal =
        ((x * y * z - 1) ^ 2 / ((x * y + y + 1) * (y * z + z + 1) * (z * x + x + 1))) *
          (MeasureTheory.volume (convexHull ℝ ({A, B, C} : Set (EuclideanSpace ℝ (Fin 2))))).toReal

Sources

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

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.