avewright/proofwiki-math huggingface dataset:
Theorem: Chinese Remainder Theorem (Commutative Algebra)

Let $A$ be a commutative and unitary ring.
{{explain|Can this condition be weakened?}}
Let $I_1, \ldots, I_n$ for some $n \ge 1$ be ideals of $A$.
Then the ring homomorphism $\phi: A \to A / I_1 \times \cdots \times A / I_n$ defined as:
:$\map \phi x = \tuple {x + I_1, \ldots, x + I_n}$
has the kernel $\ds I := \bigcap_{i \mathop = 1}^n I_i$, and is surjective {{iff}} the ideals are pairwise coprime, that is:
:$\forall i \ne j: I_i + I_j = A$
Hence in that case, it induces an ring isomorphism:
:$A / I \to A / I_1 \times \cdots \times A / I_n$
through the First Isomorphism Theorem.

Proof:
Consider $\pi$ only as a homomorphism of groups.
Then Chinese Remainder Theorem (Groups) is applicable as Subgroup of Abelian Group is Normal. 
It remains to demonstrate that the condition $I_i + I_j = R$ for all $i \ne j$ assumed here is equivalent to:
:$\ds \forall k \le n - 1: I_{k + 1} + \bigcap_{i \mathop = 1}^k I_i = R$
The implication from the latter condition is immediate.
For the converse, let $i$ be arbitrary.
The result follows from:
{{begin-eqn}}
{{eqn | l = R
      | r = \prod_{j \mathop \ne i} \paren {I_i + I_j}
      | c = $R$ has a unit and $I_i + I_j = R$ for $j \ne i$
}}
{{eqn | o = \subseteq
      | r = I_i + \prod_{j \mathop \ne i} I_j
      | c = {{Ring-axiom|D}}, {{Defof|Ideal of Ring}}
}}
{{eqn | o = \subseteq
      | r = I_i + \bigcap_{j \mathop \ne i}^n I_j
      | c = Intersection of Ideals of Ring contains Product
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of i

:$\sin i = \paren {\dfrac e 2 - \dfrac 1 {2 e} } i$

Proof:
We have:
{{begin-eqn}}
{{eqn | n = 1
      | l = \cos i + i \sin i
      | r = e^{i \times i}
      | c = Euler's Formula
}}
{{eqn | r = e^{-1}
      | c = {{Defof|Imaginary Unit}}
}}
{{eqn | r = \frac 1 e
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | n = 2
      | l = \cos i - i \sin i
      | r = \map \cos {-i} + i \map \sin {-i}
      | c = Cosine Function is Even and Sine Function is Odd
}}
{{eqn | r = e^{i \times \paren {-i} }
      | c = Euler's Formula
}}
{{eqn | r = e^1
      | c = {{Defof|Imaginary Unit}}
}}
{{eqn | r = e
}}
{{end-eqn}}
Then from $(1) - (2)$:
{{begin-eqn}}
{{eqn | l = 2 i \sin i
      | r = \frac 1 e - e
}}
{{eqn | ll= \leadsto
      | l = \sin i
      | r = \frac 1 {2 i} \paren {\frac 1 e - e}
}}
{{eqn | r = \paren {\frac e 2 - \frac 1 {2 e} } i
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of i

:$\sin i = \paren {\dfrac e 2 - \dfrac 1 {2 e} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \sin i
      | r = i \sinh 1
      | c = Hyperbolic Sine in terms of Sine
}}
{{eqn | r = i \frac {e^1 - e^{-1} } 2
      | c = {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \paren {\frac e 2 - \frac 1 {2 e} } i
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of i

:$\cos i = \dfrac e 2 + \dfrac 1 {2 e}$

Proof:
We have:
{{begin-eqn}}
{{eqn | n = 1
      | l = \cos i + i \sin i
      | r = e^{i \times i}
      | c = Euler's Formula
}}
{{eqn | r = e^{-1}
      | c = {{Defof|Imaginary Unit}}
}}
{{eqn | r = \frac 1 e
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | n = 2
      | l = \cos i - i \sin i
      | r = \map \cos {-i} + i \map \sin {-i}
      | c = Cosine Function is Even and Sine Function is Odd
}}
{{eqn | r = e^{i \times \paren {-i} }
      | c = Euler's Formula
}}
{{eqn | r = e^1
      | c = {{Defof|Imaginary Unit}}
}}
{{eqn | r = e
}}
{{end-eqn}}
Then from $(1) + (2)$:
{{begin-eqn}}
{{eqn | l = 2 \cos i
      | r = \frac 1 e + e
}}
{{eqn | ll= \leadsto
      | l = \cos i
      | r = \frac 1 2 \paren {\frac 1 e + e}
}}
{{eqn | r = \frac e 2 + \frac 1 {2 e}
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of i

:$\cos i = \dfrac e 2 + \dfrac 1 {2 e}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos i
      | r = \cosh 1
      | c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn | r = \frac {e^1 + e^{-1} } 2
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac e 2 + \frac 1 {2 e}
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of i

:$\tan i = \paren {\dfrac {e^2 - 1} {e^2 + 1} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \tan i
      | r = \frac {\sin i} {\cos i}
      | c = {{Defof|Complex Tangent Function}}
}}
{{eqn | r = \frac {\paren {\frac e 2 - \frac 1 {2 e} } i} {\frac e 2 + \frac 1 {2 e} }
      | c = Sine of $i$ and Cosine of $i$
}}
{{eqn | r = \paren {\frac {e - \frac 1 e} {e + \frac 1 e} } i
      | c = multiplying denominator and numerator by $2$
}}
{{eqn | r = \paren {\frac {e^2 - 1} {e^2 + 1} } i
      | c = multiplying denominator and numerator by $e$
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of i

:$\tan i = \paren {\dfrac {e^2 - 1} {e^2 + 1} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \tan i
      | r = i \tanh 1
      | c = Hyperbolic Tangent in terms of Tangent
}}
{{eqn | r = \paren {\frac {e^1 - e^{-1} } {e^1 + e^{-1} } } i
      | c = {{Defof|Hyperbolic Tangent}}
}}
{{eqn | r = \paren {\frac {e^2 - 1} {e^2 + 1} } i
      | c = multiplying denominator and numerator by $e$
}}
{{end-eqn}}
{{qed}}
Theorem: Cosecant of i

:$\csc i = \paren {\dfrac {2 e} {1 - e^2} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \csc i
      | r = \frac 1 {\sin i}
      | c = {{Defof|Complex Cosecant Function}}
}}
{{eqn | r = \frac 1 {\paren {\frac e 2 - \frac 1 {2 e} } i}
      | c = Sine of $i$
}}
{{eqn | r = \paren {\frac 1 {\frac 1 {2 e} - \frac e 2} } i
      | c = Reciprocal of $i$
}}
{{eqn | r = \paren {\frac {2 e} {1 - e^2} } i
      | c = multiplying denominator and numerator by $2 e$
}}
{{end-eqn}}
{{qed}}
Theorem: Cosecant of i

:$\csc i = \paren {\dfrac {2 e} {1 - e^2} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \csc i
      | r = -i \csch 1
      | c = Hyperbolic Cosecant in terms of Cosecant
}}
{{eqn | r = -\paren {\frac 2 {e^1 - e^{-1} } } i
      | c = {{Defof|Hyperbolic Cosecant}}
}}
{{eqn | r = -\paren {\frac {2 e} {e^2 - 1} } i
      | c = multiplying denominator and numerator by $e$
}}
{{eqn | r = \paren {\frac {2 e} {1 - e^2} } i
}}
{{end-eqn}}
{{qed}}
Theorem: Secant of i

:$\sec i = \dfrac {2 e} {e^2 + 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \sec i
      | r = \frac 1 {\cos i}
      | c = {{Defof|Complex Secant Function}}
}}
{{eqn | r = \frac 1 {\frac e 2 + \frac 1 {2 e} }
      | c = Cosine of $i$
}}
{{eqn | r = \frac {2 e} {e^2 + 1}
      | c = multiplying denominator and numerator by $2 e$
}}
{{end-eqn}}
{{qed}}
Theorem: Secant of i

:$\sec i = \dfrac {2 e} {e^2 + 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \sec i
      | r = \sech 1
      | c = Hyperbolic Secant in terms of Secant
}}
{{eqn | r = \frac 2 {e^1 + e^{-1} }
      | c = {{Defof|Hyperbolic Secant}}
}}
{{eqn | r = \frac {2 e} {e^2 + 1}
      | c = multiplying denominator and numerator by $e$
}}
{{end-eqn}}
{{qed}}
Theorem: Cotangent of i

:$\cot i = \paren {\dfrac {1 + e^2} {1 - e^2} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \cot i
      | r = \frac {\cos i} {\sin i}
      | c = {{Defof|Complex Cotangent Function}}
}}
{{eqn | r = \frac {\frac e 2 + \frac 1 {2 e} } {\left({\frac e 2 - \frac 1 {2 e} }\right) i}
      | c = Cosine of $i$ and Sine of $i$
}}
{{eqn | r = \left({\frac {e + \frac 1 e} {e - \frac 1 e} }\right) \left({\frac 1 i}\right)
      | c = multiplying denominator and numerator by $2$
}}
{{eqn | r = \left({ \frac {e^2 + 1} {e^2 - 1} }\right) \left({\frac 1 i}\right)
      | c = multiplying denominator and numerator by $e$
}}
{{eqn | r = \left({ \frac {1 + e^2} {1 - e^2} }\right) i
      | c = Reciprocal of $i$
}}
{{end-eqn}}
{{qed}}
Theorem: Cotangent of i

:$\cot i = \paren {\dfrac {1 + e^2} {1 - e^2} } i$

Proof:
{{begin-eqn}}
{{eqn | l = \cot i
      | r = -i \coth 1
      | c = Hyperbolic Cotangent in terms of Cotangent
}}
{{eqn | r = -\paren {\frac {e^1 + e^{-1} } {e^1 - e^{-1} } } i
      | c = {{Defof|Hyperbolic Cotangent|index = 1}}
}}
{{eqn | r = -\paren {\frac {e^2 + 1} {e^2 - 1} } i
      | c = multiplying denominator and numerator by $e$
}}
{{eqn | r = \paren {\frac {1 + e^2} {1 - e^2} } i
}}
{{end-eqn}}
{{qed}}
Theorem: Sine in terms of Cosine

{{begin-eqn}}
{{eqn | l = \sin x
      | r = +\sqrt {1 - \cos ^2 x}
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
}}
{{eqn | l = \sin x
      | r = -\sqrt {1 - \cos ^2 x}
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \cos^2 x + \sin^2 x
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin^2 x
      | r = 1 - \cos^2 x
}}
{{eqn | ll= \leadsto
      | l = \sin x
      | r = \pm \sqrt {1 - \cos^2 x}
}}
{{end-eqn}}
Then from Sign of Sine:
{{begin-eqn}}
{{eqn | l = \sin x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
}}
{{eqn | l = \sin x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
}}
{{end-eqn}}
{{qed}}
Theorem: Secant in terms of Tangent

{{begin-eqn}}
{{eqn | l = \sec x
      | r = +\sqrt {\tan ^2 x + 1}
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \sec x
      | r = -\sqrt {\tan ^2 x + 1}
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \sec^2 x - \tan^2 x
      | r = 1
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = \sec^2 x
      | r = \tan^2 x + 1
}}
{{eqn | ll= \leadsto
      | l = \sec x
      | r = \pm \sqrt {\tan ^2 x + 1}
}}
{{end-eqn}}
Also, from Sign of Secant:
:If there exists integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$, then $\sec x > 0$.
:If there exists integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$, then $\sec x < 0$.
When $\cos x = 0$, $\sec x$ and $\tan x$ is undefined.
{{qed}}
Theorem: Sine in terms of Tangent

{{begin-eqn}}
{{eqn | l = \sin x
      | r = +\frac {\tan x} {\sqrt {1 + \tan^2 x} }
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \sin x
      | r = -\frac {\tan x} {\sqrt {1 + \tan^2 x} }
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}

Proof:
For the first part, if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = +\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = Cosine in terms of Tangent
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\paren {\frac 1 {\cos x} } }
      | r = +\frac 1 {\sqrt {1 + \tan^2 x} }
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} {\paren {\frac {\sin x} {\cos x} } }
      | r = +\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = multiplying denominator and numerator by $\sin x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} {\tan x}
      | r = + \frac 1 {\sqrt {1 + \tan^2 x} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin x
      | r = + \frac {\tan x} {\sqrt {1 + \tan^2 x} }
}}
{{end-eqn}}
For the second part, if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = -\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = Cosine in terms of Tangent
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\paren {\frac 1 {\cos x} } }
      | r = -\frac 1 {\sqrt {1 + \tan^2 x} }
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} {\paren {\frac {\sin x} {\cos x} } }
      | r = -\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = multiplying denominator and numerator by $\sin x$
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} {\tan x}
      | r = -\frac 1 {\sqrt {1 + \tan^2 x} }
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin x
      | r = -\frac {\tan x} {\sqrt {1 + \tan^2 x} }
}}
{{end-eqn}}
When $\cos x = 0$, $\tan x$ is undefined.
{{qed}}
Theorem: Sine is Reciprocal of Cosecant

