avewright/proofwiki-math huggingface dataset:
Theorem: Power Reduction Formulas/Cosine to 4th

:$\cos^4 x = \dfrac {3 + 4 \cos 2 x + \cos 4 x} 8$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^4 x
      | r = \paren {\cos^2 x}^2
}}
{{eqn | r = \paren {\frac {1 + \cos 2 x} 2}^2
      | c = Square of Cosine
}}
{{eqn | r = \frac {1 + 2 \cos 2 x + \cos^2 2 x} 4
      | c = multiplying out
}}
{{eqn | r = \frac {1 + 2 \cos 2 x + \frac {1 + \cos 4 x} 2} 4
      | c = Square of Cosine
}}
{{eqn | r = \frac {2 + 4 \cos 2 x + 1 + \cos 4 x} 8
      | c = multiplying top and bottom by $2$
}}
{{eqn | r = \frac {3 + 4 \cos 2 x + \cos 4 x} 8
      | c = rearrangement
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Cosine to 4th

:$\cos^4 x = \dfrac {3 + 4 \cos 2 x + \cos 4 x} 8$

Proof:
{{begin-eqn}}
{{eqn | l = \cos ^4 x
      | r = \paren {\frac {e^{i x} + e^{-i x} } 2}^4
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac {\paren {e^{i x} + e^{-i x} }^4} {16}
      | c = rearranging
}}
{{eqn | r = \frac {\paren {e^{i x} }^4 + 4 \paren {e^{i x} }^3 \paren {e^{-i x} } + 6 \paren {e^{i x} }^2 \paren {e^{-i x} }^2 + 4 \paren {e^{i x} } \paren {e^{-i x} }^3 + \paren {e^{-i x} }^4} {16}
      | c = multiplying out
}}
{{eqn | r = \frac {e^{4 i x} + 4 e^{2 i x} + 6 + 4 e^{-2 i x} + e^{-4 i x} } {16}
      | c = multiplying out
}}
{{eqn | r = \frac {3 + 4 \paren {\dfrac {e^{2 i x} + e^{-2 i x} } 2} + \paren {\dfrac {e^{4 i x} + e^{-4 i x} } 2} } 8
      | c = gathering terms
}}
{{eqn | r = \frac {3 + 4 \cos 2 x + \cos 4 x} 8
      | c = Euler's Cosine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Sine to 5th

:$\sin^5 x = \dfrac {10 \sin x - 5 \sin 3 x + \sin 5 x} {16}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin 5 x
      | r = 5 \sin x - 20 \sin^3 x + 16 \sin^5 x
      | c = Quintuple Angle Formula for Sine
}}
{{eqn | ll= \leadsto
      | l = 16 \sin^5 x
      | r = \sin 5 x + 20 \sin^3 x - 5 \sin x
      | c = rearranging
}}
{{eqn | r = \sin 5 x + 20 \paren {\frac {3 \sin x - \sin 3 x} 4} - 5 \sin x
      | c = Power Reduction Formula for Cube of Sine
}}
{{eqn | r = \sin 5 x + 15 \sin x - 5 \sin 3 x - 5 \sin x
      | c = multipying out
}}
{{eqn | r = 10 \sin x - 5 \sin 3 x + \sin 5 x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \sin^5 x
      | r = \frac {10 \sin x - 5 \sin 3 x + \sin 5 x} {16}
      | c = dividing both sides by 16
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Cosine to 5th

:$\cos^5 x = \dfrac {10 \cos x + 5 \cos 3 x + \cos 5 x} {16}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 5 x
      | r = 16 \cos^5 x - 20 \cos^3 x + 5 \cos x
      | c = Quintuple Angle Formula for Cosine
}}
{{eqn | ll= \leadsto
      | l = 16 \cos^5 x
      | r = \cos 5 x + 20 \cos^3 x - 5 \cos x
      | c = rearranging
}}
{{eqn | r = \cos 5 x + 20 \paren {\frac {3 \cos x + \cos 3 x} 4} - 5 \cos x
      | c = Cube of Cosine
}}
{{eqn | r = \cos 5 x + 15 \cos x + 5 \cos 3 x - 5 \cos x
      | c = multiplying out
}}
{{eqn | r = 10 \cos x + 5 \cos 3 x + \cos 5 x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \cos^5 x
      | r = \frac {10 \cos x + 5 \cos 3 x + \cos 5 x} {16}
      | c = dividing both sides by $16$
}}
{{end-eqn}}
{{qed}}
Theorem: Orthocomplement of Subset of Orthocomplement is Superset

Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space.
Let $A, B \subseteq V$ be subsets of $V$ such that $B \subseteq A^\perp$, where $A^\perp$ is the orthocomplement of $A$.
Then: 
:$A \subseteq B^\perp$.

Proof:
Let $B \subseteq A^\perp$.
Then by Orthocomplement Reverses Subset:
:$A^{\perp\perp} \subseteq B^\perp$
By Double Orthocomplement is Closed Linear Span and the definition of closed linear span:
:$A \subseteq A^{\perp\perp}$
Hence, by Subset Relation is Transitive:
:$A \subseteq B^\perp$
{{qed}}
Category:Inner Product Spaces
Category:Orthocomplements
nbacrxpur2zbxjmd77cczkttzjppugm
Theorem: Werner Formulas/Cosine by Cosine

:$\cos \alpha \cos \beta = \dfrac {\map \cos {\alpha - \beta} + \map \cos {\alpha + \beta} } 2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \frac {\map \cos {\alpha - \beta} + \map \cos {\alpha + \beta} } 2
}}
{{eqn | r = \frac {\paren {\cos \alpha \cos \beta + \sin \alpha \sin \beta} + \paren {\cos \alpha \cos \beta - \sin \alpha \sin \beta} } 2
      | c = Cosine of Difference and Cosine of Sum
}}
{{eqn | r = \frac {2 \cos \alpha \cos \beta} 2
}}
{{eqn | r = \cos \alpha \cos \beta
}}
{{end-eqn}}
{{qed}}
Theorem: Werner Formulas/Sine by Sine

