Spherical law of cosines

TheoremSpherical law of cosines, general form#✓fully proved

Write \(x \cdot y = \sum_{i=1}^{3} x_i y_i\) for the dot product and \(\lVert x \rVert = \sqrt{x \cdot x}\) for the Euclidean norm on \(\mathbb{R}^3\). Let \(u, v, w \in \mathbb{R}^3\) be unit vectors and let \(a, b, c, C\) be real numbers with \(0 < a < \pi\) and \(0 < b < \pi\). Suppose that \(v \cdot w = \cos a\), \(u \cdot w = \cos b\), \(u \cdot v = \cos c\) and

\[ \cos C = \frac{u \cdot v - (u \cdot w)(v \cdot w)} {\lVert u - (u \cdot w)\, w \rVert \, \lVert v - (v \cdot w)\, w \rVert}. \]

Then \(\cos c = \cos a \cos b + \sin a \sin b \cos C\).

Only \(a\) and \(b\) need to lie in \((0, \pi)\): \(c\) and \(C\) enter only through their cosines. The quotient above is the cosine of the angle at \(w\) between the great-circle arcs from \(w\) to \(u\) and from \(w\) to \(v\).

theorem spherical_law_of_cosines_general (a b c C : ℝ)
    (u v w : Fin 3 → ℝ)
    (ha : 0 < a ∧ a < Real.pi)
    (hb : 0 < b ∧ b < Real.pi)
    (hu : ∑ i, u i * u i = 1)
    (hv : ∑ i, v i * v i = 1)
    (hw : ∑ i, w i * w i = 1)
    (ha_side : ∑ i, v i * w i = Real.cos a)
    (hb_side : ∑ i, u i * w i = Real.cos b)
    (hc_side : ∑ i, u i * v i = Real.cos c)
    (hC_angle : Real.cos C = ((∑ i, u i * v i) - (∑ i, u i * w i) * (∑ i, v i * w i)) /
      (Real.sqrt (∑ i, (u i - (∑ j, u j * w j) * w i) * (u i - (∑ j, u j * w j) * w i)) * Real.sqrt
      (∑ i, (v i - (∑ j, v j * w j) * w i) * (v i - (∑ j, v j * w j) * w i)))) :
    Real.cos c = Real.cos a * Real.cos b + Real.sin a * Real.sin b * Real.cos C

Used by 1

Used bySpherical law of cosines

TheoremSpherical law of cosines#✓fully proved

Write \(x \cdot y = \sum_{i=1}^{3} x_i y_i\) for the dot product and \(\lVert x \rVert = \sqrt{x \cdot x}\) for the Euclidean norm on \(\mathbb{R}^3\). Let \(u, v, w \in \mathbb{R}^3\) be unit vectors and let \(a, b, c, C\) be real numbers, each strictly between \(0\) and \(\pi\). Suppose that \(v \cdot w = \cos a\), \(u \cdot w = \cos b\), \(u \cdot v = \cos c\) and

\[ \cos C = \frac{u \cdot v - (u \cdot w)(v \cdot w)} {\lVert u - (u \cdot w)\, w \rVert \, \lVert v - (v \cdot w)\, w \rVert}. \]

Then \(\cos c = \cos a \cos b + \sin a \sin b \cos C\).

Geometrically, \(u\), \(v\), \(w\) are the vertices of a spherical triangle on the unit sphere, \(a\), \(b\), \(c\) are the lengths of the sides opposite \(u\), \(v\), \(w\), and \(C\) is the angle at \(w\), opposite the side \(c\).

MetaMathlibExt.spherical_law_of_cosines · 16 lines

theorem spherical_law_of_cosines (a b c C : ℝ)
    (u v w : Fin 3 → ℝ)
    (ha : 0 < a ∧ a < Real.pi)
    (hb : 0 < b ∧ b < Real.pi)
    (hc : 0 < c ∧ c < Real.pi)
    (hC : 0 < C ∧ C < Real.pi)
    (hu : ∑ i, u i * u i = 1)
    (hv : ∑ i, v i * v i = 1)
    (hw : ∑ i, w i * w i = 1)
    (ha_side : ∑ i, v i * w i = Real.cos a)
    (hb_side : ∑ i, u i * w i = Real.cos b)
    (hc_side : ∑ i, u i * v i = Real.cos c)
    (hC_angle : Real.cos C = ((∑ i, u i * v i) - (∑ i, u i * w i) * (∑ i, v i * w i)) /
      (Real.sqrt (∑ i, (u i - (∑ j, u j * w j) * w i) * (u i - (∑ j, u j * w j) * w i)) * Real.sqrt
      (∑ i, (v i - (∑ j, v j * w j) * w i) * (v i - (∑ j, v j * w j) * w i)))) :
    Real.cos c = Real.cos a * Real.cos b + Real.sin a * Real.sin b * Real.cos C

Sources

• https://en.wikipedia.org/wiki/Spherical_law_of_cosines. It follows from spherical_law_of_cosines_general; the hypotheses hc and hC are unused and keep the source's shape.

Uses 1

Proof usesSpherical law of cosines, general form

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.