avewright/proofwiki-math huggingface dataset:
Theorem: Product of Complex Numbers in Polar Form

Let $z_1 := \polar {r_1, \theta_1}$ and $z_2 := \polar {r_2, \theta_2}$ be complex numbers expressed in polar form.
Then:
:$z_1 z_2 = r_1 r_2 \paren {\map \cos {\theta_1 + \theta_2} + i \map \sin {\theta_1 + \theta_2} }$

Proof:
{{begin-eqn}}
{{eqn | l = z_1 z_2
      | r = r_1 \paren {\cos \theta_1 + i \sin \theta_1} r_2 \paren {\cos \theta_2 + i \sin \theta_2}
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = r_1 r_2 \paren {\paren {\cos \theta_1 \cos \theta_2 - \sin \theta_1 \sin \theta_2} + i \paren {\cos \theta_1 \sin \theta_2 + \sin \theta_1 \cos \theta_2} }
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = r_1 r_2 \paren {\map \cos {\theta_1 + \theta_2} + i \paren {\cos \theta_1 \sin \theta_2 + \sin \theta_1 \cos \theta_2} }
      | c = Cosine of Sum
}}
{{eqn | r = r_1 r_2 \paren {\map \cos {\theta_1 + \theta_2} + i \map \sin {\theta_1 + \theta_2} }
      | c = Sine of Sum
}}
{{end-eqn}}
{{qed}}
Theorem: Equality of Complex Numbers

Let $z_1 := a_1 + i b_1$ and $z_2 := a_2 + i b_2$ be complex numbers.
Then $z_1 = z_2$ {{iff}} $a_1 = a_2$ and $b_1 = b_2$.

Proof:
By definition of a complex number, $z_1$ and $z_2$ can be expressed in the form:
:$z_1 = \tuple {a_1, b_1}$
:$z_2 = \tuple {a_2, b_2}$
where $\tuple {a, b}$ denotes an ordered pair.
The result follows from Equality of Ordered Pairs.
Theorem: Subtraction of Complex Numbers

Let $z_1 := a_1 + i b_1$ and $z_2 := a_2 + i b_2$ be complex numbers.
The subtraction operation on $z_1$ and $z_2$ is:
:$z_1 - z_2 = \paren {a_1 - a_2} + i \paren {b_1 - b_2}$

Proof:
{{begin-eqn}}
{{eqn | l = z_1 - z_2
      | r = z_1 + \paren {- z_2}
      | c = {{Defof|Complex Subtraction}}
}}
{{eqn | r = a_1 + \paren {-a_2} + i \paren {b_1 + \paren {-b_2} }
      | c = Inverse for Complex Addition
}}
{{eqn | r = \paren {a_1 - a_2} + i \paren {b_1 - b_2}
      | c = {{Defof|Complex Subtraction}}
}}
{{end-eqn}}
{{qed}}
Theorem: Division of Complex Numbers

