avewright/proofwiki-math huggingface dataset:
Theorem: Factorisation of x^(2n)-1 in Real Domain

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n} - 1 = \paren {z - 1} \paren {z + 1} \prod_{k \mathop = 1}^n \paren {z^2 - 2 \cos \dfrac {k \pi} n z + 1}$

Proof:
From Power of Complex Number minus 1:
:$\ds z^{2 n} - 1 = \prod_{k \mathop = 0}^{2 n - 1} \paren {z - \alpha^k}$
where:
{{begin-eqn}}
{{eqn | l = \alpha
      | r = e^{2 i \pi / \paren {2 n} }
      | c = 
}}
{{eqn | r = \cos \dfrac {2 \pi} {2 n} + i \sin \dfrac {2 \pi} {2 n}
      | c = 
}}
{{eqn | r = \cos \dfrac \pi n + i \sin \dfrac \pi n
      | c = 
}}
{{end-eqn}}
From Complex Roots of Unity occur in Conjugate Pairs:
:$U_{2 n} = \set {1, \tuple {\alpha, \alpha^{2 n - 1} }, \tuple {\alpha^2, \alpha^{2 n - 2} }, \ldots, \tuple {\alpha^k, \alpha^{2 n - k} }, \ldots, \tuple {\alpha^{n - 1}, \alpha^{n + 1} }, -1}$
where $U_{2 n}$ denotes the complex $2 n$th roots of unity:
:$U_{2 n} = \set {z \in \C: z^{2 n} = 1}$
The case $k = 0$ is taken care of by setting $\alpha^0 = 1$, from whence we have the factor $z - 1$.
The case $k = n$ is taken care of by setting $\alpha^k = -1$, from whence we have the factor $z + 1$.
Taking the product of each of the remaining factors of $z^{2 n} - 1$:
{{begin-eqn}}
{{eqn | l = \paren {z - \alpha^k} \paren {z - \alpha^{2 n - k} }
      | r = \paren {z - \alpha^k} \paren {z - \overline {\alpha^k} }
      | c = Complex Roots of Unity occur in Conjugate Pairs
}}
{{eqn | r = z^2 - z \paren {\alpha^k + \overline {\alpha^k} } + \alpha^k \overline {\alpha^k}
      | c = 
}}
{{eqn | r = z^2 - z \paren {\alpha^k + \overline {\alpha^k} } + \cmod {\alpha^k}^2
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = z^2 - z \paren {\alpha^k + \overline {\alpha^k} } + 1
      | c = Modulus of Complex Root of Unity equals 1
}}
{{eqn | r = z^2 - z \paren {\cos \dfrac {k \pi} n + i \sin \dfrac {k \pi} n + \cos \dfrac {k \pi} n - i \sin \dfrac {k \pi} n} + 1
      | c = Definition of $\alpha$
}}
{{eqn | r = z^2 - 2 \cos \dfrac {k \pi} n z + 1
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Factorisation of z^n-a

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Let $a \in \C$ be a complex number.
Then:
:$z^n - a = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \alpha^k b}$
where:
:$\alpha$ is a primitive complex $n$th root of unity
:$b$ is any complex number such that $b^n = a$.

Proof:
From $z^n - a = 0$ we have that:
:$a = z^n$
Let $b = a^{1 / n}$, hence $b^n = a$, with $a, b \in \C$.
From Roots of Complex Number:
{{begin-eqn}}
{{eqn | l = z^{1 / n}
      | r = \set {a^{1 / n} e^{i \paren {\theta + 2 k \pi} / n}: k \in \set {0, 1, 2, \ldots, n - 1}, \theta = \arg a}
      | c =
}}
{{eqn | r = \set {a^{1 / n} e^{2 i k \pi / n}: k \in \set {0, 1, 2, \ldots, n - 1} }
      | c = $\theta = 0$
}}
{{eqn | r = \set {b e^{2 i k \pi / n}: k \in \set {0, 1, 2, \ldots, n - 1} }
      | c = $b = a^{1 / n}$
}}
{{end-eqn}}
and so each of $b e^{2 i k \pi / n}$ is a root of $z^n - a$.
From First Complex Root of Unity is Primitive:
For each $n \in \Z_{>0}$ there exists at least one primitive complex $n$th root of unity, $\alpha$, hence each of $b \alpha^k$ is a unique root of $z^n - a$.
From the corollary to the Polynomial Factor Theorem:
If $\zeta_1, \zeta_2, \ldots, \zeta_n \in \C$ such that all are different, and $\map P {\zeta_1} = \map P {\zeta_2} = \cdots = \map P {\zeta_n} = 0$, then:
:$\ds \map P z = k \prod_{j \mathop = 1}^n \paren {z - \zeta_j}$
where $k \in \C$.
$z^n - a$ is a monic polynomial, hence $k = 1$ in the above product.
Choose $\zeta_j = b \alpha^{j - 1}$ and we have the desired result.
{{qed}}
Theorem: Triple Angle Formulas/Cosine/2 cos 3 theta + 1

:$2 \cos 3 \theta + 1 = \paren {\cos \theta - \cos \dfrac {2 \pi} 9} \paren {\cos \theta - \cos \dfrac {4 \pi} 9} \paren {\cos \theta - \cos \dfrac {8 \pi} 9}$

Proof:
{{begin-eqn}}
{{eqn | l = z^6 + z^3 + 1
      | r = \paren {z^2 - 2 z \cos \dfrac {2 \pi} 9 + 1} \paren {z^2 - 2 z \cos \dfrac {4 \pi} 9 + 1} \paren {z^2 - 2 z \cos \dfrac {8 \pi} 9 + 1}
      | c = Complex Algebra Examples: $z^6 + z^3 + 1$
}}
{{eqn | ll= \leadsto
      | l = z^3 + z^0 + z^{-3}
      | r = \paren {z - 2 \cos \dfrac {2 \pi} 9 + z^{-1} } \paren {z - 2 \cos \dfrac {4 \pi} 9 + z^{-1} } \paren {z - 2 \cos \dfrac {8 \pi} 9 + z^{-1} }
      | c = 
}}
{{end-eqn}}
Setting $z = e^{i \theta}$:
{{begin-eqn}}
{{eqn | l = e^{3 i \theta} + 1 + e^{-3 i \theta}
      | r = \paren {e^{i \theta} - 2 \cos \dfrac {2 \pi} 9 + e^{-i \theta} } \paren {e^{i \theta} - 2 \cos \dfrac {4 \pi} 9 + e^{-i \theta} } \paren {e^{i \theta} - 2 \cos \dfrac {8 \pi} 9 + e^{-i \theta} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \dfrac {e^{3 i \theta} + e^{-3 i \theta} } 2 + 1
      | r = \paren {2 \dfrac {e^{i \theta} + e^{-i \theta} } 2 - 2 \cos \dfrac {2 \pi} 9} \paren {2 \dfrac {e^{i \theta} + e^{-i \theta} } 2 - 2 \cos \dfrac {4 \pi} 9} \paren {2 \dfrac {e^{i \theta} + e^{-i \theta} } 2 - 2 \cos \dfrac {8 \pi} 9}
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = 2 \cos 3 \theta + 1
      | r = \paren {2 \cos \theta - 2 \cos \dfrac {2 \pi} 9} \paren {2  \cos \theta - 2 \cos \dfrac {4 \pi} 9} \paren {2 \cos \theta - 2 \cos \dfrac {8 \pi} 9}
      | c = Euler's Cosine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of 144 Degrees

:$\cos 144 \degrees = \cos \dfrac {4 \pi} 5 = -\dfrac \phi 2 = -\dfrac {1 + \sqrt 5} 4$

Proof:
{{begin-eqn}}
{{eqn | l = \cos 144 \degrees
      | r = \map \cos {180 \degrees - 36 \degrees}
      | c = 
}}
{{eqn | r = -\cos 36 \degrees
      | c = Cosine of Supplementary Angle
}}
{{eqn | r = -\dfrac {1 + \sqrt 5} 4
      | c = {{cos|36}}
}}
{{end-eqn}}
{{qed}}
Category:Cosine Function
ge3xtunhsntyfh7t8q3jydddxp8hf7f
Theorem: Sine of 144 Degrees

:$\sin 144 \degrees = \cos \dfrac {4 \pi} 5 = \sqrt {\dfrac 5 8 - \dfrac {\sqrt 5} 8}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin 144 \degrees
      | r = \sin \paren {180 \degrees - 36 \degrees}
      | c = 
}}
{{eqn | r = \sin 36 \degrees
      | c = Sine of Supplementary Angle
}}
{{eqn | r = \sqrt {\dfrac 5 8 - \dfrac {\sqrt 5} 8}
      | c = Sine of $36 \degrees$
}}
{{end-eqn}}
{{qed}}
Category:Sine Function
4fz8zck3sk6pp1v6vules5zy4kohf9u
Theorem: Cube Root of Unity if Modulus is 1 and Real Part is Minus Half

Let $z \in \C$ be a complex number such that:
:$\cmod z = 1$
:$\Re \paren z = -\dfrac 1 2$
where:
:$\cmod z$ denotes the complex modulus of $z$
:$\Re \paren z$ denotes the real part of $z$.
Then:
:$z^3 = 1$

Proof:
Let $z = x + i y$.
From $\Re \paren z = -\dfrac 1 2$:
:$x = -\dfrac 1 2$
by definition of the real part of $z$.
Then:
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2 + y^2
      | r = 1
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | ll= \leadsto
      | l = \paren {-\dfrac 1 2}^2 + y^2
      | r = 1
      | c = substituting for $x$
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \sqrt {1 - \dfrac 1 4}
      | c = simplifying
}}
{{eqn | r = \pm \dfrac {\sqrt 3} 2
      | c = 
}}
{{end-eqn}}
Thus:
:$z = -\dfrac 1 2 \pm \dfrac {\sqrt 3} 2$
and the result follows from Cube Roots of Unity.
{{qed}}
Theorem: Sum of Two Cubes in Complex Domain

