De Gua's theorem

TheoremDe Gua's theorem#✓fully proved

Let \(u, v, w \in \mathbb{R}^3\) be pairwise orthogonal vectors, so that the tetrahedron with vertices \(0, u, v, w\) has a right angle between any two of the edges at \(0\). Write \(|x|\) for the Euclidean norm and \(\langle x, y \rangle\) for the inner product. Let \(A_{uv}, A_{uw}, A_{vw}, A\) be real numbers with \(A_{uv} = |u||v|/2\), \(A_{uw} = |u||w|/2\), \(A_{vw} = |v||w|/2\) (the areas of the three right-angled faces) and \((2A)^2 = |u - v|^2 |u - w|^2 - \langle u - v, u - w \rangle^2\), so that \(A\) is, up to sign, the area of the face with vertices \(u, v, w\). Then \(A^2 = A_{uv}^2 + A_{uw}^2 + A_{vw}^2\).

theorem deGua : ∀ (u v w : EuclideanSpace ℝ (Fin 3)),
  ⟪u, v⟫_ℝ = 0 →
  ⟪u, w⟫_ℝ = 0 →
  ⟪v, w⟫_ℝ = 0 →
  ∀ (Auv Auw Avw Ahyp : ℝ),
  Auv = ‖u‖ * ‖v‖ / 2 →
  Auw = ‖u‖ * ‖w‖ / 2 →
  Avw = ‖v‖ * ‖w‖ / 2 →
  (2 * Ahyp) ^ 2 = ‖u - v‖ ^ 2 * ‖u - w‖ ^ 2 - (⟪u - v, u - w⟫_ℝ) ^ 2 →
  Ahyp ^ 2 = Auv ^ 2 + Auw ^ 2 + Avw ^ 2

Sources

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

TheoremDe Gua's theorem with Heron's formula#✓fully proved

Let \(a, b, c > 0\) and let \(p_0 = (a, 0, 0)\), \(p_1 = (0, b, 0)\), \(p_2 = (0, 0, c)\) in \(\mathbb{R}^3\), so that the tetrahedron with vertices \(0, p_0, p_1, p_2\) has a right angle between any two of the edges at \(0\), with legs of lengths \(a\), \(b\), \(c\). Let \(d_{01} = d(p_0, p_1)\), \(d_{12} = d(p_1, p_2)\) and \(d_{20} = d(p_2, p_0)\) be the Euclidean distances, let \(s = (d_{01} + d_{12} + d_{20})/2\), and let \(A = \sqrt{s(s - d_{01})(s - d_{12})(s - d_{20})}\), the area of the face \(p_0 p_1 p_2\) by Heron's formula. Then \(A^2 = (ab/2)^2 + (bc/2)^2 + (ca/2)^2\).

theorem deGua_theorem : ∀ (a b c A : ℝ),
  let p₀ := EuclideanSpace.single (0 : Fin 3) a
  let p₁ := EuclideanSpace.single (1 : Fin 3) b
  let p₂ := EuclideanSpace.single (2 : Fin 3) c
  let s := (dist p₀ p₁ + dist p₁ p₂ + dist p₂ p₀) / 2
  0 < a → 0 < b → 0 < c →
  A = Real.sqrt (s * ((s - dist p₀ p₁) * ((s - dist p₁ p₂) * (s - dist p₂ p₀)))) →
  A ^ 2 = (a * b / 2) ^ 2 + (b * c / 2) ^ 2 + (c * a / 2) ^ 2

Sources

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

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.