Math 2.0

Geometry Proof

Proof of the angle sum of a triangle with sines and cosines

Builds on TriangleAngle at a pointCollinear pointsEuclidean distanceLength of a vectorDot productLinear independenceCauchy–Schwarz inequalitySine and cosinePythagorean trigonometric identityAngle addition formulascos pi = -1Arccosine

Proof

We compute the cosine and the sine of α+β\alpha + \beta from the side lengths, and then compare with π−γ\pi - \gamma.

  1. Let α=∠BAC\alpha = \angle BAC, β=∠CBA\beta = \angle CBA and γ=∠ACB\gamma = \angle ACB. Let a=d(B,C)a = d(B, C), b=d(C,A)b = d(C, A) and c=d(A,B)c = d(A, B), with the Euclidean distance dd.
  2. The vertices of a triangle are not collinear. So they are pairwise distinct, and a,b,c>0a, b, c > 0. Thus the three angles are defined.
  3. For vectors x,y∈ℝnx, y \in \R^n, the dot product is bilinear and symmetric. So ∥x−y∥2=∥x∥2−2 x⋅y+∥y∥2\norm{x - y}^2 = \norm{x}^2 - 2 \, x \cdot y + \norm{y}^2, with the length ∥⋅∥\norm{\cdot}.
  4. Let x=B−Ax = B - A and y=C−Ay = C - A. Then x−y=B−Cx - y = B - C, and step 3 gives a2=c2−2 x⋅y+b2a^2 = c^2 - 2 \, x \cdot y + b^2. So x⋅y=12(b2+c2−a2)x \cdot y = \frac{1}{2}(b^2 + c^2 - a^2).
  5. By the definition of the angle at AA, cos⁡α=x⋅ybc=b2+c2−a22bc\cos \alpha = \dfrac{x \cdot y}{bc} = \dfrac{b^2 + c^2 - a^2}{2bc}. The same computation at BB and at CC gives 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}.
  6. Let Q=4b2c2−(b2+c2−a2)2Q = 4b^2c^2 - (b^2 + c^2 - a^2)^2. By step 4, 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; for example C−B=y−xC - B = y - x. 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. 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).
  10. A permutation of aa, bb, cc only permutes the four factors in step 9. So the computation of step 9 with the letters renamed also 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.
  11. 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 5, sin⁡2α=1−cos⁡2α=Q4b2c2\sin^2 \alpha = 1 - \cos^2 \alpha = \dfrac{Q}{4b^2c^2}. So sin⁡α=R2bc\sin \alpha = \dfrac{R}{2bc}.
  12. In the same way, steps 5 and 10 give sin⁡β=R2ca\sin \beta = \dfrac{R}{2ca} and sin⁡γ=R2ab\sin \gamma = \dfrac{R}{2ab}. All three sines are positive.
  13. By the addition formula, cos⁡(α+β)=cos⁡αcos⁡β−sin⁡αsin⁡β=(b2+c2−a2)(c2+a2−b2)−Q4abc2\cos(\alpha + \beta) = \cos \alpha \cos \beta - \sin \alpha \sin \beta = \dfrac{(b^2 + c^2 - a^2)(c^2 + a^2 - b^2) - Q}{4abc^2}.
  14. We insert Q=4b2c2−(b2+c2−a2)2Q = 4b^2c^2 - (b^2 + c^2 - a^2)^2 in the numerator of step 13. The numerator becomes (b2+c2−a2)⋅2c2−4b2c2=2c2(c2−a2−b2)(b^2 + c^2 - a^2) \cdot 2c^2 - 4b^2c^2 = 2c^2 (c^2 - a^2 - b^2).
  15. So cos⁡(α+β)=c2−a2−b22ab=−cos⁡γ\cos(\alpha + \beta) = \dfrac{c^2 - a^2 - b^2}{2ab} = -\cos \gamma, by step 5.
  16. By the addition formula, sin⁡(α+β)=sin⁡αcos⁡β+cos⁡αsin⁡β=R((c2+a2−b2)+(b2+c2−a2))4abc2\sin(\alpha + \beta) = \sin \alpha \cos \beta + \cos \alpha \sin \beta = \dfrac{R \left( (c^2 + a^2 - b^2) + (b^2 + c^2 - a^2) \right)}{4abc^2}.
  17. The sum in the numerator of step 16 is 2c22c^2. So sin⁡(α+β)=R2ab=sin⁡γ>0\sin(\alpha + \beta) = \dfrac{R}{2ab} = \sin \gamma > 0.
  18. By sin⁡π=0\sin \pi = 0 and sin⁡0=0\sin 0 = 0, step 12 shows that no angle is 00 or π\pi. So α,β∈(0,π)\alpha, \beta \in (0, \pi), and 0<α+β<2π0 < \alpha + \beta < 2\pi.
  19. Suppose that α+β>π\alpha + \beta > \pi, and let z=α+β−πz = \alpha + \beta - \pi. Then z∈(0,π)z \in (0, \pi), so sin⁡z≥0\sin z \geq 0.
  20. By the addition formula and cos⁡π=−1\cos \pi = -1, sin⁡π=0\sin \pi = 0, sin⁡(α+β)=sin⁡(z+π)=−sin⁡z≤0\sin(\alpha + \beta) = \sin(z + \pi) = -\sin z \leq 0. This contradicts step 17. So α+β≤π\alpha + \beta \leq \pi.
  21. By the addition formula, cos⁡(π−γ)=cos⁡πcos⁡(−γ)−sin⁡πsin⁡(−γ)=−cos⁡γ\cos(\pi - \gamma) = \cos \pi \cos(-\gamma) - \sin \pi \sin(-\gamma) = -\cos \gamma. Here we use that the cosine is even.
  22. Both α+β\alpha + \beta and π−γ\pi - \gamma lie in [0,π][0, \pi], and by steps 15 and 21 they have the same cosine.
  23. The cosine is injective on [0,π][0, \pi], by the uniqueness in the definition of the arccosine. So α+β=π−γ\alpha + \beta = \pi - \gamma.
  24. Hence ∠BAC+∠CBA+∠ACB=π\angle BAC + \angle CBA + \angle ACB = \pi.

Idea

The law of cosines gives the cosine of each angle from the three sides, and then the sine as well. With the addition formulas, α+β\alpha + \beta has the same cosine and sine as π−γ\pi - \gamma. The sine condition rules out α+β>π\alpha + \beta > \pi, and on [0,π][0, \pi] the cosine determines the angle.

Reading path

To understand this page from the ground up, read these 273 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 that cos pi = -1 and sin pi = 0, 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 angle addition formulas by 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 that a function with positive derivative is strictly increasing, Proof of the intermediate value theorem by the supremum, 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 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 that the Cauchy product of absolutely convergent series converges absolutely to the product, Proof of the constant multiple rule.

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

Where this leads

6 pages build on this one.

Further reading

  1. Web https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Geometry/Euclidean/Triangle.lean, angle_add_angle_add_angle_eq_pi
About this page
TagGCHHQHXGCW
URIm2://GCHHQHXGCW
Kindproof
WritingW0 stub
MSC51M04
ProvesAngle sum of a triangle
UsesTriangle, Angle at a point, Collinear points, Euclidean distance, Length of a vector, Dot product, Linear independence, Cauchy–Schwarz inequality, Sine and cosine, Pythagorean trigonometric identity, Angle addition formulas, cos pi = -1, Arccosine
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.