:$\sin \alpha \sin \beta = \dfrac {\map \cos {\alpha - \beta} - \map \cos {\alpha + \beta} } 2$

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = \frac {\map \cos {\alpha - \beta} - \map \cos {\alpha + \beta} } 2
}}
{{eqn | r = \frac {\paren {\cos \alpha \cos \beta + \sin \alpha \sin \beta} - \paren {\cos \alpha \cos \beta - \sin \alpha \sin \beta} } 2
      | c = Cosine of Difference and Cosine of Sum
}}
{{eqn | r = \frac {2 \sin \alpha \sin \beta} 2
}}
{{eqn | r = \sin \alpha \sin \beta
}}
{{end-eqn}}
{{qed}}
Theorem: Werner Formulas/Cosine by Sine

:$\cos \alpha \sin \beta = \dfrac {\map \sin {\alpha + \beta} - \map \sin {\alpha - \beta} } 2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \frac {\map \sin {\alpha + \beta} - \map \sin {\alpha - \beta} } 2
}}
{{eqn | r = \frac {\paren {\sin \alpha \cos \beta + \cos \alpha \sin \beta} - \paren {\sin \alpha \cos \beta - \cos \alpha \sin \beta} } 2
      | c = Sine of Sum and Sine of Difference
}}
{{eqn | r = \frac {2 \cos \alpha \sin \beta} 2
}}
{{eqn | r = \cos \alpha \sin \beta
}}
{{end-eqn}}
{{qed}}
Theorem: Werner Formulas/Cosine by Sine

:$\cos \alpha \sin \beta = \dfrac {\map \sin {\alpha + \beta} - \map \sin {\alpha - \beta} } 2$

Proof:
{{begin-eqn}}
{{eqn | l = \cos \alpha \sin \beta
      | r = \sin \beta \cos \alpha
}}
{{eqn | r = \frac {\map \sin {\beta + \alpha} + \map \sin {\beta - \alpha} } 2
      | c = Werner Formula for Sine by Cosine
}}
{{eqn | r = \frac {\map \sin {\alpha + \beta} + \map \sin {-\paren {\alpha - \beta} } } 2
      | c = 
}}
{{eqn | r = \frac {\map \sin {\alpha + \beta} - \map \sin {\alpha - \beta} } 2
      | c = Sine Function is Odd
}}
{{end-eqn}}
{{qed}}
Theorem: Werner Formulas/Sine by Cosine

