Napoleon's theorem

TheoremNapoleon's theorem, general form#✓fully proved

Let \(A\), \(B\), \(C\), \(A_2\), \(B_2\), \(C_2\) be points of the Euclidean plane \(\mathbb{R}^2\) with \(|BA_2| = |CA_2| = |BC|\), \(|CB_2| = |AB_2| = |CA|\) and \(|AC_2| = |BC_2| = |AB|\), such that \(A_2\) and \(A\) lie strictly on opposite sides of the line \(BC\), \(B_2\) and \(B\) lie strictly on opposite sides of the line \(CA\), and \(C_2\) and \(C\) lie strictly on opposite sides of the line \(AB\). Let \(G_1 = \frac{1}{3}(B + C + A_2)\), \(G_2 = \frac{1}{3}(C + A + B_2)\) and \(G_3 = \frac{1}{3}(A + B + C_2)\). Then \(|G_1G_2| = |G_2G_3| = |G_3G_1| > 0\).

Thus the centroids \(G_1\), \(G_2\), \(G_3\) of the equilateral triangles erected outward on the sides of \(ABC\) form a nondegenerate equilateral triangle; the hypotheses force \(A\), \(B\), \(C\) to be non-collinear. Opposite sides are expressed by signed areas, for instance \(((C - B) \times (A - B)) \, ((C - B) \times (A_2 - B)) < 0\), where \((x, y) \times (x', y') = x y' - y x'\).

MetaMathlibExt.napoleon_theorem_general · 20 lines

theorem napoleon_theorem_general (A B C A2 B2 C2 G1 G2 G3 : EuclideanSpace ℝ (Fin 2))
    (hBA2 : dist B A2 = dist B C) (hCA2 : dist C A2 = dist B C)
    (hCB2 : dist C B2 = dist C A) (hAB2 : dist A B2 = dist C A)
    (hAC2 : dist A C2 = dist A B) (hBC2 : dist B C2 = dist A B)
    (hout1 : ((C.ofLp 0 - B.ofLp 0) * (A.ofLp 1 - B.ofLp 1) -
          (C.ofLp 1 - B.ofLp 1) * (A.ofLp 0 - B.ofLp 0)) *
        ((C.ofLp 0 - B.ofLp 0) * (A2.ofLp 1 - B.ofLp 1) -
          (C.ofLp 1 - B.ofLp 1) * (A2.ofLp 0 - B.ofLp 0)) < 0)
    (hout2 : ((A.ofLp 0 - C.ofLp 0) * (B.ofLp 1 - C.ofLp 1) -
          (A.ofLp 1 - C.ofLp 1) * (B.ofLp 0 - C.ofLp 0)) *
        ((A.ofLp 0 - C.ofLp 0) * (B2.ofLp 1 - C.ofLp 1) -
          (A.ofLp 1 - C.ofLp 1) * (B2.ofLp 0 - C.ofLp 0)) < 0)
    (hout3 : ((B.ofLp 0 - A.ofLp 0) * (C.ofLp 1 - A.ofLp 1) -
          (B.ofLp 1 - A.ofLp 1) * (C.ofLp 0 - A.ofLp 0)) *
        ((B.ofLp 0 - A.ofLp 0) * (C2.ofLp 1 - A.ofLp 1) -
          (B.ofLp 1 - A.ofLp 1) * (C2.ofLp 0 - A.ofLp 0)) < 0)
    (hG1 : G1 = (1 / 3 : ℝ) • (B + C + A2))
    (hG2 : G2 = (1 / 3 : ℝ) • (C + A + B2))
    (hG3 : G3 = (1 / 3 : ℝ) • (A + B + C2)) :
    dist G1 G2 = dist G2 G3 ∧ dist G2 G3 = dist G3 G1 ∧ 0 < dist G1 G2

Used by 1

Used byNapoleon's theorem

TheoremNapoleon's theorem#✓fully proved