:$a^3 + b^3 = \paren {a + b} \paren {a \omega + b \omega^2} \paren {a \omega^2 + b \omega}$
where:
: $\omega = -\dfrac 1 2 + \dfrac {\sqrt 3} 2$

Proof:
From Sum of Cubes of Three Indeterminates Minus 3 Times their Product:
:$x^3 + y^3 + z^3 - 3 x y z = \paren {x + y + z} \paren {x + \omega y + \omega^2 z} \paren {x + \omega^2 y + \omega z}$
Setting $x \gets 0, y \gets a, z \gets b$:
:$0^3 + a^3 + b^3 - 3 \times 0 \times a b = \paren {0 + a + b} \paren {0 + \omega a + \omega^2 b} \paren {0 + \omega^2 a + \omega b}$
The result follows.
{{qed}}
Theorem: Three Times Sum of Cubes of Three Indeterminates Plus 6 Times their Product

:$3 \paren {a^3 + b^3 + c^3 + 6 a b c} = \paren {a + b + c}^3 + \paren {a + b \omega + c \omega^2}^3 + \paren {a + b \omega^2 + c \omega}^3$
where:
: $\omega = -\dfrac 1 2 + \dfrac {\sqrt 3} 2$

Proof:
Multiplying out:
{{begin-eqn}}
{{eqn | l = \paren {a + b + c}^3
      | r = \paren {a + b + c} \paren {a^2 + b^2 + c^2 + 2 a b + 2 a c + 2 b c}
      | c = 
}}
{{eqn | n = 1
      | r = a^3 + b^3 + c^3 + 3 a^2 b + 3 a^2 c + 3 a b^2 + 3 b^2 c + 3 a c^2 + 3 b c^2 + 6 a b c
      | c = 
}}
{{end-eqn}}
Replacing $b$ with $b \omega$ and $c$ with $c \omega^2$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \paren {a + b \omega + c \omega^2}^3
      | r = a^3 + b^3 \omega^3 + c^3 \omega^6 + 3 a^2 b \omega + 3 a^2 c \omega^2 + 3 a b^2 \omega^2 + 3 b^2 c \omega^4 + 3 a c^2 \omega^4 + 3 b c^2 \omega^5 + 6 a b c \omega^3
      | c = 
}}
{{eqn | n = 2
      | r = a^3 + b^3 + c^3 + 3 a^2 b \omega + 3 a^2 c \omega^2 + 3 a b^2 \omega^2 + 3 b^2 c \omega + 3 a c^2 \omega + 3 b c^2 \omega^2 + 6 a b c
      | c = as $\omega^3 = 1$
}}
{{end-eqn}}
Replacing $b$ with $b \omega^2$ and $c$ with $c \omega$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \paren {a + b \omega^2 + c \omega}^3
      | r = a^3 + b^3 \omega^6 + c^3 \omega^3 + 3 a^2 b \omega^2 + 3 a^2 c \omega + 3 a b^2 \omega^4 + 3 b^2 c \omega^5 + 3 a c^2 \omega^2 + 3 b c^2 \omega^4 + 6 a b c \omega^3
      | c = 
}}
{{eqn | n = 3
      | r = a^3 + b^3 + c^3 + 3 a^2 b \omega^2 + 3 a^2 c \omega + 3 a b^2 \omega + 3 b^2 c \omega^2 + 3 a c^2 \omega^2 + 3 b c^2 \omega + 6 a b c
      | c = as $\omega^3 = 1$
}}
{{end-eqn}}
Adding together $(1)$, $(2)$ and $(3)$:
{{begin-eqn}}
{{eqn | r = \paren {a + b + c}^3 + \paren {a + b \omega + c \omega^2}^3 + \paren {a + b \omega^2 + c \omega}^3
      | o = 
      | c = 
}}
{{eqn | r = a^3 + b^3 + c^3 + 3 a^2 b + 3 a^2 c + 3 a b^2 + 3 b^2 c + 3 a c^2 + 3 b c^2 + 6 a b c
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = a^3 + b^3 + c^3 + 3 a^2 b \omega + 3 a^2 c \omega^2 + 3 a b^2 \omega^2 + 3 b^2 c \omega + 3 a c^2 \omega + 3 b c^2 \omega^2 + 6 a b c
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = a^3 + b^3 + c^3 + 3 a^2 b \omega^2 + 3 a^2 c \omega + 3 a b^2 \omega + 3 b^2 c \omega^2 + 3 a c^2 \omega^2 + 3 b c^2 \omega + 6 a b c
      | c = 
}}
{{eqn | r = 3 \paren {a^3 + b^3 + c^3 + 6 a b c}
      | c = 
}}
{{eqn | o =
      | ro= +
      | r = \paren {3 a^2 b + 3 a^2 c + 3 a b^2 + 3 b^2 c + 3 a c^2 + 3 b c^2} \paren {1 + \omega + \omega^2}
      | c = 
}}
{{eqn | r = 3 \paren {a^3 + b^3 + c^3 + 6 a b c}
      | c = Sum of Cube Roots of Unity: $1 + \omega + \omega^2 = 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Roots of Complex Number/Examples/z^8 + 1 = 0

The roots of the polynomial:
:$z^8 + 1 = 0$
are:
:$\set {\cos \dfrac {\paren {2 k + 1} \pi} 8 + i \sin \dfrac {\paren {2 k + 1} \pi} 8: k \in \set {0, 1, \ldots, 7} }$

Proof:
{{begin-eqn}}
{{eqn | l = z^8 + 1
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z
      | r = \paren {-1}^{1/8}
      | c = 
}}
{{end-eqn}}
From Euler's Identity:
:$-1 = e^{i \pi}$
Let $b$ be defined as:
{{begin-eqn}}
{{eqn | l = b
      | r = \sqrt [8] 1 \paren {\cos \dfrac \pi 8 + i \sin \dfrac \pi 8}
      | c = 
}}
{{eqn | r = \cos \dfrac \pi 8 + i \sin \dfrac \pi 8
      | c = 
}}
{{end-eqn}}
From Roots of Complex Number: Corollary:
:$\paren {-1}^{1/8} = \cos \paren {\dfrac \pi 8 + \dfrac {2 k \pi} 8} + i \sin \paren {\dfrac \pi 8 + \dfrac {2 k \pi} 8}$
for $k = 0$ to $7$.
{{begin-eqn}}
{{eqn | l = \paren {-1}^{1/8}
      | r = \set {\cos \paren {\dfrac \pi 8 + \dfrac {2 k \pi} 8} + i \sin \paren {\dfrac \pi 8 + \dfrac {2 k \pi} 8}: k \in \set {0, 1, \ldots, 7} }
      | c = 
}}
{{eqn | r = \set {\cos \dfrac {\paren {2 k + 1} \pi} 8 + i \sin \dfrac {\paren {2 k + 1} \pi} 8: k \in \set {0, 1, \ldots, 7} }
      | c = 
}}
{{eqn | r = \set {\exp \dfrac {\paren {2 k + 1} i \pi} 8: k \in \set {0, 1, \ldots, 7} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Quadruple Angle Formulas/Cosine/Factor Form

:$\cos 4 \theta = \paren {\cos \theta - \cos \dfrac \pi 8} \paren {\cos \theta - \cos \dfrac {3 \pi} 8} \paren {\cos \theta - \cos \dfrac {5 \pi} 8} \paren {\cos \theta - \cos \dfrac {7 \pi} 8}$

Proof:
{{begin-eqn}}
{{eqn | l = z^8 + 1
      | r = \prod_{k \mathop = 0}^3 \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} 8 + 1}
      | c = Complex Algebra Examples: $z^8 + 1$
}}
{{eqn | ll= \leadsto
      | l = z^4 + z^{-4}
      | r = \prod_{k \mathop = 0}^3 \paren {z - 2 \cos \dfrac {\paren {2 k + 1} \pi} 8 + z^{-1} }
      | c = dividing both sides by $z^4$
}}
{{end-eqn}}
Setting $z = e^{i \theta}$:
{{begin-eqn}}
{{eqn | l = e^{4 i \theta} + e^{-4 i \theta}
      | r = \prod_{k \mathop = 0}^3 \paren {e^{i \theta} - 2 \cos \dfrac {\paren {2 k + 1} i \pi} 8 + e^{-i \theta} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \dfrac {e^{4 i \theta} + e^{-4 i \theta} } 2
      | r = \prod_{k \mathop = 0}^3 \paren {2 \frac {e^{i \theta} + e^{-i \theta} } 2 - 2 \cos \dfrac {\paren {2 k + 1} i \pi} 8}
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = 2 \cos 4 \theta
      | r = \prod_{k \mathop = 0}^3 \paren {2 \cos \theta - 2 \cos \dfrac {\paren {2 k + 1} i \pi} 8}
      | c = Euler's Cosine Identity
}}
{{eqn | ll= \leadsto
      | l = \cos 4 \theta
      | r = \prod_{k \mathop = 0}^3 \paren {\cos \theta - \cos \dfrac {\paren {2 k + 1} i \pi} 8}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Factorisation of z^n+1

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$z^n + 1 = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} n}$

Proof:
From Factorisation of $z^n - a$, setting $a = -1$:
:$z^n + 1 = \ds \prod_{k \mathop = 0}^{n - 1} \paren {z - \alpha^k b}$
where:
:$\alpha$ is a primitive complex $n$th root of unity
:$b$ is any complex number such that $b^n = a$.
From Euler's Identity:
:$-1 = e^{i \pi}$
From Exponential of Product:
:$\paren {\exp \dfrac {i \pi} n}^n = e^{i \pi}$
and so:
:$b = \exp \dfrac {i \pi} n$
We also have by definition of the first complex $n$th root of unity, and from First Complex Root of Unity is Primitive:
:$\alpha = \exp \dfrac {2 i \pi} n$
Hence:
{{begin-eqn}}
{{eqn | l = z^n + 1
      | r = \prod_{k \mathop = 0}^{n - 1} \paren {z - \paren {\exp \dfrac {2 i \pi} n}^k \exp \dfrac {i \pi} n}
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {2 k i \pi} n \exp \dfrac {i \pi} n}
      | c = Exponential of Product
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} n}
      | c = Exponential of Sum
}}
{{end-eqn}}
{{qed}}
Category:Algebra
Category:Complex Roots
di7cjw7t8yiavxx44urhidhgk4wb29z
Theorem: Combination Theorem for Cauchy Sequences/Quotient Rule

Suppose $\sequence {y_n}$ does not converge to $0$.
Then:
:$\exists K \in \N: \forall n > K : y_n \ne 0$
and the sequences:
:$\sequence { {x_{K + n} } \paren {y_{K + n} }^{-1} }_{n \mathop \in \N}$ and $\sequence {\paren {y_{K + n} }^{-1} {x_{K + n} } }_{n \mathop \in \N}$ are well-defined and Cauchy sequences.

Proof:
By the Inverse Rule for Normed Division Ring:
:$\exists K \in \N : \forall n > K : y_n \ne 0$.
and the sequence:
:$\sequence {\paren {x_{K + n} }^{-1} }_{n \mathop \in \N}$ is well-defined and a Cauchy sequence.
By Subsequence of Cauchy Sequence in Normed Division Ring is Cauchy Sequence, $\sequence {x_{K + n} }_{n \mathop \in \N}$ is a Cauchy sequence.
By Product Rule for Normed Division Ring Sequences:
:the sequences $\sequence { {x_{K + n} } \paren {y_{K + n} }^{-1} }_{n \mathop \in \N}$ and $\sequence {\paren {y_{K + n} }^{-1} {x_{K + n} } }_{n \mathop \in \N}$ are Cauchy sequences.
{{qed}}
Theorem: Factorisation of z^(2n)+1 in Real Domain

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n} + 1 = \prod_{k \mathop = 1}^n \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} {2 n} + 1}$