:$\sin \alpha \cos \beta = \dfrac {\map \sin {\alpha + \beta} + \map \sin {\alpha - \beta} } 2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \frac {\sin \paren {\alpha + \beta} + \sin \paren {\alpha - \beta} } 2
}}
{{eqn | r = \frac {\paren {\sin \alpha \cos \beta + \cos \alpha \sin \beta} + \paren {\sin \alpha \cos \beta - \cos \alpha \sin \beta} } 2
      | c = Sine of Sum and Sine of Difference
}}
{{eqn | r = \frac {2 \sin \alpha \cos \beta} 2
}}
{{eqn | r = \sin \alpha \cos \beta
}}
{{end-eqn}}
{{qed}}
Theorem: Werner Formulas/Sine by Cosine

:$\sin \alpha \cos \beta = \dfrac {\map \sin {\alpha + \beta} + \map \sin {\alpha - \beta} } 2$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 2 \sin \alpha \cos \beta
}}
{{eqn | r = 2 \paren {\dfrac {\map \exp {i \alpha} - \map \exp {-i \alpha} } {2 i} } \paren {\dfrac {\map \exp {i \beta} + \map \exp {-i \beta} } 2}
      | c = Euler's Sine Identity and Euler's Cosine Identity
}}
{{eqn | r = \frac 1 {2 i} \paren {\map \exp {i \alpha} - \map \exp {-i \alpha} } \paren {\map \exp {i \beta} + \map \exp {-i \beta} }
}}
{{eqn | r = \frac 1 {2 i} \paren {\map \exp {i \paren {\alpha + \beta} } - \map \exp {-i \paren {\alpha + \beta} } + \map \exp {i \paren {\alpha - \beta} } - \map \exp {-i \paren {\alpha - \beta} } }
}}
{{eqn | r = \frac {\map \exp {i \paren {\alpha + \beta} } - \map \exp {-i \paren {\alpha + \beta} } } {2 i} + \frac {\map \exp {i \paren {\alpha - \beta} } - \map \exp {-i \paren {\alpha - \beta} } } {2 i}
}}
{{eqn | r = \map \sin {\alpha + \beta} + \map \sin {\alpha - \beta}
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Integer Multiple of Argument/Formulation 1

{{begin-eqn}}
{{eqn | l = \sin n \theta
      | r = \sin \theta \paren {\paren {2 \cos \theta}^{n - 1} - \dbinom {n - 2} 1 \paren {2 \cos \theta}^{n - 3} + \dbinom {n - 3} 2 \paren {2 \cos \theta}^{n - 5} - \cdots}
      | c = 
}}
{{eqn | r = \sin \theta \paren {\sum_{k \mathop \ge 0} \paren {-1}^k \binom {n - \paren {k + 1} } k \paren {2 \cos \theta}^{n - \paren {2 k + 1} } }
      | c = 
}}
{{end-eqn}}

Proof:
The proof proceeds by induction.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\ds \sin n \theta = \sin \theta \paren {\sum_{k \mathop \ge 0} \paren {-1}^k \binom {n - \paren {k + 1} } k \paren {2 \cos \theta}^{n - \paren {2 k + 1} } }$
Theorem: Cosine to Power of Odd Integer

:$\ds \cos^{2 n + 1} \theta = \frac 1 {2^{2 n} } \sum_{k \mathop = 0}^n \binom {2 n + 1} k \cos \paren {2 n - 2 k + 1} \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^{2 n + 1} \theta
      | r = \paren {\frac {e^{i \theta} + e^{-i \theta} } 2}^{2 n + 1}
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac 1 {2^{2 n + 1} } \paren {e^{i \theta} + e^{-i \theta} }^{2 n + 1}
      | c = Power of Product
}}
{{eqn | r = \frac 1 {2^{2 n + 1} } \sum^{2 n + 1}_{k \mathop = 0} \binom {2 n + 1} k e^{k i \theta} e^{-\paren {2 n - k + 1} i \theta}
      | c = Binomial Theorem
}}
{{eqn | r = \frac 1 {2^{2 n + 1} } \sum^{2 n + 1}_{k \mathop = 0} \binom {2 n + 1} k e^{-\paren {2 n - 2 k + 1} i \theta}
      | c = Exponential of Sum
}}
{{eqn | r = \frac 1 {2^{2 n + 1} } \paren {\sum^n_{k \mathop = 0} \binom {2 n + 1} k e^{-\paren {2 n - 2 k + 1} i \theta} + \sum^{2 n + 1}_{k \mathop = n + 1} \binom {2 n + 1} k e^{-\paren {2 n - 2 k + 1} i \theta} }
      | c = partitioning the sum
}}
{{eqn | r = \frac 1 {2^{2 n + 1} } \paren {\sum^n_{k \mathop = 0} \binom {2 n + 1} k e^{-\paren {2 n - 2 k + 1} i \theta} + \sum^n_{k \mathop = 0} \binom {2 n + 1} {2 n + 1 - k} e^{\paren {2 \paren {2 n - k + 1} - 2 n - 1} i \theta} }
      | c = $k \mapsto 2 n + 1 - k$
}}
{{eqn | r = \frac 1 {2^{2 n + 1} } \paren {\sum^n_{k \mathop = 0} \binom {2 n + 1} k e^{-\paren {2 n - 2 k + 1} i \theta} + \sum^n_{k \mathop = 0} \binom {2 n + 1} k e^{\paren {2 n - 2 k + 1} i \theta} }
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \frac 1 {2^{2 n} } \sum^n_{k \mathop = 0} \binom {2 n + 1} k \map \cos {2 n - 2 k + 1} \theta
      | c = Euler's Cosine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine to Power of Odd Integer

:$\ds \cos^{2 n + 1} \theta = \frac 1 {2^{2 n} } \sum_{k \mathop = 0}^n \binom {2 n + 1} k \cos \paren {2 n - 2 k + 1} \theta$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^n \theta
      | r = \paren {\frac {e^{i \theta} + e^{-i \theta} } 2}^n
      | c = De Moivre's Theorem
}}
{{eqn | r = \frac {\paren {e^{i \theta} + e^{-i \theta} }^n} {2^n}
      | c = 
}}
{{eqn | r = \frac 1 {2^n} \sum_{k \mathop = 0}^n \binom n k e^{\paren {n - k} i \theta} e^{-k i \theta}
      | c = Binomial Theorem
}}
{{eqn | r = \frac 1 {2^n} \sum_{k \mathop = 0}^n \binom n k e^{\paren {n - 2 k} i \theta}
      | c = 
}}
{{end-eqn}}
Matching up terms from the beginning of this expansion with those from the end:
{{begin-eqn}}
{{eqn | l = 2^n \cos^n \theta
      | r = e^{n i \theta} + \binom n 1 e^{\paren {n - 2} i \theta} + \binom n 2 e^{\paren {n - 4} i \theta} + \cdots
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \binom n {n - 2} e^{-\paren {n - 4} i \theta} + \binom n {n - 1} e^{-\paren {n - 2} i \theta} + e^{-n i \theta}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {2 n} 2 \cos^n \theta
      | r = \paren {\frac {e^{n i \theta} + e^{-n i \theta} } 2} + \binom n 1 \paren {\frac {e^{\paren {n - 2} i \theta} + e^{-\paren {n - 2} i \theta} } 2}
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \binom n 2 \paren {\frac {e^{\paren {n - 4} i \theta} + e^{-\paren {n - 4} i \theta} } 2} + \cdots
      | c = 
}}
{{end-eqn}}
Thus:
:$\cos^n \theta = \dfrac 1 {2^{n - 1} } \paren {\cos n \theta + n \cos \paren {n - 2} \theta + \dfrac {n \paren {n - 1} } {2!} \cos \paren {n - 4} \theta + \cdots + R_n}$
Now to determine $R_n$.
The middle two terms of the sequence $0, 1, \ldots, n$ are $\dfrac {n - 1} 2$ and $\dfrac {n + 1} 2$.
Thus, when $k = \dfrac {n - 1} 2$:
{{begin-eqn}}
{{eqn | l = n - 2 k
      | r = n - 2 \frac {n - 1} 2
      | c = 
}}
{{eqn | r = n - \frac {2 n - 2} 2
      | c = 
}}
{{eqn | r = n - n + 1
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
Similarly, when $k = \dfrac {n + 1} 2$:
{{begin-eqn}}
{{eqn | l = n + 2 k
      | r = n - 2 \frac {n + 1} 2
      | c = 
}}
{{eqn | r = n - \frac {2 n + 2} 2
      | c = 
}}
{{eqn | r = n - n - 1
      | c = 
}}
{{eqn | r = -1
      | c = 
}}
{{end-eqn}}
The binomial coefficient in each case is the same, because:
{{begin-eqn}}
{{eqn | l = n - \frac {n - 1} 2
      | r = \frac {2 n - n - 1} 2
      | c = 
}}
{{eqn | r = \frac {n + 1} 2
      | c = 
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \binom n {\paren {n - 1} / 2}
      | r = \frac {n!} {\paren {\frac {n - 1} 2}! \paren {\frac {n + 1} 2}!}
      | c = 
}}
{{eqn | r = \binom n {\paren {n + 1} / 2}
      | c = 
}}
{{end-eqn}}
Thus the two middle terms collapse to:
{{begin-eqn}}
{{eqn | l = R_n
      | r = \frac {n!} {\paren {\frac {n - 1} 2}! \paren {\frac {n + 1} 2}!} \paren {\frac {e^{i \theta} + e^{-i \theta} } 2}
      | c = 
}}
{{eqn | r = \frac {n!} {\paren {\frac {n - 1} 2}! \paren {\frac {n + 1} 2}!} \cos \theta
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Arctangent and Arccotangent

Let $x \in \R$ be a real number.
Then:
:$\arctan x + \arccot x = \dfrac \pi 2$
where $\arctan$ and $\arccot$ denote arctangent and arccotangent respectively.

Proof:
Let $y \in \R$ such that:
:$\exists x \in \R: x = \map \cot {y + \dfrac \pi 2}$
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \map \cot {y + \frac \pi 2}
      | c = 
}}
{{eqn | r = -\tan y
      | c = Cotangent of Angle plus Right Angle
}}
{{eqn | r = \map \tan {-y}
      | c = Tangent Function is Odd
}}
{{end-eqn}}
Suppose $-\dfrac \pi 2 \le y \le \dfrac \pi 2$.
Then we can write:
:$-y = \arctan x$
But then:
:$\map \cot {y + \dfrac \pi 2} = x$
Now because $-\dfrac \pi 2 \le y \le \dfrac \pi 2$ it follows that:
:$0 \le y + \dfrac \pi 2 \le \pi$
Hence:
:$y + \dfrac \pi 2 = \arccot x$
That is:
:$\dfrac \pi 2 = \arccot x + \arctan x$
{{qed}}
Theorem: Arcsine of Reciprocal equals Arccosecant

:$\map \arcsin {\dfrac 1 x} = \arccsc x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arcsin {\frac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 x
      | r = \sin y
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \csc y
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | ll= \leadstoandfrom
      | l = \arccsc x
      | r = y
      | c = {{Defof|Real Arccosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Arccosine of Reciprocal equals Arcsecant

:$\map \arccos {\dfrac 1 x} = \arcsec x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arccos {\frac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 x
      | r = \cos y
      | c = {{Defof|Real Arccosine}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \sec y
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | ll= \leadstoandfrom
      | l = \arcsec x
      | r = y
      | c = {{Defof|Real Arcsecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Arctangent of Reciprocal equals Arccotangent

:$\map \arctan {\dfrac 1 x} = \arccot x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arctan {\frac 1 x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 x
      | r = \tan y
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \cot y
      | c = Cotangent is Reciprocal of Tangent
}}
{{eqn | ll= \leadstoandfrom
      | l = \arccot x
      | r = y
      | c = {{Defof|Real Arccotangent}}
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Sine is Odd Function

Everywhere that the function is defined:
:$\map \arcsin {-x} = -\arcsin x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arcsin {-x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -x
      | r = \sin y:
      | rr = -\frac \pi 2 \le y \le \frac \pi 2
      | c = {{Defof|Real Arcsine}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = -\sin y:
      | rr = -\frac \pi 2 \le y \le \frac \pi 2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \map \sin {-y}:
      | rr = -\frac \pi 2 \le y \le \frac \pi 2
      | c = Sine Function is Odd
}}
{{eqn | ll= \leadstoandfrom
      | l = \arcsin x
      | r = -y
      | c = {{Defof|Real Arcsine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Arccosine of Negative Argument

Everywhere that the function is defined:
:$\map \arccos {-x} = \pi - \arccos x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arccos {-x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -x
      | r = \cos y:
      | rr= 0 \le y \le \pi
      | c = {{Defof|Real Arccosine}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = -\cos y:
      | rr= -\pi \le y \le 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \map \cos {\pi - y}:
      | rr= 0 \le y \le \pi
      | c = Cosine of Supplementary Angle
}}
{{eqn | ll= \leadstoandfrom
      | l = \arccos x
      | r = \pi - y
      | c = {{Defof|Real Arccosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Tangent is Odd Function

Everywhere that the function is defined:
:$\map \arctan {-x} = -\arctan x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arctan {-x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -x
      | r = \tan y:
      | rr= -\frac \pi 2 \le y \le \frac \pi 2
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = -\tan y:
      | rr= -\frac \pi 2 \le y \le \frac \pi 2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \map \tan {-y}:
      | rr= -\frac \pi 2 \le y \le \frac \pi 2
      | c = Tangent Function is Odd
}}
{{eqn | ll= \leadstoandfrom
      | l = \arctan x
      | r = -y
      | c = {{Defof|Real Arctangent}}
}}
{{end-eqn}}
{{qed}}
Theorem: Arccotangent of Negative Argument

Everywhere that the function is defined:
:$\map \arccot {-x} = \pi - \arccot x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arccot {-x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -x
      | r = \cot y:
      | rr= 0 \le y \le \pi
      | c = {{Defof|Arccotangent}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = -\cot y:
      | rr= -\pi \le y \le 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \map \cot {\pi - y}:
      | rr= 0 \le y \le \pi
      | c = Cotangent of Supplementary Angle
}}
{{eqn | ll= \leadstoandfrom
      | l = \arccot x
      | r = \pi - y
      | c = {{Defof|Arccotangent}}
}}
{{end-eqn}}
{{qed}}
Theorem: Arcsecant of Negative Argument

Everywhere that the function is defined:
:$\map \arcsec {-x} = \pi - \arcsec x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arcsec {-x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -x
      | r = \sec y:
      | rr= 0 \le y \le \pi
      | c = {{Defof|Arcsecant}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = -\sec y:
      | rr= -\pi \le y \le 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \map \sec {\pi - y}:
      | rr= 0 \le y \le \pi
      | c = Cosecant of Supplementary Angle
}}
{{eqn | ll= \leadstoandfrom
      | l = \arcsec x
      | r = \pi - y
      | c = {{Defof|Arcsecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Inverse Cosecant is Odd Function

Everywhere that the function is defined:
:$\map \arccsc {-x} = -\arccsc x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arccsc {-x}
      | r = y
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = -x
      | r = \csc y:
      | rr= -\frac \pi 2 \le y \le \frac \pi 2
      | c = {{Defof|Arccosecant}}
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = -\csc y:
      | rr= -\frac \pi 2 \le y \le \frac \pi 2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | r = \map \csc {-y}:
      | rr= -\frac \pi 2 \le y \le \frac \pi 2
      | c = Cosecant Function is Odd
}}
{{eqn | ll= \leadstoandfrom
      | l = \arccsc x
      | r = -y
      | c = {{Defof|Arccosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Law of Tangents

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:
:$\dfrac {a + b} {a - b} = \dfrac {\tan \frac 1 2 \paren {A + B} } {\tan \frac 1 2 \paren {A - B} }$

Proof:
Let $d = \dfrac a {\sin A}$.
From the Law of Sines, let:
:$d = \dfrac a {\sin A} = \dfrac b {\sin B}$
so that:
{{begin-eqn}}
{{eqn | l = a
      | r = d \sin A
      | c = 
}}
{{eqn | l = b
      | r = d \sin B
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {a + b} {a - b}
      | r = \frac {d \sin A + d \sin B} {d \sin A - d \sin B}
      | c = 
}}
{{eqn | r = \frac {\sin A + \sin B} {\sin A - \sin B}
      | c = 
}}
{{eqn-intertext|Let $C {{=}} \frac 1 2 \paren {A + B}$ and $D {{=}} \frac 1 2 \paren {A - B}$, and proceed as follows:}}
{{eqn | ll= \leadsto
      | l = \frac {a + b} {a - b}
      | r = \frac {2 \sin C \cos D} {\sin A - \sin B}
      | c = Sine plus Sine
}}
{{eqn | r = \frac {2 \sin C \cos D} {2 \sin D \cos C}
      | c = Sine minus Sine
}}
{{eqn | r = \frac {\frac {\sin C} {\cos C} } {\frac {\sin D} {\cos D} }
      | c = dividing top and bottom by $\cos C \cos D$
}}
{{eqn | r = \frac {\tan C} {\tan D}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {\tan \frac 1 2 \paren {A + B} } {\tan \frac 1 2 \paren {A - B} }
      | c = substituting back for $C$ and $D$
}}
{{end-eqn}}
{{qed}}
Theorem: Law of Tangents

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:
:$\dfrac {a + b} {a - b} = \dfrac {\tan \frac 1 2 \paren {A + B} } {\tan \frac 1 2 \paren {A - B} }$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {a + b} {a - b}
      | r = \dfrac {\tan \frac 1 2 \paren {A + B} } {\tan \frac 1 2 \paren {A - B} }
      | c = Law of Tangents
}}
{{eqn | ll= \leadsto
      | l = \tan \frac {A - B} 2
      | r = \dfrac {a - b} {a + b} \tan \frac {A + B} 2
      | c = algebraic manipulation
}}
{{eqn | r = \dfrac {a - b} {a + b} \tan \frac {180 \degrees - C} 2
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = \dfrac {a - b} {a + b} \map \tan {90 \degrees - \frac C 2}
}}
{{eqn | r = \dfrac {a - b} {a + b} \cot \dfrac C 2
      | c = Tangent of Complement equals Cotangent
}}
{{end-eqn}}
{{qed}}
Theorem: Law of Tangents

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:
:$\dfrac {a + b} {a - b} = \dfrac {\tan \frac 1 2 \paren {A + B} } {\tan \frac 1 2 \paren {A - B} }$

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac {a - b} {a + b}
      | r = \dfrac {2 R \sin A - 2 R \sin B} {2 R \sin A + 2 R \sin B}
      | c = Law of Sines
}}
{{eqn | r = \dfrac {2 \cos \frac {A + B} 2 \sin \frac {A - B} 2} {2 \sin \frac {A + B} 2 \cos \frac {A - B} 2}
      | c = Sine minus Sine, Sine plus Sine
}}
{{eqn | r = \dfrac {\tan \frac {A - B} 2} {\tan \frac {A + B} 2}
      | c = Tangent is Sine divided by Cosine and simplification
}}
{{eqn | r = \dfrac {\tan \frac {A - B} 2} {\tan \frac {180 \degrees - C} 2}
      | c = Sum of Angles of Triangle equals Two Right Angles
}}
{{eqn | r = \dfrac {\tan \frac {A - B} 2} {\map \tan {90^\circ - \frac C 2} }
      | c = simplification
}}
{{eqn | r = \dfrac {\tan \frac {A - B} 2} {\cot \dfrac C 2}
      | c = Tangent of Complement equals Cotangent
}}
{{eqn | ll= \leadsto
      | l = \dfrac {a - b} {a + b} \cot \dfrac C 2
      | r = \tan \frac {A - B} 2
      | c = Tangent of Complement equals Cotangent
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sine of Angle of Triangle by Semiperimeter

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:
: $\sin A = \dfrac 2 {b c} \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
where $\sin$ denotes sine and $s$ is the semiperimeter: $s = \dfrac {a + b + c} 2$.

Proof:
Let $Q$ be the area of $\triangle ABC$.
From Area of Triangle in Terms of Two Sides and Angle:
:$Q = \dfrac {b c \sin A} 2$
From Heron's Formula:
:$Q = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
Equating the two:
:$\dfrac {b c \sin A} 2 = \sqrt {s \paren {s - a} \paren {s - b} \paren {s - c} }$
from which follows the result.
{{qed}}