:$\sin \theta = \dfrac 1 {\csc \theta}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {\sin \theta}
      | r = \csc \theta
      | c = Cosecant is Reciprocal of Sine
}}
{{eqn | ll= \leadsto
      | l = \sin \theta
      | r = \frac 1 {\csc \theta}
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent is Reciprocal of Cotangent

:$\tan \theta = \dfrac 1 {\cot \theta}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {\tan \theta}
      | r = \cot \theta
      | c = Cotangent is Reciprocal of Tangent
}}
{{eqn | ll= \leadsto
      | l = \tan \theta
      | r = \frac 1 {\cot \theta}
}}
{{end-eqn}}
$\tan \theta$ is not defined when $\cos \theta = 0$, and $\cot \theta$ is not defined when $\sin \theta = 0$.
{{qed}}
Theorem: Cosine is Reciprocal of Secant

:$\cos \theta = \dfrac 1 {\sec \theta}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {\cos \theta}
      | r = \sec \theta
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | ll= \leadsto
      | l = \cos \theta
      | r = \frac 1 {\sec \theta}
}}
{{end-eqn}}
$\sec \theta$ and $\dfrac 1 {\cos \theta}$ are not defined when $\cos \theta = 0$.
{{qed}}
Theorem: Sine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\sin \paren {a + b i} = \sin a \cosh b + i \cos a \sinh b$
where:
:$\sin$ denotes the sine function (real and complex)
:$\cos$ denotes the real cosine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function.