Proof:
From Factorisation of $z^n + 1$:
:$(1): \ds \quad z^{2 n} + 1 = \prod_{k \mathop = 0}^{2 n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n} }$
From Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs, the roots of $(1)$ occur in conjugate pairs.
Hence we can express $(1)$ as:
{{begin-eqn}}
{{eqn | l = z^{2 n} + 1
      | r = \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n} } \prod_{k \mathop = n}^{2 n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n} }
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n} } \paren {z - \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n} }
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - z \paren {\exp \dfrac {\paren {2 k + 1} i \pi} {2 n} + \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n} } + \exp \dfrac {\paren {2 k + 1} i \pi} {2 n} \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n} }
      | c = 
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - z \paren {\exp \dfrac {\paren {2 k + 1} i \pi} {2 n} + \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n} } + 1}
      | c = simplifying
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - z \paren {\cos \dfrac {\paren {2 k + 1} \pi} {2 n} + i \sin \dfrac {\paren {2 k + 1} \pi} {2 n} + \cos \dfrac {\paren {2 k + 1} \pi} {2 n} - i \sin \dfrac {\paren {2 k + 1} \pi} {2 n} } + 1}
      | c = Euler's Formula
}}
{{eqn | r = \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} {2 n} + 1}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Factorisation of z^(2n+1)+1 in Real Domain

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
:$\ds z^{2 n + 1} + 1 = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} {2 n + 1} + 1}$