Let \(A\), \(B\), \(C\) be pairwise distinct, non-collinear points of the Euclidean plane \(\mathbb{R}^2\), and let \(A_2\), \(B_2\), \(C_2\) be points with \(|BA_2| = |CA_2| = |BC|\), \(|CB_2| = |AB_2| = |CA|\) and \(|AC_2| = |BC_2| = |AB|\), such that \(A_2\) and \(A\) lie strictly on opposite sides of the line \(BC\), \(B_2\) and \(B\) lie strictly on opposite sides of the line \(CA\), and \(C_2\) and \(C\) lie strictly on opposite sides of the line \(AB\). Let \(G_1 = \frac{1}{3}(B + C + A_2)\), \(G_2 = \frac{1}{3}(C + A + B_2)\) and \(G_3 = \frac{1}{3}(A + B + C_2)\). Then \(|G_1G_2| = |G_2G_3| = |G_3G_1|\).

That is, the centroids of the equilateral triangles erected outward on the sides of \(ABC\) are pairwise equidistant. Non-collinearity is stated as \((B - A) \times (C - A) \ne 0\) and opposite sides by signed areas, for instance \(((C - B) \times (A - B)) \, ((C - B) \times (A_2 - B)) < 0\), where \((x, y) \times (x', y') = x y' - y x'\).

MetaMathlibExt.napoleon_theorem · 24 lines

theorem napoleon_theorem :
    ∀ (A B C A2 B2 C2 G1 G2 G3 : EuclideanSpace ℝ (Fin 2)),
      A ≠ B → B ≠ C → C ≠ A →
      ((B.ofLp 0 - A.ofLp 0) * (C.ofLp 1 - A.ofLp 1) -
          (B.ofLp 1 - A.ofLp 1) * (C.ofLp 0 - A.ofLp 0) ≠ 0) →
      dist B A2 = dist B C → dist C A2 = dist B C →
      dist C B2 = dist C A → dist A B2 = dist C A →
      dist A C2 = dist A B → dist B C2 = dist A B →
      (((C.ofLp 0 - B.ofLp 0) * (A.ofLp 1 - B.ofLp 1) -
            (C.ofLp 1 - B.ofLp 1) * (A.ofLp 0 - B.ofLp 0)) *
          ((C.ofLp 0 - B.ofLp 0) * (A2.ofLp 1 - B.ofLp 1) -
            (C.ofLp 1 - B.ofLp 1) * (A2.ofLp 0 - B.ofLp 0)) < 0) →
      (((A.ofLp 0 - C.ofLp 0) * (B.ofLp 1 - C.ofLp 1) -
            (A.ofLp 1 - C.ofLp 1) * (B.ofLp 0 - C.ofLp 0)) *
          ((A.ofLp 0 - C.ofLp 0) * (B2.ofLp 1 - C.ofLp 1) -
            (A.ofLp 1 - C.ofLp 1) * (B2.ofLp 0 - C.ofLp 0)) < 0) →
      (((B.ofLp 0 - A.ofLp 0) * (C.ofLp 1 - A.ofLp 1) -
            (B.ofLp 1 - A.ofLp 1) * (C.ofLp 0 - A.ofLp 0)) *
          ((B.ofLp 0 - A.ofLp 0) * (C2.ofLp 1 - A.ofLp 1) -
            (B.ofLp 1 - A.ofLp 1) * (C2.ofLp 0 - A.ofLp 0)) < 0) →
      G1 = (1 / 3 : ℝ) • (B + C + A2) →
      G2 = (1 / 3 : ℝ) • (C + A + B2) →
      G3 = (1 / 3 : ℝ) • (A + B + C2) →
      dist G1 G2 = dist G2 G3 ∧ dist G2 G3 = dist G3 G1

Sources

• https://en.wikipedia.org/wiki/Napoleon%27s_theorem (statement id napoleon-s1; raw: "Outer equilateral-triangle centers on any triangle form an equilateral triangle."). It follows from napoleon_theorem_general, which also shows the common distance is positive; the hypotheses A ≠ B, B ≠ C, C ≠ A and nondegeneracy are unused and keep the source's shape.

Uses 1

Proof usesNapoleon's theorem, general form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.