Math 2.0

Geometry Proof

Proof of the law of sines from the law of cosines

Builds on TriangleAngle at a pointCollinear pointsEuclidean distanceLength of a vectorDot productLaw of cosinesLinear independenceCauchy–Schwarz inequalitySine and cosinePythagorean trigonometric identity

Proof

We compute each sine from the three sides and find that the three quotients are given by one symmetric formula.

  1. The vertices of the triangle are not collinear, so they are distinct. Thus a,b,c>0a, b, c > 0, and the three angles are defined.
  2. We apply the law of cosines with the vertices renamed, so that AA plays the role of CC. It gives a2=b2+c2−2bccos⁡αa^2 = b^2 + c^2 - 2bc \cos \alpha. So cos⁡α=b2+c2−a22bc\cos \alpha = \dfrac{b^2 + c^2 - a^2}{2bc}.
  3. In the same way, cos⁡β=c2+a2−b22ca\cos \beta = \dfrac{c^2 + a^2 - b^2}{2ca} and cos⁡γ=a2+b2−c22ab\cos \gamma = \dfrac{a^2 + b^2 - c^2}{2ab}.
  4. Let Q=4b2c2−(b2+c2−a2)2Q = 4b^2c^2 - (b^2 + c^2 - a^2)^2. Two differences of squares give Q=(a2−(b−c)2)((b+c)2−a2)=(a−b+c)(a+b−c)(b+c−a)(a+b+c)Q = \left( a^2 - (b - c)^2 \right) \left( (b + c)^2 - a^2 \right) = (a - b + c)(a + b - c)(b + c - a)(a + b + c).
  5. A permutation of aa, bb, cc only permutes the four factors in step 4. So step 4 with the letters renamed gives Q=4c2a2−(c2+a2−b2)2=4a2b2−(a2+b2−c2)2Q = 4c^2a^2 - (c^2 + a^2 - b^2)^2 = 4a^2b^2 - (a^2 + b^2 - c^2)^2.
  6. Let x=B−Ax = B - A and y=C−Ay = C - A. With the length and the dot product, ∥x∥=c\norm{x} = c, ∥y∥=b\norm{y} = b and x⋅y=bccos⁡α=12(b2+c2−a2)x \cdot y = bc \cos \alpha = \frac{1}{2}(b^2 + c^2 - a^2). So Q=4(∥x∥2∥y∥2−(x⋅y)2)Q = 4 \left( \norm{x}^2 \norm{y}^2 - (x \cdot y)^2 \right).
  7. Every difference of two vertices lies in the span of xx and yy. Since the vertices are not collinear, this span has dimension 22. So xx and yy are linearly independent.
  8. By the Cauchy–Schwarz inequality and its case of equality, (x⋅y)2<∥x∥2∥y∥2(x \cdot y)^2 < \norm{x}^2 \norm{y}^2. So Q>0Q > 0. Let R=Q>0R = \sqrt{Q} > 0.
  9. The sine is nonnegative on [0,π][0, \pi], and α∈[0,π]\alpha \in [0, \pi]. By the identity sin⁡2+cos⁡2=1\sin^2 + \cos^2 = 1 and step 2, sin⁡2α=1−cos⁡2α=Q4b2c2\sin^2 \alpha = 1 - \cos^2 \alpha = \dfrac{Q}{4b^2c^2}. So sin⁡α=R2bc>0\sin \alpha = \dfrac{R}{2bc} > 0.
  10. In the same way, steps 3 and 5 give sin⁡β=R2ca>0\sin \beta = \dfrac{R}{2ca} > 0 and sin⁡γ=R2ab>0\sin \gamma = \dfrac{R}{2ab} > 0. So the three quotients are defined.
  11. By steps 9 and 10, asin⁡α=2abcR\dfrac{a}{\sin \alpha} = \dfrac{2abc}{R}, bsin⁡β=2abcR\dfrac{b}{\sin \beta} = \dfrac{2abc}{R} and csin⁡γ=2abcR\dfrac{c}{\sin \gamma} = \dfrac{2abc}{R}.
  12. Hence asin⁡α=bsin⁡β=csin⁡γ\dfrac{a}{\sin \alpha} = \dfrac{b}{\sin \beta} = \dfrac{c}{\sin \gamma}.