Proof:
From Factorisation of $z^n + 1$:
:$(1): \quad \ds z^{2 n + 1} + 1 = \prod_{k \mathop = 0}^{2 n} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} }$
From Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs, the roots of $(1)$ occur in conjugate pairs.
Hence we can express $(1)$ as:
{{begin-eqn}}
{{eqn | l = z^{2 n + 1} + 1
      | r = \prod_{k \mathop = 0}^n \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} } \prod_{k \mathop = n + 1}^{2 n} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} }
      | c = 
}}
{{eqn | r = \paren {z - \exp \dfrac {\paren {2 n + 1} i \pi} {2 n + 1} } \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} } \prod_{k \mathop = n + 1}^{2 n} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} }
      | c = 
}}
{{eqn | r = \paren {z - e^{i \pi} } \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} } \prod_{k \mathop = n + 1}^{2 n} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} }
      | c = 
}}
{{eqn | r = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} } \paren {z - \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n + 1} }
      | c = 
}}
{{eqn | r = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - z \paren {\exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} + \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n + 1} } + \exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n + 1} }
      | c = 
}}
{{eqn | r = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - z \paren {\exp \dfrac {\paren {2 k + 1} i \pi} {2 n + 1} + \exp \dfrac {-\paren {2 k + 1} i \pi} {2 n + 1} } + 1}
      | c = simplifying
}}
{{eqn | r = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - z \paren {\cos \dfrac {\paren {2 k + 1} \pi} {2 n + 1} + i \sin \dfrac {\paren {2 k + 1} \pi} {2 n + 1} + \cos \dfrac {\paren {2 k + 1} \pi} {2 n + 1} - i \sin \dfrac {\paren {2 k + 1} \pi} {2 n + 1} } + 1}
      | c = Euler's Formula
}}
{{eqn | r = \paren {z + 1} \prod_{k \mathop = 0}^{n - 1} \paren {z^2 - 2 z \cos \dfrac {\paren {2 k + 1} \pi} {2 n + 1} + 1}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Roots of Complex Number/Examples/z^5 + 1 = 0

The roots of the polynomial:
:$z^5 + 1 = 0$
are:
:$\set {\cos \dfrac \pi 5 \pm i \sin \dfrac \pi 5, \cos \dfrac {3 \pi} 5 \pm i \sin \dfrac {3 \pi} 5, -1}$

Proof:
From Factorisation of $z^n + 1$:
:$z^5 + 1 = \ds \prod_{k \mathop = 0}^4 \paren {z - \exp \dfrac {\paren {2 k + 1} i \pi} 5}$
Thus:
:$z = \set {\exp \dfrac {\paren {2 k + 1} i \pi} 5}$
{{begin-eqn}}
{{eqn | n = k = 0
      | l = z
      | r = \cos \dfrac \pi 5 + i \sin \dfrac \pi 5
      | c = 
}}
{{eqn | n = k = 1
      | l = z
      | r = \cos \dfrac {3 \pi} 5 + i \sin \dfrac {3 \pi} 5
      | c = 
}}
{{eqn | n = k = 2
      | l = z
      | r = \cos \dfrac {5 \pi} 5 + i \sin \dfrac {5 \pi} 5
      | c = 
}}
{{eqn | r = \cos \pi + i \sin \pi
      | c = 
}}
{{eqn | r = -1
      | c = Euler's Identity
}}
{{eqn | n = k = 3
      | l = z
      | r = \cos \dfrac {7 \pi} 5 + i \sin \dfrac {7 \pi} 5
      | c = 
}}
{{eqn | r = \cos \dfrac {-3 \pi} 5 + i \sin \dfrac {-3 \pi} 5
      | c = 
}}
{{eqn | r = \cos \dfrac {3 \pi} 5 - i \sin \dfrac {3 \pi} 5
      | c = 
}}
{{eqn | n = k = 4
      | l = z
      | r = \cos \dfrac {9 \pi} 5 + i \sin \dfrac {9 \pi} 5
      | c = 
}}
{{eqn | r = \cos \dfrac {-\pi} 5 + i \sin \dfrac {-\pi} 5
      | c = 
}}
{{eqn | r = \cos \dfrac \pi 5 - i \sin \dfrac \pi 5
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 4 Sine Pi over 10 by Cosine Pi over 5

:$4 \sin \dfrac \pi {10} \cos \dfrac \pi 5 = 1$

Proof:
{{begin-eqn}}
{{eqn | l = 4 \sin \theta \cos 2 \theta
      | r = 1
      | c = Solve for $\theta$
}}
{{eqn | l = 4 \sin \theta \cos \theta \cos 2\theta
      | r = \cos \theta
      | c = multiplying both sides by $\cos \theta$
}}
{{eqn | l = 2 \paren {2 \sin \theta \cos \theta } \cos 2\theta
      | r = \cos \theta
      | c = factoring out $2$
}}
{{eqn | l = 2 \paren {\sin 2 \theta } \cos 2\theta
      | r = \cos \theta
      | c = Double Angle Formula for Sine
}}
{{eqn | l = \sin 4 \theta
      | r = \cos \theta
      | c = Double Angle Formula for Sine
}}
{{eqn | l = \map \sin {\frac \pi 2 - \theta}
      | r = \cos \theta
      | c = Sine of Complement equals Cosine
}}
{{eqn | l = \paren {\frac \pi 2 - \theta}
      | r = 4 \theta
      | c =
}}
{{eqn | l = \theta
      | r = \frac \pi {10}
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Convergence of Modulus of Convergent Complex Sequence

Let $\sequence {z_n}$ be a sequence in $\C$.
Let $\sequence {z_n}$ converge to a value $c \in \C$.
Let $\cmod z$ denote the modulus of a complex number $z$.
Then:
:$\sequence {\cmod {z_n} }$ converges to a value $\cmod c$.

Proof:
By definition of convergent complex sequence:
:$\forall \epsilon \in \R_{>0}: \exists N \in \R: n > N \implies \cmod {z_n - c} < \epsilon$
From the Reverse Triangle Inequality:
:$\size {\cmod x - \cmod y} \le \cmod {x - y}$
and the result follows.
{{qed}}
Theorem: Combination Theorem for Sequences/Real/Difference Rule

:$\ds \lim_{n \mathop \to \infty} \paren {x_n - y_n} = l - m$

Proof:
From Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {x_n + y_n} = l + m$
From Multiple Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {-y_n} = -m$
Hence:
:$\ds \lim_{n \mathop \to \infty} \paren {x_n + \paren {-y_n} } = l + \paren {-m}$
The result follows.
{{qed}}