avewright/proofwiki-math huggingface dataset:
Theorem: Newton-Girard Identities/Lemma 2

{{begin-eqn}}
{{eqn | l = \map \ln {\map G z}
      | r = \sum_{k \mathop \ge 1} \paren {-1}^{k + 1} \dfrac {S_k z^k} k
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \map G z
      | r = \paren {1 + x_a z} \paren {1 + x_{a + 1} z} \cdots \paren {1 + x_b z}
      | c = Lemma 1
}}
{{eqn | ll= \leadsto
      | l = \map \ln {\map G z}
      | r = \map \ln {1 + x_a z} + \map \ln {1 + x_{a + 1} z} + \cdots + \map \ln {1 + x_b z}
      | c = Sum of Logarithms
}}
{{eqn | r = \paren {\sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k + 1} {x_a}^k z^k} k} + \paren {\sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k + 1} {x_{a + 1} }^k z^k} k} + \cdots + \paren {\sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k + 1} {x_b}^k z^k} k}
      | c = Power Series Expansion for Logarithm of 1 + x
}}
{{eqn | r = \sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k + 1} z^k} k \paren { {x_a}^k + {x_{a + 1} }^k + \cdots + {x_b}^k}
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k + 1} z^k} k \sum_{j \mathop = a}^b {x_j}^k
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k + 1} S_k z^k} k
      | c = Definition of $S_k$
}}
{{end-eqn}}
{{qed}}
Category:Newton-Girard Identities
rr1amvbxfqv1nerscs6rhaojdsq74eg
Theorem: Newton-Girard Identities/Examples/Order 2

:$\ds \sum_{a \mathop \le i \mathop < j \mathop \le b} x_i x_j = \dfrac 1 2 \paren {\paren {\sum_{i \mathop = a}^b x_i}^2 - \paren {\sum_{i \mathop = a}^b {x_i}^2} }$