Idea

The law of cosines gives each cosine from the sides, and then each sine. All three sines have the same numerator Q\sqrt{Q}, a symmetric expression in the sides, which is four times the area. Dividing a side by the sine of the opposite angle then gives 2abc/Q2abc / \sqrt{Q} every time.

Reading path

To understand this page from the ground up, read these 261 pages in order. The foundations come first. The path takes the proofs Proof of the Cauchy–Hadamard theorem, Proof of the derivative of cosine by term-by-term differentiation, Proof of the Weierstrass M-test, Proof of the limit of a sum of sequences, Proof of Rolle's theorem, Proof of the approximation property of the supremum, Proof that every sequence has a monotone subsequence, by peaks, Proof of the formula for the derivative of a polynomial, Proof of the commutativity of addition by induction, Proof of term-by-term differentiation, Proof of the epsilon-delta form of continuity, Proof of the power rule by induction, Proof that absolutely convergent series converge, Proof of the sum of a finite geometric series, Proof that convergent sequences are Cauchy, Proof that a complex number times its conjugate is the square of its modulus, Proof of the Cauchy–Schwarz inequality, Proof that there is a natural number n with 1/n below any positive epsilon, Proof of the chain rule with an auxiliary difference quotient, Proof of the Cauchy criterion for series, Proof of the Cauchy criterion for sequences by the Bolzano–Weierstrass theorem, Proof of the equality of complex numbers, Proof that the reals form an ordered field, with the Cauchy sequence construction, Proof of the root test, Proof of the double negation law by a truth table, Proof that power series converge uniformly on smaller intervals inside the radius of convergence, Proof of the extreme value theorem by the Bolzano–Weierstrass theorem, Proof of the uniqueness of limits, Proof of strong induction from ordinary induction, Proof that power series are differentiable inside the radius of convergence, Proof of the limit of a product of sequences, Proof that uniform convergence of derivatives allows term-by-term differentiation, Proof that the absolute value is multiplicative, Proof of the squeeze theorem for sequences, Proof of the existence of square roots of nonnegative reals, Proof of Pascal's rule from the recursive definition, Proof of the linearity of differentiation, Proof of the sequential characterization of limits, Proof that Cauchy sequences are bounded, Proof of the triangle inequality for real numbers, Proof of the epsilon-N definition of the limit of a sequence, Proof of the comparison test, Proof of Fermat's theorem on stationary points, Proof that limits preserve non-strict inequalities, Proof of the factorial formula for binomial coefficients by induction, Proof of the binomial theorem by induction, Proof that exponentials dominate powers in sequences, by the ratio of consecutive terms, Proof that differentiable functions are continuous, Proof of the epsilon-delta form of the limit of a function, Proof of the derivative of sine by term-by-term differentiation, Proof of the well-ordering principle from strong induction, Proof of the Bolzano–Weierstrass theorem by a monotone subsequence, Proof of the Archimedean property in an Archimedean ordered field, Proof that a composition of continuous functions is continuous, Proof of the Pythagorean trigonometric identity by differentiation, Proof that a decreasing sequence bounded below converges, Proof of the term test, Proof that the reals are Archimedean from the completeness axiom, Proof of the ratio test, Proof that convergent sequences are bounded, Proof of the law of cosines with the dot product, Proof of the product rule, Proof of the monotone convergence theorem for sequences, Proof that continuity is equivalent to sequential continuity, Proof that a function with zero derivative on an open interval is constant, Proof of the boundedness theorem by Bolzano–Weierstrass, Proof that a series of nonnegative terms converges iff its partial sums are bounded, Proof of the mean value theorem from Rolle's theorem, Proof of the constant multiple rule.

  1. Angle at a point concept
  2. Binomial coefficient definition
  3. Collinear points concept
  4. Complex numbers object
  5. Complex numbers as pairs of reals concept
  6. Construction of the reals from Cauchy sequences concept
  7. Definition by recursion concept
  8. Dot product concept
  9. Element definition
  10. Euclidean distance concept
  11. Factorial definition
  12. Group concept
  13. Imaginary unit object
  14. Inner product concept
  15. Inner product space concept
  16. Integers object
  17. Length of a vector concept
  18. Limit point of a set definition
  19. Linear independence concept
  20. Local maximum definition
  21. Mathematical induction concept
  22. Natural numbers object
  23. Norm induced by an inner product concept
  24. Ordered field definition
  25. Peano axioms concept
  26. Proposition concept
  27. Rational numbers object
  28. Real numbers object
  29. Sequence definition
  30. Set bounded above definition
  31. Sine and cosine concept
  32. Triangle concept
  33. Vector space definition
  34. Proof of Pascal's rule from the recursive definition proof
  35. Real and imaginary parts definition
  36. Set definition
  37. Ring definition
  38. Proof of the law of cosines with the dot product proof
  39. Ring of integers statement
  40. Limit of a function definition
  41. Local minimum definition
  42. Successor function definition
  43. Archimedean ordered field definition
  44. Conjunction definition
  45. Disjunction definition
  46. Implication definition
  47. Negation definition
  48. Predicate definition
  49. The reals form a field statement
  50. Real sequence definition
  51. Subsequence definition
  52. Infimum definition
  53. Supremum definition
  54. Inner product definition
  55. Linear combination definition
  56. Norm definition
  57. Pascal's rule statement
  58. Complex conjugate definition
  59. Ordered pair definition
  60. Commutative ring definition
  61. Continuity at a point definition
  62. Derivative definition
  63. One-sided limit definition
  64. Biconditional definition
  65. Law of cosines statement
  66. Truth table concept
  67. Addition of natural numbers definition
  68. Modus ponens concept
  69. Universal quantifier definition
  70. The rationals form a field statement
  71. Bounded sequence definition
  72. Cauchy sequence definition
  73. Geometric sequence definition
  74. Limit of a sequence definition
  75. Monotone sequence definition
  76. Proof of the Archimedean property in an Archimedean ordered field proof
  77. Sequence tending to infinity definition
  78. Series definition
  79. The successor function is injective statement
  80. Zero is not a successor statement
  81. Inner product space definition
  82. Linear independence definition
  83. Completeness axiom statement
  84. Cartesian product definition
  85. Proof of the factorial formula for binomial coefficients by induction proof
  86. Continuous function definition
  87. Proof of the equality of complex numbers proof
  88. Differentiable function definition
  89. One-sided derivative definition
  90. Subset definition
  91. Mathematical proof concept
  92. Proof of the commutativity of addition by induction proof
  93. Propositional logic concept
  94. Archimedean property statement
  95. Limit superior definition
  96. Order on the natural numbers definition
  97. Proof of the sum of a finite geometric series proof
  98. Convergent sequence definition
  99. Pointwise convergence definition
  100. Sequential continuity definition
  101. The rationals form an ordered field statement
  102. The sequence r^n tends to infinity for r > 1 example
  103. Partial sum definition
  104. Power series definition
  105. Norm induced by an inner product definition
  106. Equality of complex numbers statement
  107. Binary relation definition
  108. Proof that a composition of continuous functions is continuous proof
  109. Factorial formula for binomial coefficients statement
  110. Tautology definition
  111. Order on the reals definition
  112. Commutativity of addition statement
  113. Sum of a finite geometric series statement
  114. Uniform convergence definition
  115. Proof of strong induction from ordinary induction proof
  116. Radius of convergence definition
  117. Convergent series definition
  118. Sine and cosine definition
  119. Antisymmetric relation definition
  120. Reflexive relation definition
  121. Transitive relation definition
  122. Proof of the binomial theorem by induction proof
  123. Interval definition
  124. Logical equivalence definition
  125. Uniform convergence on a set definition
  126. Strong induction statement
  127. Series of functions definition
  128. Sum of a series definition
  129. Absolute convergence definition
  130. Preorder definition
  131. Binomial theorem statement
  132. Proof of the epsilon-delta form of continuity proof
  133. Proof of the epsilon-delta form of the limit of a function proof
  134. Proof of the well-ordering principle from strong induction proof
  135. Proof of the double negation law by a truth table proof
  136. Partial order definition
  137. Epsilon-delta definition of continuity statement
  138. Epsilon-delta definition of a limit statement
  139. Double negation law statement
  140. Well-ordering principle statement
  141. Total order definition
  142. Composition of continuous functions is continuous statement
  143. Proof by contradiction concept
  144. Proof that every sequence has a monotone subsequence, by peaks proof
  145. Proof that the reals form an ordered field, with the Cauchy sequence construction proof
  146. Every sequence has a monotone subsequence statement
  147. The reals form an ordered field statement
  148. Absolute value definition
  149. Proof of the approximation property of the supremum proof
  150. Proof of the existence of square roots of nonnegative reals proof
  151. Proof of the triangle inequality for real numbers proof
  152. Proof that the absolute value is multiplicative proof
  153. Proof of the epsilon-N definition of the limit of a sequence proof
  154. Existence of square roots of nonnegative reals statement
  155. Approximation property of the supremum statement
  156. Triangle inequality statement
  157. Absolute value is multiplicative statement
  158. Square root definition
  159. Epsilon-N definition of the limit of a sequence statement
  160. Proof that the reals are Archimedean from the completeness axiom proof
  161. Proof of the limit of a sum of sequences proof
  162. Proof of the squeeze theorem for sequences proof
  163. Proof of the uniqueness of limits proof
  164. Proof that limits preserve non-strict inequalities proof
  165. Modulus of a complex number definition
  166. Proof that differentiable functions are continuous proof
  167. Proof that convergent sequences are bounded proof
  168. Proof that convergent sequences are Cauchy proof
  169. Proof that Cauchy sequences are bounded proof
  170. The reals are Archimedean statement
  171. The sequence 1/n tends to zero example
  172. Proof of the term test proof
  173. Proof of the monotone convergence theorem for sequences proof
  174. Proof that a complex number times its conjugate is the square of its modulus proof
  175. Differentiable functions are continuous statement
  176. Limit of a sum of sequences statement
  177. Uniqueness of limits statement
  178. Limits preserve non-strict inequalities statement
  179. Squeeze theorem statement
  180. Convergent sequences are bounded statement
  181. Proof that there is a natural number n with 1/n below any positive epsilon proof
  182. Convergent sequences are Cauchy statement
  183. Cauchy sequences are bounded statement
  184. Monotone convergence theorem for sequences statement
  185. A complex number times its conjugate statement
  186. Proof of the limit of a product of sequences proof
  187. There is a natural number n with 1/n below any positive epsilon statement
  188. Term test statement
  189. Proof that a series of nonnegative terms converges iff its partial sums are bounded proof
  190. The sequence r^n tends to zero for |r| < 1 example
  191. Proof that a decreasing sequence bounded below converges proof
  192. Proof of the sequential characterization of limits proof
  193. Proof that continuity is equivalent to sequential continuity proof
  194. Decreasing sequence bounded below converges statement
  195. Limit of a product of sequences statement
  196. Geometric series example
  197. Proof of the Cauchy–Schwarz inequality proof
  198. A series of nonnegative terms converges iff its partial sums are bounded statement
  199. Continuity is equivalent to sequential continuity statement
  200. Sequential characterization of limits statement
  201. Proof of the root test proof
  202. Proof of the ratio test proof
  203. Proof of the Cauchy–Hadamard theorem proof
  204. Proof of the Bolzano–Weierstrass theorem by a monotone subsequence proof
  205. Proof that exponentials dominate powers in sequences, by the ratio of consecutive terms proof
  206. Proof of the comparison test proof
  207. Cauchy–Schwarz inequality statement
  208. Proof of the chain rule with an auxiliary difference quotient proof
  209. Proof of the product rule proof
  210. Proof of the linearity of differentiation proof
  211. Comparison test statement
  212. Bolzano–Weierstrass theorem statement
  213. Exponentials dominate powers in sequences statement
  214. Chain rule statement
  215. Product rule statement
  216. Linearity of differentiation statement
  217. Ratio test statement
  218. Root test statement
  219. Proof of the boundedness theorem by Bolzano–Weierstrass proof
  220. Proof of the Cauchy criterion for sequences by the Bolzano–Weierstrass theorem proof
  221. Proof of the constant multiple rule proof
  222. Proof of the power rule by induction proof
  223. Boundedness theorem statement
  224. Cauchy–Hadamard theorem statement
  225. Cauchy criterion for sequences statement
  226. Constant multiple rule statement
  227. Power rule statement
  228. Proof of the extreme value theorem by the Bolzano–Weierstrass theorem proof
  229. Uniformly Cauchy sequence of functions definition
  230. Proof of the Cauchy criterion for series proof
  231. Extreme value theorem statement
  232. Proof of the formula for the derivative of a polynomial proof
  233. Proof of Fermat's theorem on stationary points proof
  234. Cauchy criterion for series statement
  235. Derivative of a polynomial statement
  236. Proof that absolutely convergent series converge proof
  237. Fermat's theorem on stationary points statement
  238. Absolutely convergent series converge statement
  239. Proof of Rolle's theorem proof
  240. Rolle's theorem statement
  241. Proof of the Weierstrass M-test proof
  242. Proof of the mean value theorem from Rolle's theorem proof
  243. Weierstrass M-test statement
  244. Mean value theorem statement
  245. Proof that power series converge uniformly on smaller intervals inside the radius of convergence proof
  246. Proof that a function with zero derivative on an open interval is constant proof
  247. Proof that uniform convergence of derivatives allows term-by-term differentiation proof
  248. Power series converge uniformly on smaller discs inside the radius of convergence statement
  249. A function with zero derivative is constant statement
  250. Uniform convergence of derivatives allows term-by-term differentiation statement
  251. Proof of term-by-term differentiation proof
  252. Term-by-term differentiation statement
  253. Proof that power series are differentiable inside the radius of convergence proof
  254. Power series are differentiable inside the radius of convergence statement
  255. Proof of the derivative of cosine by term-by-term differentiation proof
  256. Proof of the derivative of sine by term-by-term differentiation proof
  257. Derivative of cosine statement
  258. Derivative of sine statement
  259. Proof of the Pythagorean trigonometric identity by differentiation proof
  260. Pythagorean trigonometric identity statement
  261. Proof of the law of sines from the law of cosines proof

Where this leads

4 pages build on this one.

Further reading

  1. Web https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Geometry/Euclidean/Triangle.lean, sin_angle_mul_norm_eq_sin_angle_mul_norm
About this page
TagJD65S6DHQA
URIm2://JD65S6DHQA
Kindproof
WritingW0 stub
MSC51M04
ProvesLaw of sines
UsesTriangle, Angle at a point, Collinear points, Euclidean distance, Length of a vector, Dot product, Law of cosines, Linear independence, Cauchy–Schwarz inequality, Sine and cosine, Pythagorean trigonometric identity
Changed4 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • an inventory row: the row of the inventory that the node accounts for (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.