avewright/proofwiki-math huggingface dataset:
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\ds \sum_{i \mathop = 1}^n i^3 = {T_n}^2$
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^1 i^3
      | r = 1^3
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \paren {\frac {1 \paren {1 + 1} } 2}^2
      | c = 
}}
{{eqn | r = {T_1}^2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$\ds \sum_{i \mathop = 1}^k i^3 = {T_k}^2$
from which it is to be shown that:
:$\ds \sum_{i \mathop = 1}^{k + 1} i^3 = {T_{k + 1} }^2$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^{k + 1} i^3
      | r = \sum_{i \mathop = 1}^k i^3 + \paren {k + 1}^3
      | c = 
}}
{{eqn | r = {T_k}^2 + \paren {k + 1}^3
      | c = Induction Hypothesis
}}
{{eqn | r = {T_k}^2 + \paren { {T_{k + 1} }^2 - {T_k}^2}
      | c = Cube Number as Difference between Squares of Triangular Numbers
}}
{{eqn | r = {T_{k + 1} }^2
      | c = 
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{> 0}: \ds \sum_{i \mathop = 1}^n i^3 = {T_n}^2$
{{qed}}
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {r - 1} r \paren {r + 1}
      | r = r \paren {r^2 - 1}
      | c = Difference of Two Squares
}}
{{eqn | r = r^3 - r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r^3
      | r = \paren {r - 1} r \paren {r + 1} + r
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{r \mathop = 1}^n r^3
      | r = \sum_{r \mathop = 1}^n \paren {\paren {r - 1} r \paren {r + 1} + r}
      | c = 
}}
{{eqn | r = \sum_{r \mathop = 1}^n \paren {r - 1} r \paren {r + 1} + \sum_{r \mathop = 1}^n r
      | c = 
}}
{{eqn | r = \dfrac {\paren {n - 1} n \paren {n + 1} \paren {n + 2} } 4 + \sum_{r \mathop = 1}^n r
      | c = Sum from $1$ to $n$ of $r \paren {r + 1} \paren {r + 2}$
}}
{{eqn | r = \dfrac {\paren {n - 1} n \paren {n + 1} \paren {n + 2} } 4 + \frac {n \paren {n + 1} } 2
      | c = Closed Form for Triangular Numbers
}}
{{eqn | r = \dfrac {\paren {n - 1} n \paren {n + 1} \paren {n + 2} + 2 n \paren {n + 1} } 4
      | c = common denominator
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {\paren {n - 1} \paren {n + 2} + 2} } 4
      | c = factoring
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {n^2 + n - 2 + 2} } 4
      | c = 
}}
{{eqn | r = \dfrac {n \paren {n + 1} \paren {n \paren {n + 1} } } 4
      | c = 
}}
{{eqn | r = \dfrac {\paren {n \paren {n + 1}^2} } 4
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
First, from Closed Form for Triangular Numbers:
:$\ds \sum_{i \mathop = 1}^n i = \frac {n \paren {n + 1} } 2$
So:
:$\ds \paren {\sum_{i \mathop = 1}^n i}^2 = \dfrac {n^2 \paren {n + 1}^2} 4$
Next we use induction on $n$ to show that:
:$\ds \sum_{i \mathop = 1}^n i^3 = \dfrac {n^2 \paren {n + 1}^2} 4$
The proof proceeds by induction.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\ds \sum_{i \mathop = 1}^n i^3 = \dfrac {n^2 \paren {n + 1}^2} 4$
=== Basis for the Induction ===
$\map P 1$ is the case:
:$1^3 = \dfrac {1 \paren {1 + 1}^2} 4$
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^1 i^3
      | r = 1^3
      | c = 
}}
{{eqn | r = \dfrac {1^2 \paren {1 + 1}^2} 4
      | c = 
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$\ds \sum_{i \mathop = 1}^k i^3 = \dfrac {k^2 \paren {k + 1}^2} 4$
from which it is to be shown that:
:$\ds \sum_{i \mathop = 1}^{k + 1} i^3 = \dfrac {\paren {k + 1}^2 \paren {k + 2}^2} 4$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^{k + 1} i^3
      | r = \sum_{i \mathop = 1}^k i^3 + \paren {k + 1}^3
      | c = 
}}
{{eqn | r = \frac {k^2 \paren {k + 1}^2} 4 + \paren {k + 1}^3
      | c = Induction Hypothesis
}}
{{eqn | r = \frac {k^4 + 2 k^3 + k^2} 4 + \frac {4 k^3 + 12 k^2 + 12 k + 4} 4
      | c = 
}}
{{eqn | r = \frac {k^4 + 6 k^3 + 13 k^2 + 12 k + 4} 4
      | c = 
}}
{{eqn | r = \frac {\paren {k + 1}^2 \paren {k + 2}^2} 4
      | c = 
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{>0}: \ds \sum_{i \mathop = 1}^n i^3 = \dfrac {n^2 \paren {n + 1}^2} 4$
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
By Nicomachus's Theorem, we have:
:$\forall n \in \N_{>0}: n^3 = \paren {n^2 - n + 1} + \paren {n^2 - n + 3} + \ldots + \paren {n^2 + n - 1}$
Also by Nicomachus's Theorem, we have that the first term for $\paren {n + 1}^3$ is $2$ greater than the last term for $n^3$.
So if we add them all up together, we get:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n i^3
      | r = \sum_{\stackrel {1 \mathop \le i \mathop \le n^2 \mathop + n \mathop - 1} {i \text { odd} } } i
      | c = ... the sum of all the odd numbers up to $n^2 + n - 1$
}}
{{eqn | r = \sum_{i \mathop = 1}^{\frac {n^2 \mathop + n} 2} 2 i - 1
      | c = ... that is, the first $\dfrac {n^2 + n} 2$ odd numbers
}}
{{eqn | r = \paren {\frac {n^2 + n} 2}^2
      | c = Odd Number Theorem
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
From Closed Form for Triangular Numbers:
:$(1): \quad \ds \map A n := \sum_{i \mathop = 1}^n i = \frac{n \paren {n + 1} } 2$
From Sum of Sequence of Squares:
:$(2): \quad \ds \map B n := \sum_{i \mathop = 1}^n i^2 = \frac{n \paren {n + 1} \paren {2 n + 1} } 6$
Let $\ds \map S n = \sum_{i \mathop = 1}^n i^3$.
Then:
{{begin-eqn}}
{{eqn | l = \map S n
      | r = n^3 + \paren {n - 1}^3 + \paren {n - 2}^3 + \cdots + 2^3 + 1^3
      | c =
}}
{{eqn | r = \sum_{k \mathop = 0}^{n \mathop - 1} \paren {n - k}^3
      | c =
}}
{{eqn | r = \sum_{k \mathop = 0}^{n \mathop - 1} \paren {n^3 - 3 n^2 k + 3 n k^2 - k^3}
      | c =
}}
{{eqn | r = n^4 - 3 n^2 \cdot \map A {n - 1} + 3 n \cdot \map B {n - 1} - \map S {n - 1}
      | c = 
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \map S n
      | r = n^4 - 3 n^2 \cdot \frac {n \paren {n - 1} } 2 + 3n \cdot \frac{n \paren {n - 1} \paren {2 n - 1} } 6 - \map S {n - 1}
      | c = substituting from $(1)$ and $(2)$
}}
{{eqn | n = 4
      | l = \map S n
      | r = n^3 + \map S {n - 1}
      | c = recursive definition
}}
{{eqn | ll= \leadsto
      | l = 2 \map S n
      | r = n^4 + n^3 - 3 n^2 \cdot \frac {n \paren {n - 1} } 2 + 3 n \cdot \frac {n \paren {n - 1} \paren {2 n - 1} } 6
      | c = adding $(3)$ and $(4)$
}}
{{eqn | ll= \leadsto
      | r = \frac {n^2 \paren {n + 1}^2} 2
      | c = simplification
}}
{{eqn | ll= \leadsto
      | l = \map S n
      | r = \frac {n^2 \paren {n + 1}^2} 4
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
From Faulhaber's Formula:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n i^p
      | r = 1^p + 2^p + \cdots + n^p
      | c = 
}}
{{eqn | r = \frac {n^{p + 1} } {p + 1} + \sum_{k \mathop = 1}^p \frac {B_k \, p^{\underline {k - 1} } \, n^{p - k + 1} } {k!}
      | c = 
}}
{{end-eqn}}
where $B_k$ are the Bernoulli numbers.
Setting $p = 3$:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n i^3
      | r = \frac {n^{3 + 1} } {3 + 1} + \sum_{k \mathop = 1}^3 \frac {B_k \, 3^{\underline {k - 1} } \, n^{3 - k + 1} } {k!}
      | c = 
}}
{{eqn | r = \frac {n^4} 4 + \frac {B_1 \, 3^{\underline 0} \, n^3} {1!} + \frac {B_2 \, 3^{\underline 1} \, n^2} {2!} + \frac {B_3 \, 3^{\underline 2} \, n^1} {3!}
      | c = 
}}
{{eqn | r = \frac {n^4} 4 + \frac 1 2 \frac {n^3} {1!} + \frac 1 6 \frac {3 n^2} {2!} + 0 \frac {3 \times 2 n} {3!}
      | c = {{Defof|Bernoulli Numbers}} and {{Defof|Falling Factorial}}
}}
{{eqn | r = \frac {n^4} 4 + \dfrac {n^3} 2 + \frac {n^2} 4
      | c = simplifying
}}
{{eqn | r = \frac {n^2} 4 \paren {n^2 + 2 n + 1}
      | c = factor out $\dfrac {n^2} 4$
}}
{{eqn | r = \frac {n^2 \paren {n + 1}^2} 4
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
:$\ds \paren {\sum_{i \mathop = 1}^n i}^2 = \paren {1 + 2 + 3 + \cdots + N}^2$
{{begin-eqn}}
{{eqn | l = \paren {1 + 2 + 3 + \cdots + N}^2
      | r = 1 \times \paren {1 + 2 + 3 + \cdots + N}
      | c = 
}}
{{eqn | o = +
      | r = 2 \times \paren {1 + 2 + 3 + \cdots + N}
      | c = 
}}
{{eqn | o = +
      | r = \cdots
      | c = 
}}
{{eqn | o = +
      | r = N \times \paren {1 + 2 + 3 + \cdots + N}
      | c = 
}}
{{end-eqn}}
Organizing the terms above in a square matrix:
:<nowiki>$\begin{array}{r|cccccccccc}
\paren {\ds \sum_{i \mathop = 1}^n i}^2 & 1 & 2 & 3 & 4 & 5 & 6 & \cdots & N \\
\hline
1 & 1 & 2 & 3 & 4 & 5 & 6 & \cdots & N \\
2 & 2 & 4 & 6 & 8 & 10 & 12 & \cdots & 2 N  \\
3 & 3 & 6 & 9 & 12 & 15 & 18 & \cdots & 3 N \\
4 & 4 & 8 & 12 & 16 & 20 & 24 & \cdots & 4 N \\
5 & 5 & 10 & 15 & 20 & 25 & 30 & \cdots & 5 N \\
6 & 6 & 12 & 18 & 24 & 30 & 36 & \cdots & 6 N \\
\vdots  & \vdots & \vdots & \vdots & \vdots & \vdots & \vdots & \ddots & \vdots \\
N  & N & 2 N & 3 N & 4 N & 5 N & 6 N & \cdots & N^2 \\
\end{array}$</nowiki>
From Closed Form for Triangular Numbers:
:$\ds \sum_{i \mathop = 1}^n i = \frac {n \paren {n + 1} } 2$
Therefore:
:$\ds \paren {\sum_{i \mathop = 1}^n i}^2 = \dfrac {n^2 \paren {n + 1}^2} 4$
Next we notice that the sum of the terms in row $N$ with the terms in column $N$ (less $N^2$ so as not to double count) is precisely $N^3$.
{{begin-eqn}}
{{eqn | l = 1^3
      | r = 1
      | c = 
}}
{{eqn | l = 2^3
      | r = 2 + 4 + 2
      | c = 
}}
{{eqn | l = 3^3
      | r = 3 + 6 + 9 + 6 + 3
      | c = 
}}
{{eqn | o = \cdots
}}
{{eqn | l = n^3
      | r = n + 2 n + 3 n + \cdots + \paren {n - 1} \paren n + n^2 + \paren {n - 1} \paren n + \cdots + 2 n + n
      | c = 1+2+...+n+(n-1)+...+1 = n^2
}}
{{end-eqn}}
Therefore:
:$\forall n \in \Z_{>0}: \ds \sum_{i \mathop = 1}^n i^3 = \dfrac {n^2 \paren {n + 1}^2} 4$
{{qed}}
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
{{begin-eqn}}
{{eqn | l = \sin c \sin a \cos B
      | r = \cos b - \cos c \cos a
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos b - \cos c \paren {\cos b \cos c + \sin b \sin c \cos A}
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos b \paren {1 - \cos^2 c} - \sin b \sin c \cos c \cos A
      | c = rearranging
}}
{{eqn | r = \sin^2 c \cos b - \sin b \sin c \cos c \cos A
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin a \cos B
      | r = \sin c \cos b - \sin b \cos c \cos A
      | c = simplifying
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \sin a \sin b \cos C
      | r = \cos c - \cos a \cos b
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos c - \cos b \paren {\cos b \cos c + \sin b \sin c \cos A}
      | c = Spherical Law of Cosines
}}
{{eqn | r = \cos c \paren {1 - \cos^2 b} - \sin b \sin c \cos b \cos A
      | c = rearranging
}}
{{eqn | r = \sin^2 b \cos c - \sin b \sin c \cos b \cos A
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin a \cos C
      | r = \cos b \sin c - \sin c \cos b \cos A
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
:500px
Suppose $c$ is less than $\dfrac \pi 2$.
Let $BA$ be produced to $D$ so that $BD = \dfrac \pi 2$.
Then:
:$AD = \dfrac \pi 2 - c$
and:
:$\angle CAD = pi - A$
Let $C$ and $D$ be joined by an arc of a great circle, denoted $x$.
From the triangle $\sphericalangle DAC$, using the Spherical Law of Cosines:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \map \cos {\dfrac \pi 2 - c} \cos b + \map \sin {\dfrac \pi 2 - c} \sin b \, \map \cos {\pi - A}
      | c = 
}}
{{eqn | r = \sin c \cos b - \cos c \sin b \cos A
      | c = 
}}
{{end-eqn}}
From the triangle $\sphericalangle DBC$, using the Spherical Law of Cosines:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \cos \dfrac \pi 2 \cos a + \sin \pi 2 \sin a \cos B
      | c = 
}}
{{eqn | r = \sin a \cos B
      | c = 
}}
{{end-eqn}}
Hence:
:$\sin a \cos B = \sin c \cos b - \cos c \sin b \cos A$
The case where $c > \dfrac \pi 2$ is worked similarly, but by making $D$ the point between $A$ and $B$ such that $BD$ is $\dfrac \pi 2$.
{{qed}}
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
:500px
Let $A$, $B$ and $C$ be the vertices of a spherical triangle on the surface of a sphere $S$.
By definition of a spherical triangle, $AB$, $BC$ and $AC$ are arcs of great circles on $S$.
By definition of a great circle, the center of each of these great circles is $O$.
Let $O$ be joined to each of $A$, $B$ and $C$.
Let $P$ be an arbitrary point on $OC$.
Construct $PQ$ perpendicular to $OA$ meeting $OA$ at $Q$.
Construct $PR$ perpendicular to $OB$ meeting $OB$ at $R$.
In the plane $OAB$:
:construct $QS$ perpendicular to $OA$
:construct $RS$ perpendicular to $OB$
where $S$ is the point where $QS$ and $RS$ intersect.
Let $OS$ and $PS$ be joined.
Let tangents be constructed at $A$ to the arcs of the great circles $AC$ and $AB$.
These tangents contain the spherical angle $A$.
But by construction, $QS$ and $QP$ are parallel to these tangents.
Hence $\angle PQS = \sphericalangle A$.
Similarly, $\angle PRS = \sphericalangle B$.
Also we have:
{{begin-eqn}}
{{eqn | l = \angle COB
      | r = a
}}
{{eqn | l = \angle COA
      | r = b
}}
{{eqn | l = \angle AOB
      | r = c
}}
{{end-eqn}}
It is to be proved that $PS$ is perpendicular to the plane $AOB$.
By construction, $OQ$ is perpendicular to both $PQ$ and $QS$.
Thus $OQ$ is perpendicular to the plane $PQS$.
Similarly, $OR$ is perpendicular to the plane $PRS$.
Thus $PS$ is perpendicular to both $OQ$ and $OR$.
Thus $PS$ is perpendicular to every line in the plane of $OQ$ and $OR$.
That is, $PS$ is perpendicular to the plane $OAB$.
In particular, $PS$ is perpendicular to $OS$, $SQ$ and $SR$
It follows that $\triangle PQS$ and $\triangle PRS$ are right triangles.
From the right triangles $\triangle OQP$ and $\triangle ORP$, we have:
{{begin-eqn}}
{{eqn | n = 1
      | l = PQ
      | r = OP \sin b
}}
{{eqn | n = 2
      | l = PR
      | r = OP \sin a
}}
{{eqn | n = 3
      | l = OQ
      | r = OP \cos b
}}
{{eqn | n = 4
      | l = OR
      | r = OP \cos a
}}
{{end-eqn}}
Let us denote the angle $\angle SOQ$ by $x$.
Then:
:$\angle ROS = c - x$
From the right triangles $\triangle OSQ$ and $\triangle OSR$, we have:
{{begin-eqn}}
{{eqn | l = QS
      | r = OS \sin x
}}
{{eqn | l = RS
      | r = OS \, \map \sin {c - x}
}}
{{eqn | ll= \leadsto
      | l = RS \sin x
      | r = QS \paren {\sin c \cos x - \cos c \sin x}
      | c = Sine of Difference
}}
{{eqn | ll= \leadsto
      | l = RS
      | r = QS \paren {\sin c \cot x - \cos c}
      | c = dividing both sides by $\sin x$
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = RS
      | r = PR \cos B
}}
{{eqn | r = OP \sin a \cos B
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = QS
      | r = PQ \cos A
}}
{{eqn | r = OP \sin b \cos A
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = QS \cot x
      | r = OQ
}}
{{eqn | r = OP \cos b
}}
{{end-eqn}}
from which it follows that:
:$\sin a \cos B = \cos b \sin c - \sin b \cos c \cos A$
The result follows.
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
Let $\triangle ABC$ be embedded in a Cartesian coordinate system by identifying:
:$C := \tuple {0, 0}$
:$B := \tuple {a, 0}$
:400px
Thus by definition of sine and cosine:
:$A = \tuple {b \cos C, b \sin C}$
By the Distance Formula:
:$c = \sqrt {\paren {b \cos C - a}^2 + \paren {b \sin C - 0}^2}$
Hence:
{{begin-eqn}}
{{eqn | l = c^2
      | r = \paren {b \cos C - a}^2 + \paren {b \sin C - 0}^2
      | c = squaring both sides of Distance Formula
}}
{{eqn | r = b^2 \cos^2 C - 2 a b \cos C + a^2 + b^2 \sin^2 C
      | c = Square of Difference
}}
{{eqn | r = a^2 + b^2 \paren {\sin^2 C + \cos^2 C} - 2 a b \cos C
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = a^2 + b^2 - 2 a b \cos C
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
Let $\triangle ABC$ be a triangle.
=== Case 1: $AC$ greater than $AB$ ===
Using $AC$ as the radius, we construct a circle whose center is $A$.
Now we extend:
:$CB$ to $D$
:$AB$ to $F$
:$BA$ to $G$
:$CA$ to $E$.
$D$ is joined with $E$, thus:
:300px
Using the Intersecting Chords Theorem we have:
:$GB \cdot BF = CB \cdot BD$
$AF$ is a radius, so $AF = AC = b = GA$ and thus:
:$GB = GA + AB = b + c$
:$BF = AF - AB = b - c$
Thus:
{{begin-eqn}}
{{eqn | l = \paren {b + c} \paren {b - c}
      | r = a \cdot BD
}}
{{eqn | ll= \leadsto
      | l = \frac {b^2 - c^2} a 
      | r = BD
}}
{{end-eqn}}
Next:
{{begin-eqn}}
{{eqn | l = CD
      | r = CB + BD
}}
{{eqn | r = a + \frac {b^2 - c^2} a
}}
{{eqn | r = \frac {a^2 + b^2 - c^2} a
}}
{{end-eqn}}
As $CA$ is a radius, $CE$ is a diameter.
By Thales' Theorem, it follows that $\angle CDE$ is a right angle.
Then using the definition of cosine, we have
{{begin-eqn}}
{{eqn | l = \cos C 
      | r = \frac {CD} {CE}
}}
{{eqn | r = \frac {\paren {\dfrac {a^2 + b^2 - c^2} a} } {2 b}
}}
{{eqn | r = \frac {a^2 + b^2 - c^2} {2 a b}
}}
{{eqn | ll= \leadsto
      | l = c^2
      | r = a^2 + b^2 - 2 a b \cos C
}}
{{end-eqn}}
{{qed|lemma}}
=== Case 2: $AC$ less than $AB$ ===
When $AC$ is less than $AB$, the point $B$ lies outside the circle and so the diagram needs to be modified accordingly:
:300px
{{expand|Draw a diagram for the case where $\angle ACB$ is a right angle and where it is a convex angle to show that the formula will be the same.}}
Now we extend:
:$BA$ to $G$
:$CA$ to $E$.
Then we construct:
:$D$ as the point at which $CB$ intersects the circle
:$F$ as the point at which $AB$ intersects the circle.
Finally $D$ is joined to $E$.
Using the Secant Secant Theorem we have:
:$GB \cdot BF = CB \cdot BD$
$AF$ is a radius, so $AF = AC = b = GA$ and thus:
:$GB = GA + AB = b + c$
:$BF = AB - AF = b - c$
Thus:
{{begin-eqn}}
{{eqn | l = \paren {b + c} \paren {b - c}
      | r = CB \cdot BD
      | c = Secant Secant Theorem
}}
{{eqn | l = \paren {b + c} \paren {b - c}
      | r = a \cdot BD
}}
{{eqn | ll= \leadsto
      | l = \frac {b^2 - c^2} a 
      | r = BD
}}
{{end-eqn}}
Next:
{{begin-eqn}}
{{eqn | l = CD
      | r = CB - BD
}}
{{eqn | r = a - \frac {b^2 - c^2} a
}}
{{eqn | r = \frac {a^2 - b^2 + c^2} a
}}
{{end-eqn}}
As $CA$ is a radius, $CE$ is a diameter.
By Thales' Theorem, it follows that $\angle CDE$ is a right angle.
Then using the definition of cosine, we have
{{begin-eqn}}
{{eqn | l = \cos C 
      | r = \frac {CD} {CE}
}}
{{eqn | r = \frac {\paren {\dfrac {a^2 - b^2 + c^2} a} } {2 b}
}}
{{eqn | r = \frac {a^2 - b^2 + c^2} {2 a b}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = c^2
      | r = a^2 + b^2 - 2 a b \cos C
}}
{{end-eqn}}
{{qed|lemma}}
=== Case 3: $AC = AB$ ===
When $AC = AB$ the points $B$, $D$ and $F$ coincide on the circumference of the circle:
:300px
We extend:
:$BA$ to $G$
:$CA$ to $E$
and immediately:
:$GB = CB$
{{finish}}
{{qed}}
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
=== Lemma: Right Triangle ===
{{:Law of Cosines/Right Triangle}}{{qed|lemma}}
=== Acute Triangle ===
{{:Law of Cosines/Proof 3/Acute Triangle}}{{qed|lemma}}
=== Obtuse Triangle ===
{{:Law of Cosines/Proof 3/Obtuse Triangle}}{{qed}}
Theorem: Law of Cosines

Let $\triangle ABC$ be a triangle whose sides $a, b, c$ are such that $a$ is opposite $A$, $b$ is opposite $B$ and $c$ is opposite $C$.
Then:
:$c^2 = a^2 + b^2 - 2 a b \cos C$

Proof:
:500px
Let $A$, $B$ and $C$ be the vertices of a spherical triangle on the surface of a sphere $S$.
By definition of a spherical triangle, $AB$, $BC$ and $AC$ are arcs of great circles on $S$.
By definition of a great circle, the center of each of these great circles is $O$.
Let $AD$ be the tangent to the great circle $AB$.
Let $AE$ be the tangent to the great circle $AC$.
Thus the radius $OA$ of $S$ is perpendicular to $AD$ and $AE$.
By construction, $AD$ lies in the same plane as $AB$.
Thus when $OB$ is produced, it will intersect $AD$ at $D$, say.
Similarly, $OC$ can be produced to intersect $AE$ at $E$, say.
The spherical angle $\sphericalangle BAC$ is defined as the angle between the tangents $AD$ and $AE$.
Thus:
:$\sphericalangle BAC = \angle DAE$
or, denoting that spherical angle $\sphericalangle BAC$ as $A$:
:$A = \angle DAE$
In the (plane) triangle $OAD$, we have that $\angle OAD$ is a right angle.
We also have that $\angle AOD = \angle AOB$ is equal to $c$, by definition of the length of a side of a spherical triangle.
Thus:
{{begin-eqn}}
{{eqn | l = AD
      | r = OA \tan c
      | c = 
}}
{{eqn | l = OD
      | r = OA \sec c
      | c = 
}}
{{end-eqn}}
and by similar analysis of $\triangle OAE$, we have:
{{begin-eqn}}
{{eqn | l = AE
      | r = OA \tan b
      | c = 
}}
{{eqn | l = OE
      | r = OA \sec b
      | c = 
}}
{{end-eqn}}
From consideration of $\triangle DAE$:
{{begin-eqn}}
{{eqn | l = DE^2
      | r = AD^2 + AE^2 - 2 AD \cdot AE \cos \angle DAE
      | c = Law of Cosines
}}
{{eqn | n = 1
      | r = OA^2 \paren {\tan^2 c + \tan^2 b - 2 \tan b \tan c \cos A}
      | c = 
}}
{{end-eqn}}
From consideration of $\triangle DOE$:
{{begin-eqn}}
{{eqn | l = DE^2
      | r = OD^2 + OE^2 - 2 OD \cdot OE \cos \angle DOE
      | c = Law of Cosines
}}
{{eqn | n = 2
      | r = OA^2 \paren {\sec^2 c + \sec^2 b - 2 \sec b \sec c \cos a}
      | c = as $\angle DOE = \angle BOC$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \sec^2 c + \sec^2 b - 2 \sec b \sec c \cos a
      | r = \tan^2 c + \tan^2 b - 2 \tan b \tan c \cos A
      | c = from $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + \tan^2 c} + \paren {1 + \tan^2 b} - 2 \sec b \sec c \cos a
      | r = \tan^2 c + \tan^2 b - 2 \tan b \tan c \cos A
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = 1 - \sec b \sec c \cos a
      | r = \tan b \tan c \cos A
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \cos b \cos c - \cos a
      | r = \sin b \sin c \cos A
      | c = multiplying both sides by $\cos b \cos c$
}}
{{end-eqn}}
and the result follows.
{{qed}}