Proof:
{{begin-eqn}}
{{eqn | l = \sinh \paren {a + b i}
      | r = \sinh a \cosh \paren {b i} + \cosh a \sinh \paren {b i}
      | c = Hyperbolic Sine of Sum
}}
{{eqn | r = \sinh a \cos b + \cosh a \sin \paren {b i}
      | c = Cosine in terms of Hyperbolic Cosine
}}
{{eqn | r = \sinh a \cos b + i \cosh a \sin b
      | c = Sine in terms of Hyperbolic Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\sin \paren {a + b i} = \sin a \cosh b + i \cos a \sinh b$
where:
:$\sin$ denotes the sine function (real and complex)
:$\cos$ denotes the real cosine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function.

Proof:
{{begin-eqn}}
{{eqn | l = \sinh a \cos b + i \cosh a \sin b
      | r = \frac {e^a - e^{-a} } 2 \frac {e^{i b} + e^{-i b} } 2 + i \frac {e^a + e^{-a} } 2 \frac {e^{i b} - e^{-i b} } {2 i}
      | c = {{Defof|Hyperbolic Sine}}, Euler's Cosine Identity, {{Defof|Hyperbolic Cosine}}, Euler's Sine Identity
}}
{{eqn | r = \frac {e^{a + i b} - e^{-a + i b} + e^{a - i b} - e^{-a - i b} + e^{a + i b} + e^{-a + i b} - e^{a - i b} - e^{-a - i b} } 4
      | c = simplifying
}}
{{eqn | r = \frac {e^{\paren {a + b i} } - e^{-\paren {a + b i} } } 2
      | c = simplifying
}}
{{eqn | r = \sinh \paren {a + b i}
      | c = {{Defof|Hyperbolic Sine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\sin \paren {a + b i} = \sin a \cosh b + i \cos a \sinh b$
where:
:$\sin$ denotes the sine function (real and complex)
:$\cos$ denotes the real cosine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function.

Proof:
{{begin-eqn}}
{{eqn | l = \sin \paren {a + b i}
      | r = \sin a \cos \paren {b i} + \cos a \sin \paren {b i}
      | c = Sine of Sum {{explain|Is Sine of Sum valid for complex numbers? Here is $ib$ complex.<br/>Of course it is, we just haven't proved it properly. Needs to be done. Sources quoted on the relevant pages do not go into details.}}
}}
{{eqn | r = \sin a \cosh b + \cos a \sin \paren {b i}
      | c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn | r = \sin a \cosh b + i \cos a \sinh b
      | c = Hyperbolic Sine in terms of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\sin \paren {a + b i} = \sin a \cosh b + i \cos a \sinh b$
where:
:$\sin$ denotes the sine function (real and complex)
:$\cos$ denotes the real cosine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function.

Proof:
{{begin-eqn}}
{{eqn | l = \sin a \cosh b + i \cos a \sinh b
      | r = \frac {e^{i a} - e^{-i a} } {2 i} \frac {e^b - e^{-b} } 2 + i \frac {e^{i a} + e^{-i a} } 2 \frac {e^b - e^{-b} } 2
      | c = Euler's Sine Identity, Euler's Cosine Identity, {{Defof|Hyperbolic Sine}}, {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac {e^{b + i a} - e^{-b + i a} - e^{b - i a} + e^{-b - i a} - e^{b + i a} + e^{-b + i a} - e^{b - i a} + e^{-b - i a} } {4 i}
      | c = simplifying
}}
{{eqn | r = \frac {e^{-b - i a} - e^{b - i a} } {2 i}
      | c = simplifying
}}
{{eqn | r = \frac {e^{i \paren {a + b i} } - e^{-i \paren {a + b i} } } {2 i}
      | c = 
}}
{{eqn | r = \map \sin {a + b i}
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\cos \left({a + b i}\right) = \cos a \cosh b - i \sin a \sinh b$
where:
:$\cos$ denotes the cosine function (real and complex)
:$\sin$ denotes the real sine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function

Proof:
{{begin-eqn}}
{{eqn | l = \cos \paren {a + b i}
      | r = \cos a \cos \paren {b i} - \sin a \sin \paren {b i}
      | c = Cosine of Sum
}}
{{eqn | r = \cos a \cosh b - \sin a \sin \paren {b i}
      | c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn | r = \cos a \cosh b - i \sin a \sinh b
      | c = Hyperbolic Sine in terms of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\cos \left({a + b i}\right) = \cos a \cosh b - i \sin a \sinh b$
where:
:$\cos$ denotes the cosine function (real and complex)
:$\sin$ denotes the real sine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function

Proof:
{{begin-eqn}}
{{eqn | l = \cos a \cosh b - i \sin a \sinh b
      | r = \frac {e^{i a} + e^{-i a} } 2 \frac {e^b + e^{-b} } 2 - i \frac {e^{i a} - e^{-i a} } {2 i} \frac {e^b - e^{-b} } 2
      | c = Euler's Cosine Identity, {{Defof|Hyperbolic Cosine}}, Euler's Sine Identity, {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \frac {e^{b + i a} + e^{-b + i a} + e^{b - i a} + e^{-b - i a} - e^{b + i a} + e^{-b + i a} + e^{b - i a} - e^{-b - i a} } 4
      | c = simplifying
}}
{{eqn | r = \frac {e^{-b + i a} + e^{b - i a} } 2
      | c = simplifying
}}
{{eqn | r = \frac {e^{i \paren {a + b i} } + e^{-i \paren {a + b i} } } 2
      | c = 
}}
{{eqn | r = \map \cos {a + b i}
      | c = Euler's Cosine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\cos \left({a + b i}\right) = \cos a \cosh b - i \sin a \sinh b$
where:
:$\cos$ denotes the cosine function (real and complex)
:$\sin$ denotes the real sine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function

Proof:
{{begin-eqn}}
{{eqn | l = \map \cosh {a + b i}
      | r = \cosh a \map \cosh {b i} + \sinh a \map \sinh {b i}
      | c = Hyperbolic Cosine of Sum
}}
{{eqn | r = \cosh a \cos b + \sinh a \map \sinh {b i}
      | c = Cosine in terms of Hyperbolic Cosine
}}
{{eqn | r = \cosh a \cos b + i \sinh a \sin b
      | c = Sine in terms of Hyperbolic Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Complex Number

Let $a$ and $b$ be real numbers.
Let $i$ be the imaginary unit.
Then:
:$\cos \left({a + b i}\right) = \cos a \cosh b - i \sin a \sinh b$
where:
:$\cos$ denotes the cosine function (real and complex)
:$\sin$ denotes the real sine function
:$\sinh$ denotes the hyperbolic sine function
:$\cosh$ denotes the hyperbolic cosine function

Proof:
{{begin-eqn}}
{{eqn | l = \cosh a \cos b - i \sinh a \sin b
      | r = \frac {e^a + e^{-a} } 2 \frac {e^{i b} + e^{-i b} } 2 + i \frac {e^a - e^{-a} } {2 i} \frac {e^{i b} - e^{-i b} } 2
      | c = {{Defof|Hyperbolic Cosine}}, Euler's Cosine Identity, {{Defof|Hyperbolic Sine}}, Euler's Sine Identity
}}
{{eqn | r = \frac {e^{a + i b} + e^{-a + i b} + e^{a - i b} + e^{-a - i b} + e^{a + i b} - e^{-a + i b} - e^{a - i b} + e^{-a - i b} } 4
      | c = simplifying
}}
{{eqn | r = \frac {e^{a + i b} + e^{-\paren {a + i b} } } 2
      | c = simplifying
}}
{{eqn | r = \cosh \paren {a + b i}
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine in terms of Sine

{{begin-eqn}}
{{eqn | l = \cos x
      | r = +\sqrt {1 - \sin^2 x}
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \cos x
      | r = -\sqrt {1 - \sin^2 x}
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \cos^2 x + \sin^2 x
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \cos^2 x
      | r = 1 - \sin^2 x
}}
{{eqn | ll= \leadsto
      | l = \cos x
      | r = \pm \sqrt {1 - \sin^2 x}
}}
{{end-eqn}}
Then from Sign of Cosine:
{{begin-eqn}}
{{eqn | l = \cos x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n - \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 1 2} \pi$
}}
{{eqn | l = \cos x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + \dfrac 1 2} \pi < x < \paren {2 n + \dfrac 3 2} \pi$
}}
{{end-eqn}}
{{qed}}
Theorem: Sine in terms of Secant

{{begin-eqn}}
{{eqn | l = \sin x
      | r = + \frac {\sqrt{\sec ^2 x - 1} } {\sec x}
      | c = if there exists an integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$
}}
{{eqn | l = \sin x
      | r = - \frac {\sqrt{\sec ^2 x - 1} } {\sec x}
      | c = if there exists an integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$
}}
{{end-eqn}}

Proof:
For the first part, if there exists integer $n$ such that $n \pi < x < \paren {n + \dfrac 1 2} \pi$:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = +\sqrt {\sec^2 x - 1}
      | c = Tangent in terms of Secant
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} {\cos x}
      | r = +\sqrt {\sec^2 x - 1}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin x \sec x
      | r = +\sqrt {\sec^2 x - 1}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin x
      | r = +\frac {\sqrt {\sec^2 x - 1} } {\sec x}
}}
{{end-eqn}}
For the second part, if there exists integer $n$ such that $\paren {n + \dfrac 1 2} \pi < x < \paren {n + 1} \pi$:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = -\sqrt {\sec^2 x - 1}
      | c = Tangent in terms of Secant
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} {\cos x}
      | r = -\sqrt {\sec^2 x - 1}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin x \sec x
      | r = -\sqrt {\sec^2 x - 1}
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | ll= \leadsto
      | l = \sin x
      | r = -\frac {\sqrt {\sec^2 x - 1} } {\sec x}
}}
{{end-eqn}}
When $\cos x = 0$, $\sec x$ is undefined.
{{qed}}
Theorem: Sign of Sine

Let $x$ be a real number.
{{begin-eqn}}
{{eqn | l = \sin x
      | o = >
      | r = 0
      | c = if there exists an integer $n$ such that $2 n \pi < x < \paren {2 n + 1} \pi$
}}
{{eqn | l = \sin x
      | o = <
      | r = 0
      | c = if there exists an integer $n$ such that $\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi$
}}
{{end-eqn}}
where $\sin$ is the real sine function.

Proof:
First the case where $n \ge 0$ is addressed.
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\forall x \in \R:$
::$2 n \pi < x < \paren {2 n + 1} \pi \implies \sin x > 0$
::$\paren {2 n + 1} \pi < x < \paren {2 n + 2} \pi \implies \sin x < 0$