Proof:
From Newton-Girard Identities:
:$\ds \sum_{a \mathop \le j_1 \mathop < \cdots \mathop < j_m \mathop \le b} x_{j_1} \cdots x_{j_m} = \sum_{\substack {k_1, k_2, \ldots, k_m \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + \mathop \cdots \mathop + m k_m \mathop = m} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !} \cdots \dfrac {\paren {\paren {-1}^{m + 1} S_m}^{k_m} } {m^{k_m} k_m !}$
where:
:$S_r = \ds \sum_{k \mathop = a}^b {x_k}^r$ for $r \in \Z_{\ge 0}$.
Setting $m = 2$, and setting $x_i := x_{j_1}, x_j := x_{j_2}$:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le i \mathop < j \mathop \le b} x_{j_1} x_{j_2}
      | r = \sum_{\substack {k_1, k_2 \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop = 2} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !}
      | c = 
}}
{{eqn | r = \dfrac { {S_1}^2 \paren {-S_2}^0} {\paren {1^2 \times 2!} \paren {2^0 \times 0!} } + \dfrac { {S_1}^0 \paren {-S_2}^1} {\paren {1^0 \times 0!} \paren {2^1 \times 1!} }
      | c = as $k_1 = 2, k_2 = 0$ and $k_1 = 0, k_2 = 1$ are the only $k_1$ and $k_2$ to fulfil the criteria
}}
{{eqn | r = \frac 1 2 \paren { {S_1}^2 - S_2}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Newton-Girard Identities/Examples/Order 3

:$\ds \sum_{a \mathop \le i \mathop < j \mathop < k \mathop \le b} x_i x_j x_k = \dfrac { {S_1}^3} 6 - \dfrac {S_1 S_2} 2 + \dfrac {S_3} 3$
where:
:$\ds S_r := \sum_{k \mathop = a}^b {x_k}^r$

Proof:
From Newton-Girard Identities:
:$\ds \sum_{a \mathop \le j_1 \mathop < \cdots \mathop < j_m \mathop \le b} x_{j_1} \cdots x_{j_m} = \sum_{\substack {k_1, k_2, \ldots, k_m \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + \mathop \cdots \mathop + m k_m \mathop = m} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !} \dfrac { {S_3}^{k_3} } {3^{k_3} k_3 !} \cdots \dfrac {\paren {\paren {-1}^{m + 1} S_m}^{k_m} } {m^{k_m} k_m !}$
where:
:$S_r = \ds \sum_{k \mathop = a}^b {x_k}^r$ for $r \in \Z_{\ge 0}$.
Setting $m = 3$, and setting $x_i := x_{j_1}, x_j := x_{j_2}, x_k := x_{j_3}$:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop < j_1 \mathop < j_2 \mathop < j_3 \mathop \le b} x_{j_1} x_{j_2} x_{j_3}
      | r = \sum_{\substack {k_1, k_2, k_3 \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + 3 k_3 \mathop = 3} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !} \dfrac { {S_3}^{k_3} } {3^{k_3} k_3 !}
      | c = 
}}
{{end-eqn}}
We need to find all sets of $k_1, k_2, k_3 \in \Z_{\ge 0}$ such that:
:$k_1 + 2 k_2 + 3 k_3 = 3$
Thus $\tuple {k_1, k_2, k_3}$ can be:
:$\tuple {3, 0, 0}$
:$\tuple {1, 1, 0}$
:$\tuple {0, 0, 1}$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le j_3 \mathop \le b} x_{j_1} x_{j_2} x_{j_3}
      | r = \dfrac { {S_1}^3 \paren {-S_2}^0 {S_3}^0} {\paren {1^3 \times 3!} \paren {2^0 \times 0!} \paren {3^0 \times 0!} } + \dfrac { {S_1}^1 \paren {-S_2}^1 {S_3}^0} {\paren {1^1 \times 1!} \paren {2^1 \times 1!} \paren {3^0 \times 0!} } + \dfrac { {S_1}^0 \paren {-S_2}^0 {S_3}^1} {\paren {1^0 \times 0!} \paren {2^0 \times 0!} \paren {3^1 \times 1!} }
      | c = 
}}
{{eqn | r = \dfrac { {S_1}^3} 6 - \dfrac {S_1 S_2} 2 + \dfrac {S_3} 3
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Newton-Girard Identities/Examples/Order 4

:$\ds \sum_{a \mathop \le j_1 \mathop < j_2 \mathop < j_3 \mathop < j_4 \mathop \le b} x_{j_1} x_{j_2} x_{j_3} x_{j_4} = \dfrac { {S_1}^4} {24} - \dfrac { {S_1}^2 S_2} 4 + \dfrac { {S_2}^2} 8 + \dfrac {S_1 S_3} 3 - \dfrac {S_4} 4$
where:
:$\ds S_r := \sum_{k \mathop = a}^b {x_k}^r$.

Proof:
From Newton-Girard Identities:
:$\ds \sum_{a \mathop \le j_1 \mathop < \mathop \cdots \mathop < j_m \mathop \le b} x_{j_1} \cdots x_{j_m} = \sum_{\substack {k_1, k_2, \ldots, k_m \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + \mathop \cdots \mathop + m k_m \mathop = m} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !} \dfrac { {S_3}^{k_3} } {3^{k_3} k_3 !} \cdots \dfrac {\paren {\paren {-1}^{m + 1} S_m}^{k_m} } {m^{k_m} k_m !}$
where:
:$S_j = \ds \sum_{k \mathop = a}^b {x_k}^j$ for $j \in \Z_{\ge 0}$.
Setting $m = 4$:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le j_1 \mathop < j_2 \mathop < j_3 \mathop < j_4 \mathop \le b} x_{j_1} x_{j_2} x_{j_3} x_{j_4}
      | r = \sum_{\substack {k_1, k_2, k_3, k_4 \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + 3 k_3 \mathop + 4 k_4 \mathop = 4} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !} \dfrac { {S_3}^{k_3} } {3^{k_3} k_3 !} \dfrac {\paren {-S_4}^{k_4} } {4^{k_4} k_4 !}
      | c = 
}}
{{end-eqn}}
We need to find all ordered quadruples of $k_1, k_2, k_3, k_4 \in \Z_{\ge 0}$ such that:
:$k_1 + 2 k_2 + 3 k_3 + 4 k_4 = 4$
Thus $\tuple {k_1, k_2, k_3, k_4}$ can be:
:$\tuple {4, 0, 0, 0}$
:$\tuple {2, 1, 0, 0}$
:$\tuple {0, 2, 0, 0}$
:$\tuple {1, 0, 1, 0}$
:$\tuple {0, 0, 0, 1}$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le j_1 \mathop \le j_2 \mathop \le j_3 \mathop \le b} x_{j_1} x_{j_2} x_{j_3}
      | r = \dfrac { {S_1}^4 \paren {-S_2}^0 {S_3}^0 \paren {-S_4}^0} {\paren {1^4 \times 4!} \paren {2^0 \times 0!} \paren {3^0 \times 0!} \paren {4^0 \times 0!} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \dfrac { {S_1}^2 \paren {-S_2}^1 {S_3}^0 \paren {-S_4}^0} {\paren {1^2 \times 2!} \paren {2^1 \times 1!} \paren {3^0 \times 0!} \paren {4^0 \times 0!} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \dfrac { {S_1}^0 \paren {-S_2}^2 {S_3}^0 \paren {-S_4}^0} {\paren {1^0 \times 0!} \paren {2^2 \times 2!} \paren {3^0 \times 0!} \paren {4^0 \times 0!} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \dfrac { {S_1}^1 \paren {-S_2}^0 {S_3}^1 \paren {-S_4}^0} {\paren {1^1 \times 1!}\ \paren {2^0 \times 0!} \paren {3^1 \times 1!} \paren {4^0 \times 0!} }
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = \dfrac { {S_1}^0 \paren {-S_2}^0 {S_3}^0 \paren {-S_4}^1} {\paren {1^0 \times 0!} \paren {2^0 \times 0!} \paren {3^0 \times 0!} \paren {4^1 \times 1!} }
      | c = 
}}
{{eqn | r = \dfrac { {S_1}^4} {24} - \dfrac { {S_1}^2 S_2} 4 + \dfrac { {S_2}^2} 8 + \dfrac {S_1 S_3} 3 - \dfrac {S_4} 4
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Newton-Girard Identities/Examples/Order 1

:$\ds \sum_{a \mathop \le i \mathop \le b} x_i = S_1$
where:
:$\ds S_r := \sum_{k \mathop = a}^b {x_k}^r$

Proof:
From Newton-Girard Identities:
:$\ds \sum_{a \mathop \le j_1 \mathop < \cdots \mathop < j_m \mathop \le b} x_{j_1} \cdots x_{j_m} = \sum_{\substack {k_1, k_2, \ldots, k_m \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop + \mathop \cdots \mathop + m k_m \mathop = m} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !} \dfrac {\paren {-S_2}^{k_2} } {2^{k_2} k_2 !} \cdots \dfrac {\paren {\paren {-1}^{m + 1} S_m}^{k_m} } {m^{k_m} k_m !}$
where:
:$S_r = \ds \sum_{k \mathop = a}^b {x_k}^r$ for $r \in \Z_{\ge 0}$.
Setting $m = 1$, and setting $x_i := x_{j_1}$:
{{begin-eqn}}
{{eqn | l = \sum_{a \mathop \le i \mathop \le b} x_{j_1}
      | r = \sum_{\substack {k_1, k_2 \mathop \ge 0 \\ k_1 \mathop + 2 k_2 \mathop = 2} } \dfrac { {S_1}^{k_1} } {1^{k_1} k_1 !}
      | c = 
}}
{{eqn | r = \dfrac { {S_1}^1} {1^1 \times 1!} 
      | c = as $k_1 = 1$ is the only $k_1$ to fulfil the criteria
}}
{{eqn | r = S_1
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Newton-Girard Identities

Let $X$ be a set of $n$ numbers $\set {x_1, x_2, \ldots, x_n}$.
Define:
{{begin-eqn}}
{{eqn | l = \mathbf S_m 
      | r = \set {\paren {j_1, \ldots, j_m} : 1 \le j_1 < \cdots < j_m \le n}
      | c = $1 \le m \le n$
}}
{{eqn | l = \map {e_m} X
      | r = \begin {cases} 1 & : m = 0 \\ \ds \sum_{\mathbf S_m} x_{j_1} \cdots x_{j_m} & : 1 \le m \le n \\ 0 & : m > n \\ \end {cases}
      | c = {{Defof|Elementary Symmetric Function}}
}}
{{eqn | l = \map {p_k} X
      | r = \begin{cases} n & : k = 0 \\ \ds \sum_{i \mathop = 1}^n  x_i^k & : k \ge 1 \end {cases}
      | c = {{Defof|Power Sum}}
}}
{{end-eqn}}
The '''Newton-Girard Identities''' are:
{{begin-eqn}}
{{eqn | n = 1
      | l = k \map {e_k} X
      | r = \sum_{i \mathop = 1}^k \paren {-1}^{i - 1} \map {e_{k - i} } X \map {p_i} X
      | c = for $1 \le k \le n$
}}
{{eqn | n = 2
      | l = 0
      | r = \sum_{i \mathop = k - n}^k \paren {-1}^{i - 1} \map {e_{k - i} } X \map {p_i} X
      | c = for $1 \le n < k$
}}
{{end-eqn}}

Proof:
=== Outline ===
The proof is divided into three cases: $k < n$, $k = n$ and $k > n$.
The tools are Viète's Formulas, Recursion Property of Elementary Symmetric Function, telescoping sums and  homogeneous functions of degree $k$.
Theorem: Summation of Products of n Numbers taken m at a time with Repetitions/Inverse Formula

Let $S_m$ be expressed in the form:
:$S_m = \ds \sum_{k_1 \mathop + 2 k_2 \mathop + \mathop \cdots \mathop + m k_m \mathop = m} A_m {h_1}^{k_1} {h_2}^{k_2} \cdots {h_m}^{k_m}$
for $k_1, k_2, \ldots, k_m \ge 0$.
Then :
:$A_m = \paren {-1}^{k_1 + k_2 + \cdots + k_m - 1} \dfrac {m \paren {k_1 + k_2 + \cdots + k_m - 1}! } {k_1! \, k_2! \, \cdots k_m!}$

Proof:
Let $\map G z$ be the generating function for the sequence $\sequence {h_m}$.
{{begin-eqn}}
{{eqn | l = \sum_{m \mathop \ge 1} \dfrac {S_m z^m} m
      | r = \map \ln {\map G z}
      | c = Summation of Products of n Numbers taken m at a time with Repetitions: Lemma 2
}}
{{eqn | r = \map \ln {1 + h_1 z + h_2 z^2 + \cdots}
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k - 1} } k \paren {h_1 z + h_2 z^2 + \cdots}^k
      | c = Power Series Expansion for Logarithm of 1 + x
}}
{{eqn | ll= \leadsto
      | l = S_m
      | r = m \sum_{k \mathop \ge 1} \dfrac {\paren {-1}^{k - 1} } k \paren {\sum_{j \mathop = 1} h_j z^j}^k
      | c = 
}}
{{end-eqn}}
{{finish|Not sure where this is going}}
Theorem: Doubly Sequenced Generating Function for Binomial Coefficients

Let $\sequence {a_{m n} }$ be the doubly subscripted sequence defined as:
:$\forall m, n \in \N_{\ge 0}: a_{m n} = \dbinom n m$
where $\dbinom n m$ denotes a binomial coefficient.
Then the generating function for $\sequence {a_{m n} }$ is given as:
:$\map G {w, z} = \dfrac 1 {1 - z - w z}$

Proof:
{{begin-eqn}}
{{eqn | l = \map G {w, z}
      | r = \sum_{m, \, n \mathop \ge 0} a_{m n} w^m z^n
      | c = {{Defof|Generating Function for Doubly Subscripted Sequence}}
}}
{{eqn | r = \sum_{m, \, n \mathop \ge 0} \dbinom n m w^m z^n
      | c = 
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {1 + w}^n z^n
      | c = Binomial Theorem
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {\paren {1 + w} z}^n
      | c = 
}}
{{eqn | r = \dfrac 1 {1 - \paren {1 + w} z}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \dfrac 1 {1 - z - w z}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Generating Function of Sequence

Let $\sequence{a_n}$ be a sequence which has a generating function which is convergent.
Let $\map G z$ be the generating function for $\sequence{a_n}$.
Let $\map f x$ be the step function:
:$\map f x = \ds \sum_{k \mathop \in \Z} a_k \sqbrk{0 \le k \le x}$
where $\sqbrk{0 \le k \le x}$ is Iverson's convention.
Then the Laplace transform of $\map f x$ is given by:
:$\laptrans {\map f s} = \dfrac {\map G {e^{-s} }} s$

Proof:
We note that:
{{begin-eqn}}
{{eqn | n = 1
      | l = \laptrans {\map f s}
      | r = \int_0^\infty e^{-s t} \map f t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | n = 2
      | l = \map G z
      | r = \sum_{n \mathop \ge 0} a_n z^n
      | c = {{Defof|Generating Function}}
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int_n^{n + 1} e^{-s t} \map f t \rd t
      | r = \int_n^{n + 1} \paren{a_0 + a_1 + \cdots + a_n} e^{-s t} \rd t
      | c = Definition of $f \left({x}\right)$
}}
{{eqn | r = \sum_{k \mathop = 0}^n a_k \sqbrk{\dfrac {-1} s e^{-s t} }_n^{n + 1}
      | c = Primitive of Exponential Function
}}
{{eqn | r = \sum_{k \mathop = 0}^n \dfrac {a_k} s \paren{e^{-s n} - e^{-s \paren{n + 1} } }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f s}
      | r = \int_0^\infty e^{-s t} \map f t \rd t
      | c = from $(1)$
}}
{{eqn | r = \sum_{n \mathop \ge 0} \sum_{k \mathop = 0}^n \dfrac {a_k} s \paren{e^{-s n} - e^{-s \paren{n + 1} } }
      | c = 
}}
{{eqn | r = \dfrac {a_0} s \paren{1 - e^{-s} } + \dfrac {a_0 + a_1} s \paren{e^{-s} - e^{-2 s} } + \dfrac {a_0 + a_1 + a_2} s \paren{e^{-2 s} - e^{-3 s} } + \cdots
      | c = 
}}
{{eqn | r = \dfrac 1 s \paren{a_0 + a_1 e^{-s} + a_2 e^{-2 s} + \cdots}
      | c = 
}}
{{eqn | r = \dfrac 1 s \sum_{n \mathop \ge 0} a_n e^{-s n}
      | c = 
}}
{{eqn | r = \dfrac 1 s \map G {e^{-s} }
      | c = from $(2)$
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Rational Sequence is not necessarily Rational

Let $S = \sequence {a_n}$ be a rational sequence.
Let $S$ be convergent to a limit $L$.
Then it is not necessarily the case that $L$ is itself a rational number.

Proof:
Proof by Counterexample:
By definition, Euler's number $e$ can be defined as:
:$e = \ds \sum_{n \mathop = 0}^\infty \frac 1 {n!}$
Each of the terms of the sequence of partial sums is rational.
However, from Euler's Number is Irrational, $e$ itself is not.
{{qed}}
Theorem: Product of Negative Real Numbers is Positive

Let $a, b \in \R_{\le 0}$ be negative real numbers.
Then:
:$a \times b \in \R_{\ge 0}$
That is, their product $a \times b$ is a positive real number.

Proof:
From Real Numbers form Ring, the set $\R$ of real numbers forms a ring.
The result then follows from Product of Ring Negatives.
{{qed}}
Theorem: Powers of Imaginary Unit

The (integer) powers of the imaginary unit $i$ are:
{{begin-eqn}}
{{eqn | l = i^0
      | r = 1
      | c = 
}}
{{eqn | l = i^1
      | r = i
      | c = 
}}
{{eqn | l = i^2
      | r = -1
      | c = 
}}
{{eqn | l = i^3
      | r = -i
      | c = 
}}
{{eqn | l = i^4
      | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}

Proof:
By definition:
:$i^2 = -1$
Then we have:
{{begin-eqn}}
{{eqn | l = i^0
      | r = e^{0 \ln i}
      | c = {{Defof|Power to Complex Number}}
}}
{{eqn | r = e^0
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = i^1
      | r = e^{1 \ln i}
      | c = {{Defof|Power to Complex Number}}
}}
{{eqn | r = e^{\ln i}
      | c = 
}}
{{eqn | r = i
      | c = {{Defof|Exponential Function}}
}}
{{end-eqn}}
Finally:
{{begin-eqn}}
{{eqn | l = i^3
      | r = i^2 \times i
      | c = 
}}
{{eqn | r = \paren {-1} \times i
      | c = 
}}
{{eqn | r = -i
      | c = {{Defof|Negative of Complex Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Real Number Multiplied by Complex Number

Let $a \in \R$ be a real number.
Let $c + d i \in \C$ be a complex number.
Then:
:$a \times \paren {c + d i} = \paren {c + d i} \times a = a c + i a d$

Proof:
$a$ can be expressed as a wholly real complex number $a + 0 i$.
Then we have:
{{begin-eqn}}
{{eqn | l = a \times \paren {c + d i}
      | r = \paren {a + 0 i} \times \paren {c + d i}
      | c = {{Defof|Wholly Real}}
}}
{{eqn | r = \paren {a c - 0 d} + \paren {a d + 0 c} i
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = a c + i a d
      | c = simplification
}}
{{end-eqn}}
The result for $\paren {c + d i} \times a$ follows from Complex Multiplication is Commutative.
{{qed}}
Theorem: Complex Number equals Negative of Conjugate iff Wholly Imaginary

Let $z \in \C$ be a complex number.
Let $\overline z$ be the complex conjugate of $z$.
Then $\overline z = -z$ {{iff}} $z$ is wholly imaginary.

Proof:
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = \overline z
      | r = -z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x - i y
      | r = -\left({x + i y}\right)
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | ll= \leadsto
      | l = +x
      | r = -x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = 0
      | c = 
}}
{{end-eqn}}
Hence by definition, $z$ is wholly imaginary.
{{qed|lemma}}
Now suppose $z$ is wholly imaginary.
Then:
{{begin-eqn}}
{{eqn | l = \overline z
      | r = 0 - i y
      | c = 
}}
{{eqn | r = -i y
      | c = 
}}
{{eqn | r = -\left({0 + i y}\right)
      | c = 
}}
{{eqn | r = -z
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Square of Complex Conjugate is Complex Conjugate of Square

Let $z \in \C$ be a complex number.
Let $\overline z$ denote the complex conjugate of $z$.
Then:
: $\overline {z^2} = \left({\overline z}\right)^2$

Proof:
A direct consequence of Product of Complex Conjugates:
: $\overline {z_1  z_2} = \overline {z_1} \cdot \overline {z_2}$
for two  complex numbers $z_1, z_2 \in \C$.
{{qed}}
Theorem: Complex Modulus equals Zero iff Zero

Let $z = a + i b$ be a complex number.
Let $\cmod z$ be the modulus of $z$.
Then:
:$\cmod z = 0 \iff z = 0$

Proof:
=== Necessary Condition ===
{{begin-eqn}}
{{eqn | l = z
      | r = 0
      | c = 
}}
{{eqn | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod z
      | r = \sqrt {0^2 + 0^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Complex Modulus is Non-Negative

Let $z = a + i b \in \C$ be a complex number.
Let $\cmod z$ be the modulus of $z$.
Then:
:$\cmod z \ge 0$

Proof:
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = \cmod {a + b i}
      | c = Definition of $z$
}}
{{eqn | r = +\sqrt {a^2 + b^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | o = \ge
      | r = 0
      | c = {{Defof|Positive Square Root}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus equals Complex Modulus of Conjugate

Let $z \in \C$ be a complex number.
Let $\overline z$ denote the complex conjugate of $z$.
Let $\cmod z$ denote the modulus of $z$.
Then:
:$\cmod z = \cmod {\overline z}$

Proof:
Let $z = a + b i$.
Then:
{{begin-eqn}}
{{eqn | l = \cmod z
      | r = \cmod {a + b i}
      | c = Definition of $z$
}}
{{eqn | r = \sqrt {a^2 + b^2}
      | c = {{Defof|Complex Modulus}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \cmod {\overline z}
      | r = \cmod {\overline {a + b i} }
      | c = Definition of $z$
}}
{{eqn | r = \cmod {a - b i}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = \cmod {a + \paren {- b} i}
      | c = 
}}
{{eqn | r = \sqrt {a^2 + \paren {- b}^2}
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \sqrt {a^2 + b^2}
      | c = 
}}
{{eqn | r = \cmod z
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Square of Complex Modulus equals Complex Modulus of Square

Let $z \in \C$ be a complex number.
Let $\cmod z$ be the modulus of $z$.
Then:
: $\cmod {z^2} = \cmod z^2$

Proof:
From Complex Modulus of Product of Complex Numbers:
: $\cmod {z_1 z_2} = \cmod {z_1} \cmod {z_2}$
for $z_1, z_2 \in \C$.
Set $z = z_1 = z_2$ and the result follows.
{{qed}}
Theorem: Power of Complex Modulus equals Complex Modulus of Power

Let $z \in \C$ be a complex number.
Let $\left\vert{z}\right\vert$ be the modulus of $z$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\left\vert{z^n}\right\vert = \left\vert{z}\right\vert^n$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $P \left({n}\right)$ be the proposition:
:$\left\vert{z^n}\right\vert = \left\vert{z}\right\vert^n$
$P \left({0}\right)$ is the case:
{{begin-eqn}}
{{eqn | l = \left\vert{z^0}\right\vert
      | r = \left\vert{1}\right\vert
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \left\vert{z}\right\vert^0
      | c = 
}}
{{end-eqn}}
Thus $P \left({0}\right)$ is seen to hold.
Theorem: Power of Complex Conjugate is Complex Conjugate of Power

Let $z \in \C$ be a complex number.
Let $\overline z$ denote the complex conjugate of $z$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\overline {z^n} = \left({\overline z}\right)^n$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $P \left({n}\right)$ be the proposition:
:$\overline {z^n} = \left({\overline z}\right)^n$
$P \left({0}\right)$ is the case:
{{begin-eqn}}
{{eqn | l = \overline {z^0}
      | r = \overline 1
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \left({\overline z}\right)^0
      | c = 
}}
{{end-eqn}}
Thus $P \left({0}\right)$ is seen to hold.
Theorem: Conjugate of Polynomial is Polynomial of Conjugate

Let $\map f z = a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0$ be a polynomial over complex numbers where $a_0, \ldots, a_n$ are real numbers.
Let $\alpha \in \C$ be a complex number.
Then:
:$\overline {\map f \alpha} = \map f {\overline \alpha}$
where $\overline \alpha$ denotes the complex conjugate of $\alpha$.

Proof:
By Power of Complex Conjugate is Complex Conjugate of Power:
:$\overline {\alpha^k} = \paren {\overline \alpha}^k$
for all $k$ between $0$ and $n$.
Then from Product of Complex Conjugates:
:$\overline {a_k \alpha^k} = \overline {a_k} \cdot \overline {\alpha^k}$
But $a_k$ is real.
So by Complex Number equals Conjugate iff Wholly Real:
:$\overline {a_k} = a_k$.
From Sum of Complex Conjugates, it follows that:
:$\overline {\map f \alpha} = a_n \paren {\overline \alpha}^n + a_{n - 1} \paren {\overline \alpha}^{n - 1} + \cdots + a_1 \overline \alpha + a_0$
Hence the result.
{{qed}}
Theorem: Complex Roots of Polynomial with Real Coefficients occur in Conjugate Pairs

Let $\map f z = a_n z^n + a_{n - 1} z^{n - 1} + \cdots + a_1 z + a_0$ be a polynomial over complex numbers where $a_0, \ldots, a_n$ are real numbers.
Let $\alpha \in \C$ be a root of $f$.
Then $\overline \alpha$ is also a root of $f$, where $\overline \alpha$ denotes the complex conjugate of $\alpha$.
That is, all complex roots of $f$ appear as conjugate pairs.

Proof:
Let $\alpha \in \C$ be a root of $f$.
Then $\map f \alpha = 0$ by definition.
Suppose $\alpha$ is wholly real.
Then by Complex Number equals Conjugate iff Wholly Real:
:$\alpha = \overline \alpha$
and so $\overline \alpha$ is a root of $f$.
Now let $\alpha \in \C$ not be wholly real.
By definition of complex conjugate, we have that:
:$\overline 0 = 0$
and so:
:$\map f \alpha = \overline {\map f \alpha}$
From Conjugate of Polynomial is Polynomial of Conjugate:
:$\overline {\map f \alpha} = \map f {\overline \alpha}$
from which it follows that:
:$\map f {\overline \alpha} = 0$
That is, $\overline \alpha$ is also a root of $f$.
{{qed}}