Let $z_1 := a_1 + i b_1$ and $z_2 := a_2 + i b_2$ be complex numbers such that $z_2 \ne 0$.
The operation of division is performed on $z_1$ by $z_2$ as follows:
:$\dfrac {z_1} {z_2} = \dfrac {a_1 a_2 + b_1 b_2} {a_2^2 + b_2^2} + i \dfrac {a_2 b_1 - a_1 b_2} {a_2^2 + b_2^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {z_1} {z_2}
      | r = z_1 \paren {z_2}^{-1}
      | c = {{Defof|Complex Division}}
}}
{{eqn | r = \paren {a_1 + i b_1} \dfrac {a_2 - i b_2} {a_2^2 + b_2^2}
      | c = Inverse for Complex Multiplication
}}
{{eqn | r = \frac {\paren {a_1 a_2 + b_1 b_2} + i \paren {a_2 b_1 - a_1 b_2} } {a_2^2 + b_2^2}
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = \frac {a_1 a_2 + b_1 b_2} {a_2^2 + b_2^2} + i \frac {a_2 b_1 - a_1 b_2} {a_2^2 + b_2^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: De Moivre's Formula/Proof 1

Let $z \in \C$ be a complex number expressed in complex form:
:$z = r \paren {\cos x + i \sin x}$
Then:
:$\forall \omega \in \C: \paren {r \paren {\cos x + i \sin x} }^\omega = r^\omega \map \cos {\omega x} + i \map \sin {\omega x}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {r \paren {\cos x + i \sin x} }^\omega
      | r = \paren {r e^{i x} }^\omega
      | c = Euler's Formula
}}
{{eqn | r = r^\omega e^{i \omega x}
      | c = Power of Power
}}
{{eqn | r = r^\omega \paren {\map \cos {\omega x} + i \map \sin {\omega x} }
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Theorem: Division of Complex Numbers in Polar Form

Let $z_1 := \polar {r_1, \theta_1}$ and $z_2 := \polar {r_2, \theta_2}$ be complex numbers expressed in polar form, such that $z_2 \ne 0$.
Then:
:$\dfrac {z_1} {z_2} = \dfrac {r_1} {r_2} \paren {\map \cos {\theta_1 - \theta_2} + i \map \sin {\theta_1 - \theta_2} }$
or:
:$\dfrac {z_1} {z_2} = \dfrac {r_1} {r_2} \map \cis {\theta_1 - \theta_2}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {z_1} {z_2}
      | r = \frac {r_1 \paren {\cos \theta_1 + i \sin \theta_1} } {r_2 \paren {\cos \theta_2 + i \sin \theta_2} }
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = \frac {\paren {r_1 \paren {\cos \theta_1 + i \sin \theta_1} } \paren {r_2 \paren {\cos \theta_2 - i \sin \theta_2} } } {\paren {r_2 \paren {\cos \theta_2 + i \sin \theta_2} } \paren {r_2 \paren {\cos \theta_2 - i \sin \theta_2} } }
      | c = multiplying numerator and denominator by $r_2 \paren {\cos \theta_1 - i \sin \theta_1}$
}}
{{eqn | r = \frac {r_1 r_2 \paren {\map \cos {\theta_1 - \theta_2} + i \map \sin {\theta_1 - \theta_2} } } {r_2^2 \paren {\map \cos {\theta_2 - \theta_2} + i \map \sin {\theta_2 - \theta_2} } }
      | c = Product of Complex Numbers in Polar Form
}}
{{eqn | r = \frac {r_1 \paren {\map \cos {\theta_1 - \theta_2} + i \map \sin {\theta_1 - \theta_2} } } {r_2 \paren {\cos 0 + i \sin 0} }
      | c = 
}}
{{eqn | r = \frac {r_1 \paren {\map \cos {\theta_1 - \theta_2} + i \map \sin {\theta_1 - \theta_2} } } {r_2 \paren {1 + 0} }
      | c = {{cos|0}} and {{sin|0}}
}}
{{eqn | r = \frac {r_1} {r_2} \paren {\map \cos {\theta_1 - \theta_2} + i \map \sin {\theta_1 - \theta_2} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Roots of Complex Number

Let $z := \polar {r, \theta}$ be a complex number expressed in polar form, such that $z \ne 0$.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then the $n$th roots of $z$ are given by:
:$z^{1 / n} = \set {r^{1 / n} \paren {\map \cos {\dfrac {\theta + 2 \pi k} n} + i \, \map \sin {\dfrac {\theta + 2 \pi k} n} }: k \in \set {0, 1, 2, \ldots, n - 1} }$
There are $n$ distinct such $n$th roots.

Proof:
Let:
: $w := r^{1 / n} \paren {\map \cos {\dfrac {\theta + 2 \pi k} n} + i \, \map \sin {\dfrac {\theta + 2 \pi k} n} }$
for $k \in \Z_{>0}$.
Then:
{{begin-eqn}}
{{eqn | l = w^n
      | r = \paren {r^{1 / n} \paren {\map \cos {\dfrac {\theta + 2 \pi k} n} + i \, \sin {\dfrac {\theta + 2 \pi k} n} } }^n
      | c = 
}}
{{eqn | r = \paren {r^{1 / n} }^n \paren {\cos n \paren {\dfrac {\theta + 2 \pi k} n} + i \sin n \paren {\dfrac {\theta + 2 \pi k} n} }
      | c = De Moivre's Formula
}}
{{eqn | r = r \paren {\map \cos {\theta + 2 \pi k} + i \, \map \sin {\theta + 2 \pi k} }
      | c = 
}}
{{eqn | r = r \paren {\cos \theta + i \, \map \sin {\theta + 2 \pi k} }
      | c = Cosine of Angle plus Multiple of Full Angle
}}
{{eqn | r = r \paren {\cos \theta + i \sin \theta}
      | c = Sine of Angle plus Multiple of Full Angle
}}
{{end-eqn}}
Now let $m = k + n$.
Then:
{{begin-eqn}}
{{eqn | l = \frac {\theta + 2 m \pi} n 
      | r = \frac {\theta + 2 \paren {k + n} \pi} n
      | c = 
}}
{{eqn | r = \frac {\theta + 2 k \pi} n + \frac {2 n \pi} n
      | c = 
}}
{{eqn | r = \frac {\theta + 2 k \pi} n + 2 \pi
      | c = 
}}
{{eqn | r = \frac {\theta + 2 k \pi} n + 2 \pi
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cos \frac {\theta + 2 m \pi} n + i \sin \frac {\theta + 2 m \pi} n
      | r = \cos \frac {\theta + 2 k \pi} n + i \sin \frac {\theta + 2 k \pi} n
      | c = from above
}}
{{end-eqn}}
exploiting the fact that Sine and Cosine are Periodic on Reals.
The result follows.
{{qed}}
Theorem: Zeroth Power of Real Number equals One

Let $a \in \R_{>0}$ be a (strictly) positive real number.
Let $a^x$ be defined as $a$ to the power of $x$.
Then:
:$a^0 = 1$

Proof:
{{begin-eqn}}
{{eqn | l = a^0
      | r = \map \exp {0 \ln a}
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \map \exp 0
      | c = 
}}
{{eqn | r = 1
      | c = Exponential of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of One

:$\exp 1 = e$
where $e$ is Euler's number: $e = 2.718281828\ldots$

Proof:
We have that the exponential function is the inverse of the natural logarithm function:
:$\ln e = 1$
Hence the result.
{{qed}}
Theorem: Exponential of Zero

: $\exp 0 = 1$

Proof:
We have that the exponential function is the inverse of the natural logarithm function:
: $\ln 1 = 0$
Hence the result.
{{qed}}
Theorem: Exponential of Zero

: $\exp 0 = 1$

Proof:
Using the definition of the exponential as a limit of a sequence:
{{begin-eqn}}
{{eqn | l = \exp 0
      | r = \lim_{n \mathop \to \infty} \left({1 + \frac 0 n}\right)^n
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Zero

: $\exp 0 = 1$

Proof:
This proof assumes the power series definition of $\exp$.
That is, let:
:$\ds \exp x = \sum_{k \mathop = 0}^\infty \frac {x^k} {k!}$
Then:
{{begin-eqn}}
{{eqn | l = \exp 0
      | r = \sum_{k \mathop = 0}^\infty \frac {0^k} {k!}
}}
{{eqn | r = 1
      | c = {{Defof|Power of Zero}}
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Zero

: $\exp 0 = 1$

Proof:
This proof assumes the Definition of $\exp x$ as the unique continuous extension of $e^x$.
{{begin-eqn}}
{{eqn | l = \exp 0
      | r = e^0
}}
{{eqn | r = 1
      | c = {{Defof|Power (Algebra)|$x^0$}}, where $x \ne 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Zero

: $\exp 0 = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \map \exp {z + \paren {-z} }
      | r = \exp z \, \map \exp {-z}
      | c = Exponential of Sum
}}
{{eqn | ll= \leadsto
      | l = \map \exp {z - z}
      | r = \dfrac {\exp z} {\exp z}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \exp 0
      | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Logarithms

:$\log_b x - \log_b y = \map {\log_b} {\dfrac x y}$

Proof:
{{begin-eqn}}
{{eqn | l = \log_b x - \log_b y
      | r = \map {\log_b} {b^{\log_b x - \log_b y} }
      | c = {{Defof|General Logarithm}}
}}
{{eqn | r = \map {\log_b} {\frac {\paren {b^{\log_b x} } } {\paren {b^{\log_b y} } } }
      | c = Quotient of Powers
}}
{{eqn | r = \map {\log_b} {\frac x y}
      | c = {{Defof|General Logarithm}}
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Logarithms

:$\log_b x - \log_b y = \map {\log_b} {\dfrac x y}$

Proof:
{{begin-eqn}}
{{eqn | l = \log_b x - \log_b y
      | r = \frac {\log_e x} {\log_e b} - \frac {\log_e y} {\log_e b}
      | c = Change of Base of Logarithm
}}
{{eqn | r = \frac {\log_e x - \log_e y} {\log_e b}
      | c = 
}}
{{eqn | r = \frac {\log_e \left({\frac x y}\right)} {\log_e b}
      | c = Difference of Logarithms: Proof for Natural Logarithm
}}
{{eqn | r = \log_b \left({\frac x y}\right)
      | c = Change of Base of Logarithm
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Logarithms

:$\log_b x - \log_b y = \map {\log_b} {\dfrac x y}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\log_b} {\frac x y} + \log_b y
      | r = \map {\log_b} {\frac x y \times y}
      | c = Sum of Logarithms
}}
{{eqn | r = \log_b x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {\log_b} {\frac x y}
      | r = \log_b x - \log_b y
      | c = subtracting $\log_b y$ from both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Power of Identity is Identity

Let $\struct {M, \circ}$ be a monoid whose identity element is $e$.
Then:
:$\forall n \in \Z: e^n = e$

Proof:
Since $e$ is invertible, the power of $e$ is defined for all $n \in \Z$.
We prove the case $n \ge 0$ by induction.
Theorem: Euler's Tangent Identity/Formulation 1

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

Proof:
{{begin-eqn}}
{{eqn | l = \tan z
      | r = \frac {\sin z} {\cos z}
      | c = {{Defof|Complex Tangent Function}}
}}
{{eqn | r = \frac {\frac 1 2 i \paren {e^{-i z} - e^{i z} } } {\frac 1 2 \paren {e^{-i z} + e^{i z} } }
      | c = Euler's Sine Identity and Euler's Cosine Identity
}}
{{eqn | r = i \frac {e^{-i z} - e^{i z} } {e^{-i z} + e^{i z} }
}}
{{eqn | r = i \frac {1 - e^{2 i z} } {1 + e^{2 i z} }
      | c = multiplying numerator and denominator by $e^{i z}$
}}
{{end-eqn}}
{{qed}}
Category:Euler's Tangent Identity
lsw2wpazfdxygpspqolmyylt0qq6ag5
Theorem: Euler's Tangent Identity/Formulation 2

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

Proof:
{{begin-eqn}}
{{eqn | l = \tan z
      | r = \frac {\sin z} {\cos z}
      | c = {{Defof|Complex Tangent Function}}
}}
{{eqn | r = \frac {e^{i z} - e^{-i z} } {2 i} / \frac {e^{i z} + e^{-i z} } 2
      | c = Euler's Sine Identity and Euler's Cosine Identity
}}
{{eqn | r = \frac {e^{i z} - e^{-i z} } {i \paren {e^{i z} + e^{-i z} } }
      | c = multiplying top and bottom by $2 i$
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Tangent Identity/Formulation 3

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

Proof:
{{begin-eqn}}
{{eqn | l = \tan z
      | r = \frac {\sin z} {\cos z}
      | c = {{Defof|Complex Tangent Function}}
}}
{{eqn | r = \frac {e^{i z} - e^{-i z} } {i \paren {e^{i z} + e^{-i z} } }
      | c = Euler's Tangent Identity: Formulation 2
}}
{{eqn | r = -i \paren {\dfrac {e^{i z} - e^{-i z} } {e^{i z} + e^{-i z} } }
      | c = multiplying numerator and denominator by $-i$
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cotangent Identity

:$\cot z = i \dfrac {e^{i z} + e^{-i z} } {e^{i z} - e^{-i z} }$

Proof:
We have, {{hypothesis}}, that $z$ is a complex number such that:
:$\forall k \in \Z: z \ne k \pi$
Therefore:
:$\sin z \ne 0$
It follows from the definition of the complex cotangent function that:
:$\cot z$
is well-defined.
Hence:
{{begin-eqn}}
{{eqn | l = \cot z
      | r = \frac {\cos z} {\sin z}
      | c = {{Defof|Complex Cotangent Function}}
}}
{{eqn | r = \frac {e^{i z} + e^{-i z} } 2 / \frac {e^{i z} - e^{-i z} } {2 i}
      | c = Euler's Sine Identity and Euler's Cosine Identity
}}
{{eqn | r = i \frac {e^{i z} + e^{-i z} } {e^{i z} - e^{-i z} }
      | c = multiplying numerator and denominator by $2 i$
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cotangent Identity

:$\cot z = i \dfrac {e^{i z} + e^{-i z} } {e^{i z} - e^{-i z} }$

Proof:
We have, {{hypothesis}}, that $z$ is a complex number such that:
:$\forall k \in \Z: z \ne k \pi$
Therefore:
:$\sin z \ne 0$
It follows from the definition of the complex cotangent function that:
:$\cot z$
is well-defined.
Hence:
{{begin-eqn}}
{{eqn | l = \cot z
      | r = \frac 1 {\tan z}
      | c = {{Defof|Complex Cotangent Function}}
}}
{{eqn | r = 1 / \dfrac {e^{i z} - e^{-i z} } {i \paren {e^{i z} + e^{-i z} } }
      | c = Euler's Tangent Identity
}}
{{eqn | r = i \frac {e^{i z} + e^{-i z} } {e^{i z} - e^{-i z} }
      | c = {{Defof|Reciprocal}}
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Cosecant Identity

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

Proof:
{{begin-eqn}}
{{eqn | l = \csc z
      | r = \frac 1 {\sin z}
      | c = {{Defof|Complex Cosecant Function}}
}}
{{eqn | r = 1 / \frac {e^{i z} - e^{-i z} } {2 i}
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac {2 i} {e^{i z} - e^{-i z} }
      | c = multiplying top and bottom by $2 i$
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Secant Identity

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

Proof:
{{begin-eqn}}
{{eqn | l = \sec z
      | r = \frac 1 {\cos z}
      | c = {{Defof|Complex Secant Function}}
}}
{{eqn | r = 1 / \frac {e^{i z} + e^{-i z} } 2
      | c = Euler's Sine Identity and Euler's Cosine Identity
}}
{{eqn | r = \frac 2 {e^{i z} + e^{-i z} }
      | c = multiplying top and bottom by $2$
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Complex Numbers in Exponential Form

Let $z_1 := r_1 e^{i \theta_1}$ and $z_2 := r_2 e^{i \theta_2}$ be complex numbers expressed in exponential form.
Then:
:$z_1 z_2 = r_1 r_2 e^{i \paren {\theta_1 + \theta_2} }$

Proof:
{{begin-eqn}}
{{eqn | l = z_1 z_2
      | r = r_1 e^{i \theta_1} r_2 e^{i \theta_2}
      | c = {{Defof|Exponential Form of Complex Number}}
}}
{{eqn | r = r_1 \paren {\cos \theta_1 + i \sin \theta_1 } r_2 \paren {\cos \theta_2 + i \sin \theta_2}
      | c = Euler's Formula
}}
{{eqn | r = r_1 r_2 \paren {\map \cos {\theta_1 + \theta_2} + i \map \sin {\theta_1 + \theta_2} }
      | c = Product of Complex Numbers in Polar Form
}}
{{eqn | r = r_1 r_2 e^{i \paren {\theta_1 + \theta_2} }
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Theorem: Division of Complex Numbers in Exponential Form

Let $z_1 := r_1 e^{i \theta_1}$ and $z_2 := r_2 e^{i \theta_2}$ be complex numbers expressed in exponential form.
Then:
:$\dfrac {z_1} {z_2} = \dfrac {r_1} {r_2} e^{i \paren {\theta_1 - \theta_2} }$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {z_1} {z_2}
      | r = \frac {r_1 e^{i \theta_1} } {r_2 e^{i \theta_2} }
      | c = {{Defof|Exponential Form of Complex Number}}
}}
{{eqn | r = \frac {r_1 \paren {\cos \theta_1 + i \sin \theta_1 } } {r_2 \paren {\cos \theta_2 + i \sin \theta_2} }
      | c = Euler's Formula
}}
{{eqn | r = \frac {r_1} {r_2} \paren {\map \cos {\theta_1 - \theta_2} + i \map \sin {\theta_1 - \theta_2} }
      | c = Division of Complex Numbers in Polar Form
}}
{{eqn | r = \frac {r_1} {r_2} e^{i \paren {\theta_1 - \theta_2} }
      | c = Euler's Formula
}}
{{end-eqn}}
{{qed}}
Theorem: De Moivre's Formula/Exponential Form

:$\forall \omega \in \C: \paren {r e^{i \theta} }^\omega = r^\omega e^{i \omega \theta}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {r e^{i \theta} }^\omega
      | r = \paren {r \paren {\cos \theta + i \sin \theta} }^\omega
      | c = {{Defof|Exponential Form of Complex Number}}
}}
{{eqn | r = r^\omega \paren {\cos \omega \theta + i \sin \omega \theta}
      | c = De Moivre's Formula
}}
{{eqn | r = r^\omega e^{i \omega \theta}
      | c = {{Defof|Exponential Form of Complex Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Roots of Complex Number/Exponential Form

:$z^{1 / n} = \set {r^{1 / n} e^{i \paren {\theta + 2 \pi k} / n}: k \in \set {0, 1, 2, \ldots, n - 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = z^{1 / n}
      | r = \paren {r e^{i \theta} }^{1 / n}
      | c = {{Defof|Exponential Form of Complex Number}}
}}
{{eqn | r = \paren {r \paren {\cos x + i \sin x} }^{1 / n}
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = \set {r^{1 / n} \paren {\cos \paren {\dfrac {\theta + 2 \pi k} n} + i \sin \paren {\dfrac {\theta + 2 \pi k} n} }: k \in \set {0, 1, 2, \ldots, n - 1} }
      | c = Roots of Complex Number
}}
{{eqn | r = \set {r^{1 / n} e^{i \paren {\theta + 2 \pi k} / n}: k \in \set {0, 1, 2, \ldots, n - 1} }
      | c = {{Defof|Exponential Form of Complex Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Z/(m)-Module Associated with Ring of Characteristic m

Let $\struct {R, +, *}$ be a ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let the characteristic of $R$ be $m$.
Let $\struct {\Z_m, +_m, \times_m}$ be the ring of integers modulo $m$.
Let $\circ$ be the mapping from $\Z_m \times R$ to $R$ defined as:
:$\forall \eqclass a m \in \Z_m: \forall x \in R: \eqclass a m \circ x = a \cdot x$
where $\eqclass a m$ is the residue class of $a$ modulo $m$ and $a \cdot x$ is the $a$th power of $x$.
Then $\struct {R, +, \circ}_{\Z_m}$ is a unitary $\Z_m$-module.

Proof:
Let us verify that the definition of $\circ$ is well-defined.
Let $\eqclass a m = \eqclass b m$.
Then we need to show that:
:$\forall x \in R: \eqclass a m \circ x = \eqclass b m \circ x$
By the definition of congruence:
:$\eqclass a m = \eqclass b m \iff \exists k \in \Z : a = b + k m$
Then:
{{begin-eqn}}
{{eqn | l = \eqclass a m \circ x
      | r = a \cdot x
      | c = Definition of $\circ$
}}
{{eqn | r = \paren {b + k m} \cdot x
}}
{{eqn | r = b \cdot x + k m \cdot x
      | c = Powers of Group Elements: Sum of Indices
}}
{{eqn | r = b \cdot x + k \cdot \paren {m \cdot x}
      | c = Powers of Group Elements: Product of Indices
}}
{{eqn | r = b \cdot x + k \cdot 0_R
      | c = Characteristic times Ring Element is Ring Zero
}}
{{eqn | r = b \cdot x + 0_R
      | c = Power of Identity is Identity
}}
{{eqn | r = b \cdot x
}}
{{eqn | r = \eqclass b m \circ x
      | c = Definition of $\circ$
}}
{{end-eqn}}
Thus, the definition of $\circ$ is well-defined.
{{qed|lemma}}
Let us verify that $\struct {R, +, \circ}_{\Z_m}$ is a unitary $\Z_m$-module by verifying the axioms in turn.
Theorem: Sum of Squares of Hyperbolic Secant and Tangent

:$\sech^2 x + \tanh^2 x = 1$
where $\sech$ and $\tanh$ are hyperbolic secant and hyperbolic tangent.

Proof:
{{begin-eqn}}
{{eqn | l = \sech^2 x + \tanh^2 x
      | r = \paren {\frac 2 {e^x + e^{-x} } }^2 + \tanh^2 x
      | c = {{Defof|Hyperbolic Secant|index = 1}}
}}
{{eqn | r = \paren {\frac 2 {e^x + e^{-x} } }^2 + \paren {\frac {e^x - e^{-x} } {e^x + e^{-x} } }^2  
      | c = {{Defof|Hyperbolic Tangent|index = 1}}
}}
{{eqn | r = \frac {4 + e^{2 x} - 2 + e^{-2 x} } {e^{2 x} + 2 + e ^{-2 x} }
      | c = Exponent Combination Laws
}}
{{eqn | r = \frac {e^{2 x} + 2 + e ^{-2 x} } {e^{2 x} + 2 + e ^{-2 x} }
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Squares of Hyperbolic Cotangent and Cosecant

:$\coth^2 x - \csch^2 x = 1$
where $\coth$ and $\csch$ are hyperbolic cotangent and hyperbolic cosecant.

Proof:
{{begin-eqn}}
{{eqn | l = \coth^2 x - \csch^2 x
      | r = \paren {\frac {e^x + e^{-x} } {e^x - e^{-x} } }^2 - \csch^2 x
      | c = {{Defof|Hyperbolic Cotangent|index = 1}}
}}
{{eqn | r = \paren {\frac {e^x + e^{-x} } {e^x - e^{-x} } }^2 - \paren {\frac 2 {e^x - e^{-x} } }^2
      | c = {{Defof|Hyperbolic Cosecant|index = 1}}
}}
{{eqn | r = \frac {e^{2 x} + 2 + e^{-2 x} - 4} {e^{2 x} - 2 + e ^{-2 x} }
      | c = Exponent Combination Laws
}}
{{eqn | r = \frac {e^{2 x} - 2 + e ^{-2 x} } {e^{2 x} - 2 + e ^{-2 x} }
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cosecant Function is Odd

Let $\csch: \C \to \C$ be the hyperbolic cosecant function on the set of complex numbers.
Then $\csch$ is odd:
:$\map \csch {-x} = -\csch x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \csch {-x}
      | r = \frac 1 {\map \sinh {-x} } 
      | c = {{Defof|Hyperbolic Cosecant|index = 2}}
}}
{{eqn | r = \frac 1 {-\sinh x}
      | c = Hyperbolic Sine Function is Odd
}}
{{eqn | r = -\csch x
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Secant Function is Even

:$\map \sech {-x} = \sech x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \sech {-x}
      | r = \frac 1 {\map \cosh {-x} } 
      | c = {{Defof|Hyperbolic Secant|index = 2}}
}}
{{eqn | r = \frac 1 {\cosh x} 
      | c = Hyperbolic Cosine Function is Even
}}
{{eqn | r = \sech x
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Secant Function is Even

:$\map \sech {-x} = \sech x$

Proof:
{{begin-eqn}}
{{eqn	| l = \sech \paren {-x}
	| r = \frac 1 {\cosh \paren {-x} }
	| c = {{Defof|Hyperbolic Secant}}
}}
{{eqn	| r = \frac 1 {\cos \paren {-i x} }
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn	| r = \frac 1 {\cos \paren {i x} }
	| c = Cosine Function is Even
}}
{{eqn	| r = \frac 1 {\cosh x}
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn	| r = \sech x
	| c = {{Defof|Hyperbolic Secant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cotangent Function is Odd

Let $\coth: \C \to \C$ be the hyperbolic cotangent function on the set of complex numbers.
Then $\coth$ is odd:
:$\map \coth {-x} = -\coth x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \coth {-x}
      | r = \frac {\map \cosh {-x} } {\map \sinh {-x} }
      | c = {{Defof|Hyperbolic Cotangent|index = 2}}
}}
{{eqn | r = \frac {\map \cosh {-x} }  {-\sinh x}
      | c = Hyperbolic Sine Function is Odd
}}
{{eqn | r = \frac {\cosh x} {-\sinh x}
      | c = Hyperbolic Cosine Function is Even
}}
{{eqn | r = -\coth x
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Sine of Sum

:$\map \sinh {a + b} = \sinh a \cosh b + \cosh a \sinh b$

Proof:
{{begin-eqn}}
{{eqn | l = \sinh a \cosh b + \cosh a \sinh b
      | r = \frac {e^a - e^{-a} } 2 \frac {e^b + e^{-b} } 2 + \frac {e^a + e^{-a} } 2 \frac {e^b - e^{-b} } 2
      | c = {{Defof|Hyperbolic Sine}} and {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac {e^{a + b} - e^{-a + b} + e^{a - b} - e^{-a - b} } 4 
      | c = Exponential of Sum
}}
{{eqn | o = 
      | ro= +
      | r = \frac {e^{a + b} + e^{-a + b} - e^{a - b} - e^{-a - b} } 4
      | c = 
}}
{{eqn | r = \frac {2 e^{a + b} - 2 e^{-\paren {a + b} } } 4
      | c = 
}}
{{eqn | r = \frac {e^{a + b} - e^{-\paren {a + b} } } 2
      | c = 
}}
{{eqn | r = \map \sinh {a + b}
      | c = {{Defof|Hyperbolic Sine}}
}}
{{end-eqn}}
{{qed}}