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.
- The vertices of the triangle are not collinear, so they are distinct. Thus , and the three angles are defined.
- We apply the law of cosines with the vertices renamed, so that plays the role of . It gives . So .
- In the same way, and .
- Let . Two differences of squares give .
- A permutation of , , only permutes the four factors in step 4. So step 4 with the letters renamed gives .
- Let and . With the length and the dot product, , and . So .
- Every difference of two vertices lies in the span of and . 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 .
- The sine is nonnegative on , and . By the identity and step 2, . So .
- In the same way, steps 3 and 5 give and . So the three quotients are defined.
- By steps 9 and 10, , and .
- Hence .
Idea
The law of cosines gives each cosine from the sides, and then each sine. All three sines have the same numerator , a symmetric expression in the sides, which is four times the area. Dividing a side by the sine of the opposite angle then gives 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.
- Angle at a point 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
- Triangle concept
- Vector space definition
- Proof of Pascal's rule from the recursive definition proof
- Real and imaginary parts definition
- Set definition
- Ring definition
- Proof of the law of cosines with the dot product proof
- 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
- Complex conjugate definition
- Ordered pair definition
- Commutative ring definition
- Continuity at a point definition
- Derivative definition
- One-sided limit definition
- Biconditional definition
- Law of cosines statement
- Truth table concept
- Addition of natural numbers definition
- Modus ponens concept
- Universal quantifier definition
- The rationals form a field statement
- Bounded sequence definition
- Cauchy sequence definition
- Geometric sequence definition
- Limit of a sequence definition
- Monotone sequence definition
- Proof of the Archimedean property in an Archimedean ordered field proof
- Sequence tending to infinity definition
- Series definition
- 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
- Proof of the factorial formula for binomial coefficients by induction proof
- Continuous function definition
- Proof of the equality of complex numbers proof
- Differentiable function definition
- One-sided derivative definition
- Subset definition
- Mathematical proof concept
- Proof of the commutativity of addition by induction proof
- Propositional logic concept
- Archimedean property statement
- Limit superior definition
- Order on the natural numbers definition
- Proof of the sum of a finite geometric series proof
- Convergent sequence definition
- Pointwise convergence definition
- Sequential continuity definition
- The rationals form an ordered field statement
- The sequence r^n tends to infinity for r > 1 example
- Partial sum definition
- Power series definition
- Norm induced by an inner product definition
- Equality of complex numbers statement
- Binary relation definition
- Proof that a composition of continuous functions is continuous proof
- Factorial formula for binomial coefficients statement
- Tautology definition
- Order on the reals definition
- Commutativity of addition statement
- Sum of a finite geometric series statement
- Uniform convergence definition
- Proof of strong induction from ordinary induction proof
- Radius of convergence definition
- Convergent series definition
- Sine and cosine definition
- Antisymmetric relation definition
- Reflexive relation definition
- Transitive relation definition
- Proof of the binomial theorem by induction proof
- Interval definition
- Logical equivalence definition
- Uniform convergence on a set definition
- Strong induction statement
- Series of functions definition
- Sum of a series definition
- Absolute convergence definition
- Preorder definition
- Binomial theorem statement
- 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
- Proof that the reals form an ordered field, with the Cauchy sequence construction proof
- Every sequence has a monotone subsequence statement
- 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 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
- 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 reals are Archimedean statement
- The sequence 1/n tends to zero example
- 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
- Proof that there is a natural number n with 1/n below any positive epsilon proof
- Convergent sequences are Cauchy statement
- Cauchy sequences are bounded statement
- 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
- Proof that a series of nonnegative terms converges iff its partial sums are bounded proof
- The sequence r^n tends to zero for |r| < 1 example
- 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
- Decreasing sequence bounded below converges statement
- Limit of a product of sequences statement
- Geometric series example
- Proof of the Cauchy–Schwarz inequality proof
- A series of nonnegative terms converges iff its partial sums are bounded statement
- Continuity is equivalent to sequential continuity statement
- Sequential characterization of limits statement
- Proof of the root test 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
- 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
- A function with zero derivative is constant statement
- Uniform convergence of derivatives allows term-by-term differentiation 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 Pythagorean trigonometric identity by differentiation proof
- Pythagorean trigonometric identity statement
- Proof of the law of sines from the law of cosines proof
Where this leads
4 pages build on this one.
Further reading
- 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
| Tag | JD65S6DHQA |
|---|---|
| URI | m2://JD65S6DHQA |
| Kind | proof |
| Writing | W0 stub |
| MSC | 51M04 |
| Proves | Law of sines |
| Uses | Triangle, 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 |
| 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.