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 from the side lengths, and then compare with .
- Let , and . Let , and , with the Euclidean distance .
- The vertices of a triangle are not collinear. So they are pairwise distinct, and . Thus the three angles are defined.
- For vectors , the dot product is bilinear and symmetric. So , with the length .
- Let and . Then , and step 3 gives . So .
- By the definition of the angle at , . The same computation at and at gives and .
- Let . By step 4, .
- Every difference of two vertices lies in the span of and ; for example . Since the vertices are not collinear, this span has dimension . So and are linearly independent.
- By the Cauchy–Schwarz inequality and its case of equality, . So . Let .
- Two differences of squares give .
- A permutation of , , only permutes the four factors in step 9. So the computation of step 9 with the letters renamed also gives .
- The sine is nonnegative on , and . By the identity and step 5, . So .
- In the same way, steps 5 and 10 give and . All three sines are positive.
- By the addition formula, .
- We insert in the numerator of step 13. The numerator becomes .
- So , by step 5.
- By the addition formula, .
- The sum in the numerator of step 16 is . So .
- By and , step 12 shows that no angle is or . So , and .
- Suppose that , and let . Then , so .
- By the addition formula and , , . This contradicts step 17. So .
- By the addition formula, . Here we use that the cosine is even.
- Both and lie in , and by steps 15 and 21 they have the same cosine.
- The cosine is injective on , by the uniqueness in the definition of the arccosine. So .
- Hence .
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, has the same cosine and sine as . The sine condition rules out , and on 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.
- Angle at a point concept
- Arccosine concept
- Binomial coefficient definition
- Collinear points concept
- Complex numbers object
- Complex numbers as pairs of reals concept
- Construction of the reals from Cauchy sequences concept
- Definition by recursion concept
- Dot product concept
- Element definition
- Euclidean distance concept
- Factorial definition
- Group concept
- Imaginary unit object
- Inner product concept
- Inner product space concept
- Integers object
- Length of a vector concept
- Limit point of a set definition
- Linear independence concept
- Local maximum definition
- Mathematical induction concept
- Natural numbers object
- Norm induced by an inner product concept
- Ordered field definition
- Peano axioms concept
- Proposition concept
- Rational numbers object
- Real numbers object
- Sequence definition
- Set bounded above definition
- Sine and cosine concept
- Strictly monotone function definition
- Triangle concept
- Vector space definition
- Proof of Pascal's rule from the recursive definition proof
- Real and imaginary parts definition
- Set definition
- Ring definition
- Ring of integers statement
- Limit of a function definition
- Local minimum definition
- Successor function definition
- Archimedean ordered field definition
- Conjunction definition
- Disjunction definition
- Implication definition
- Negation definition
- Predicate definition
- The reals form a field statement
- Real sequence definition
- Subsequence definition
- Infimum definition
- Supremum definition
- Inner product definition
- Linear combination definition
- Norm definition
- Pascal's rule statement
- Ordered pair definition
- Complex conjugate definition
- Commutative ring definition
- Continuity at a point definition
- Derivative definition
- One-sided limit definition
- Biconditional definition
- Truth table concept
- Modus ponens concept
- Addition of natural numbers definition
- Universal quantifier definition
- Bounded sequence definition
- Cauchy sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Sequence tending to infinity definition
- Series definition
- The rationals form a field statement
- Proof of the Archimedean property in an Archimedean ordered field proof
- The successor function is injective statement
- Zero is not a successor statement
- Inner product space definition
- Linear independence definition
- Completeness axiom statement
- Cartesian product definition
- Continuous function definition
- Proof of the factorial formula for binomial coefficients by induction proof
- Proof of the equality of complex numbers proof
- Differentiable function definition
- One-sided derivative definition
- Subset definition
- Mathematical proof concept
- Limit superior definition
- Propositional logic concept
- Proof of the commutativity of addition by induction proof
- Archimedean property statement
- Proof of the sum of a finite geometric series proof
- Convergent sequence definition
- Pointwise convergence definition
- Sequential continuity definition
- The sequence r^n tends to infinity for r > 1 example
- Order on the natural numbers definition
- Cauchy product definition
- Partial sum definition
- Power series definition
- The rationals form an ordered field statement
- Norm induced by an inner product definition
- Equality of complex numbers statement
- Proof that a composition of continuous functions is continuous proof
- Binary relation definition
- Factorial formula for binomial coefficients statement
- Tautology definition
- Sum of a finite geometric series statement
- Order on the reals definition
- Commutativity of addition statement
- Uniform convergence definition
- Radius of convergence definition
- Proof of strong induction from ordinary induction proof
- Convergent series definition
- Sine and cosine definition
- Antisymmetric relation definition
- Proof of the binomial theorem by induction proof
- Reflexive relation definition
- Transitive relation definition
- Interval definition
- Logical equivalence definition
- Uniform convergence on a set definition
- Series of functions definition
- Absolute convergence definition
- Sum of a series definition
- Strong induction statement
- Binomial theorem statement
- Preorder definition
- Proof of the epsilon-delta form of continuity proof
- Proof of the epsilon-delta form of the limit of a function proof
- Proof of the well-ordering principle from strong induction proof
- Proof of the double negation law by a truth table proof
- Partial order definition
- Epsilon-delta definition of continuity statement
- Epsilon-delta definition of a limit statement
- Double negation law statement
- Well-ordering principle statement
- Total order definition
- Composition of continuous functions is continuous statement
- Proof by contradiction concept
- Proof that every sequence has a monotone subsequence, by peaks proof
- Every sequence has a monotone subsequence statement
- Proof that the reals form an ordered field, with the Cauchy sequence construction proof
- The reals form an ordered field statement
- Absolute value definition
- Proof of the approximation property of the supremum proof
- Proof of the existence of square roots of nonnegative reals proof
- Proof of the triangle inequality for real numbers proof
- Proof that the absolute value is multiplicative proof
- Proof of the epsilon-N definition of the limit of a sequence proof
- Existence of square roots of nonnegative reals statement
- Approximation property of the supremum statement
- Triangle inequality statement
- Absolute value is multiplicative statement
- Square root definition
- Epsilon-N definition of the limit of a sequence statement
- Proof of the intermediate value theorem by the supremum proof
- Proof that the reals are Archimedean from the completeness axiom proof
- Proof of the limit of a sum of sequences proof
- Proof of the squeeze theorem for sequences proof
- Proof of the uniqueness of limits proof
- Proof that limits preserve non-strict inequalities proof
- Modulus of a complex number definition
- Intermediate value theorem statement
- Proof that differentiable functions are continuous proof
- Proof that convergent sequences are bounded proof
- Proof that convergent sequences are Cauchy proof
- Proof that Cauchy sequences are bounded proof
- The sequence 1/n tends to zero example
- The reals are Archimedean statement
- Proof of the term test proof
- Proof of the monotone convergence theorem for sequences proof
- Proof that a complex number times its conjugate is the square of its modulus proof
- Differentiable functions are continuous statement
- Limit of a sum of sequences statement
- Uniqueness of limits statement
- Limits preserve non-strict inequalities statement
- Squeeze theorem statement
- Convergent sequences are bounded statement
- Cauchy sequences are bounded statement
- Convergent sequences are Cauchy statement
- Proof that there is a natural number n with 1/n below any positive epsilon proof
- Monotone convergence theorem for sequences statement
- A complex number times its conjugate statement
- Proof of the limit of a product of sequences proof
- There is a natural number n with 1/n below any positive epsilon statement
- Term test statement
- The sequence r^n tends to zero for |r| < 1 example
- Proof that a series of nonnegative terms converges iff its partial sums are bounded proof
- Proof that a decreasing sequence bounded below converges proof
- Proof of the sequential characterization of limits proof
- Proof that continuity is equivalent to sequential continuity proof
- Limit of a product of sequences statement
- Decreasing sequence bounded below converges statement
- Geometric series example
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Proof of the Cauchy–Schwarz inequality proof
- Continuity is equivalent to sequential continuity statement
- Proof of the root test proof
- Sequential characterization of limits statement
- Proof that the Cauchy product of absolutely convergent series converges absolutely to the product proof
- Proof of the ratio test proof
- Proof of the Cauchy–Hadamard theorem proof
- Proof of the Bolzano–Weierstrass theorem by a monotone subsequence proof
- Proof that exponentials dominate powers in sequences, by the ratio of consecutive terms proof
- Proof of the comparison test proof
- Cauchy–Schwarz inequality statement
- Proof of the chain rule with an auxiliary difference quotient proof
- Proof of the product rule proof
- Proof of the linearity of differentiation proof
- Comparison test statement
- Bolzano–Weierstrass theorem statement
- Cauchy product of absolutely convergent series statement
- Exponentials dominate powers in sequences statement
- Chain rule statement
- Product rule statement
- Linearity of differentiation statement
- Ratio test statement
- Root test statement
- Proof of the boundedness theorem by Bolzano–Weierstrass proof
- Proof of the Cauchy criterion for sequences by the Bolzano–Weierstrass theorem proof
- Proof of the constant multiple rule proof
- Proof of the power rule by induction proof
- Boundedness theorem statement
- Cauchy–Hadamard theorem statement
- Cauchy criterion for sequences statement
- Constant multiple rule statement
- Power rule statement
- Proof of the extreme value theorem by the Bolzano–Weierstrass theorem proof
- Uniformly Cauchy sequence of functions definition
- Proof of the Cauchy criterion for series proof
- Extreme value theorem statement
- Proof of the formula for the derivative of a polynomial proof
- Proof of Fermat's theorem on stationary points proof
- Cauchy criterion for series statement
- Derivative of a polynomial statement
- Proof that absolutely convergent series converge proof
- Fermat's theorem on stationary points statement
- Absolutely convergent series converge statement
- Proof of Rolle's theorem proof
- Rolle's theorem statement
- Proof of the Weierstrass M-test proof
- Proof of the mean value theorem from Rolle's theorem proof
- Weierstrass M-test statement
- Mean value theorem statement
- Proof that power series converge uniformly on smaller intervals inside the radius of convergence proof
- Proof that a function with zero derivative on an open interval is constant proof
- Proof that uniform convergence of derivatives allows term-by-term differentiation proof
- Power series converge uniformly on smaller discs inside the radius of convergence statement
- Proof that a function with positive derivative is strictly increasing proof
- A function with zero derivative is constant statement
- Uniform convergence of derivatives allows term-by-term differentiation statement
- A function with positive derivative is strictly increasing statement
- Proof of term-by-term differentiation proof
- Term-by-term differentiation statement
- Proof that power series are differentiable inside the radius of convergence proof
- Power series are differentiable inside the radius of convergence statement
- Proof of the derivative of cosine by term-by-term differentiation proof
- Proof of the derivative of sine by term-by-term differentiation proof
- Derivative of cosine statement
- Derivative of sine statement
- Proof of the angle addition formulas by differentiation proof
- Proof of the Pythagorean trigonometric identity by differentiation proof
- pi object
- Pythagorean trigonometric identity statement
- Angle addition formulas statement
- Proof that cos pi = -1 and sin pi = 0 proof
- cos pi = -1 statement
- Proof of the angle sum of a triangle with sines and cosines proof
Where this leads
6 pages build on this one.
Further reading
- Web https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Geometry/Euclidean/Triangle.lean, angle_add_angle_add_angle_eq_pi
About this page
| Tag | GCHHQHXGCW |
|---|---|
| URI | m2://GCHHQHXGCW |
| Kind | proof |
| Writing | W0 stub |
| MSC | 51M04 |
| Proves | Angle sum of a triangle |
| Uses | Triangle, 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 |
| Changed | 4 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.