avewright/proofwiki-math huggingface dataset:
Theorem: Sum of Two Odd Powers

Let $\F$ be one of the standard number systems, that is $\Z, \Q, \R$ and so on.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
{{begin-eqn}}
{{eqn | l = a^{2 n + 1} + b^{2 n + 1}
      | r = \paren {a + b} \sum_{j \mathop = 0}^{2 n} \paren {-1}^j a^{2 n - j} b^j
      | c = 
}}
{{eqn | r = \paren {a + b} \paren {a^{2 n} - a^{2 n - 1} b + a^{2 n - 2} b^2 - \dotsb - a b^{2 n - 1} + b^{2 n} }
      | c = 
}}
{{end-eqn}}

Proof:
From Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
Let $x = a$ and $y = -b$.
Then:
{{begin-eqn}}
{{eqn | l = x^3 + y^3
      | r = x^3 - \paren {-y^3}
      | c = 
}}
{{eqn | r = x^3 - \paren {-y}^3
      | c = 
}}
{{eqn | r = \paren {x - \paren {-y} } \sum_{j \mathop = 0}^2 x^{n - j - 1} \paren {-y}^j
      | c = 
}}
{{eqn | r = \paren {x + y} \paren {x^2 + x \paren {-y} + \paren {-y}^2}
      | c = 
}}
{{eqn | r = \paren {x + y} \paren {x^2 - x y + y^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Two Odd Powers

Let $\F$ be one of the standard number systems, that is $\Z, \Q, \R$ and so on.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
{{begin-eqn}}
{{eqn | l = a^{2 n + 1} + b^{2 n + 1}
      | r = \paren {a + b} \sum_{j \mathop = 0}^{2 n} \paren {-1}^j a^{2 n - j} b^j
      | c = 
}}
{{eqn | r = \paren {a + b} \paren {a^{2 n} - a^{2 n - 1} b + a^{2 n - 2} b^2 - \dotsb - a b^{2 n - 1} + b^{2 n} }
      | c = 
}}
{{end-eqn}}

Proof:
From Sum of Two Odd Powers:
:$a^{2 n + 1} + b^{2 n + 1} = \paren {a + b} \paren {a^{2 n} - a^{2 n - 1} b + a^{2 n - 2} b^2 - \dotsb + a b^{2 n - 1} + b^{2 n} }$
We have that $3 = 2 \times 1 + 1$.
Hence setting $n = 1$ gives the result.
{{qed}}
Theorem: Difference of Two Fifth Powers

:$x^5 - y^5 = \paren {x - y} \paren {x^4 + x^3 y + x^2 y^2 + x y^3 + y^4}$

Proof:
From Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
The result follows directly by setting $n = 5$.
{{qed}}
Theorem: Sum of Two Fifth Powers

:$x^5 + y^5 = \paren {x + y} \paren {x^4 - x^3 y + x^2 y^2 - x y^3 + y^4}$

Proof:
From Sum of Two Odd Powers:
:$a^{2 n + 1} + b^{2 n + 1} = \paren {a + b} \paren {a^{2 n} - a^{2 n - 1} b + a^{2 n - 2} b^2 - \dotsb + a b^{2 n - 1} + b^{2 n} }$
We have that $5 = 2 \times 2 + 1$.
The result follows directly by setting $n = 2$.
{{qed}}
Theorem: Difference of Two Sixth Powers

:$x^6 - y^6 = \paren {x - y} \paren {x + y} \paren {x^2 + x y + y^2} \paren {x^2 - x y + y^2}$

Proof:
{{begin-eqn}}
{{eqn | l = x^6 - y^6
      | r = \paren {x^3}^2 - \paren {y^3}^2
      | c = 
}}
{{eqn | r = \paren {x^3 - y^3} \paren {x^3 + y^3}
      | c = 
}}
{{eqn | r = \paren {x - y} \paren {x^2 + x y + y^2} \paren {x^3 + y^3}
      | c = Difference of Two Cubes
}}
{{eqn | r = \paren {x - y} \paren {x^2 + x y + y^2} \paren {x + y} \paren {x^2 - x y + y^2}
      | c = Sum of Two Cubes
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Fourth Powers with Product of Squares

:$x^4 + x^2 y^2 + y^4 = \paren {x^2 + x y + y^2} \paren {x^2 - x y + y^2}$

Proof:
{{begin-eqn}}
{{eqn | l = x^6 - y^6
      | r = \paren {x - y} \paren {x + y} \paren {x^2 + 2 x y + 2 y^2} \paren {x^2 - 2 x y + 2 y^2}
      | c = Difference of Two Sixth Powers
}}
{{eqn | r = \paren {x^2 - y^2} \paren {x^2 + 2 x y + 2 y^2} \paren {x^2 - 2 x y + 2 y^2}
      | c = Difference of Two Squares
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = x^6 - y^6
      | r = \paren {x^2}^3 - \paren {y^2}^3
      | c = 
}}
{{eqn | r = \paren {x^2 - y^2} \paren {\paren {x^2}^2 + \paren {x^2} \paren {y^2} + \paren {y^2}^2}
      | c = Difference of Two Cubes
}}
{{eqn | r = \paren {x^2 - y^2} \paren {x^4 + x^2 y^2 + y^4}
      | c = simplifying
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \paren {x^2 - y^2} \paren {x^4 + x^2 y^2 + y^4}
      | r = \paren {x^2 - y^2} \paren {x^2 + 2 x y + 2 y^2} \paren {x^2 - 2 x y + 2 y^2}
      | c = as both equal $x^6 - y^6$
}}
{{eqn | ll= \leadsto
      | l = \paren {x^4 + x^2 y^2 + y^4}
      | r = \paren {x^2 + 2 x y + 2 y^2} \paren {x^2 - 2 x y + 2 y^2}
      | c = cancelling $\paren {x^2 - y^2}$ from both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Two Odd Powers

Let $\mathbb F$ denote one of the standard number systems, that is $\Z$, $\Q$, $\R$ and $\C$.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then for all $a, b \in \mathbb F$:
{{begin-eqn}}
{{eqn | l = a^{2 n + 1} - b^{2 n + 1}
      | r = \paren {a - b} \sum_{j \mathop = 0}^{2 n} a^{2 n - j} b^j
      | c = 
}}
{{eqn | r = \paren {a - b} \paren {a^{2 n} + a^{2 n - 1} b + a^{2 n - 2} b^2 + \dotsb + a b^{2 n - 1} + b^{2 n} }
      | c = 
}}
{{end-eqn}}

Proof:
A direct application of Difference of Two Powers:
{{begin-eqn}}
{{eqn | l = a^n - b^n
      | r = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j
      | c = 
}}
{{eqn | r = \paren {a - b} \paren {a^{n - 1} + a^{n - 2} b + a^{n - 3} b^2 + \dotsb + a b^{n - 2} + b^{n - 1} }
      | c = 
}}
{{end-eqn}}
and setting $n \to 2 n + 1$.
{{qed}}
Theorem: Difference of Two Even-Times Odd Powers

Let $\F$ be one of the standard number systems, that is $\Z, \Q, \R$ and so on.
Let $n \in \Z_{> 0}$ be a (strictly) positive odd integer.
Then:
{{begin-eqn}}
{{eqn | l = a^{2 n} - b^{2 n}
      | r = \paren {a - b} \paren {a + b} \paren {\sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j} \paren {\sum_{j \mathop = 0}^{n - 1} \paren {-1}^j a^{n - j - 1} b^j}
      | c = 
}}
{{eqn | r = \paren {a - b} \paren {a + b} \paren {a^{n - 1} + a^{n - 2} b + a^{n - 3} b^2 + \dotsb + a b^{n - 2} + b^{n - 1} } \paren {a^{n - 1} - a^{n - 2} b + a^{n - 3} b^2 - \dotsb - a b^{n - 2} + b^{n - 1} }
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = a^{2 n} - b^{2 n}
      | r = \paren {a^n}^2 - \paren {b^n}^2
      | c = 
}}
{{eqn | r = \paren {a^n - b^n} \paren {a^n + b^n}
      | c = 
}}
{{eqn | r = \paren {a - b} \paren {\sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j} \paren {a^n + b^n}
      | c = Difference of Two Powers
}}
{{eqn | r = \paren {a - b} \paren {\sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j} \paren {a + b} \paren {\sum_{j \mathop = 0}^{n - 1} \paren {-1}^j a^{n - j - 1} b^j}
      | c = Sum of Two Odd Powers
}}
{{end-eqn}}
whence the result.
{{qed}}
Theorem: Difference of Two Even Powers

Let $\GF$ denote one of the standard number systems, that is $\Z$, $\Q$, $\R$ and $\C$.
Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then for all $a, b \in \GF$:
{{begin-eqn}}
{{eqn | l = a^{2 n} - b^{2 n}
      | r = \paren {a - b} \paren {a + b} \sum_{j \mathop = 0}^{n - 1} a^{2 \paren {n - j - 1} } b^{2 j}
      | c = 
}}
{{eqn | r = \paren {a - b} \paren {a + b} \paren {a^{2 n - 2} + a^{2 n - 4} b^2 + a^{2 n - 6} b^4 + \dotsb + a^2 b^{2 n - 4} + b^{2 n - 2} }
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = a^{2 n} - b^{2 n}
      | r = \paren {a^2}^n - \paren {b^2}^n
      | c = 
}}
{{eqn | r = \paren {a^2 - b^2} \paren {\sum_{j \mathop = 0}^{n - 1} \paren {a^2} ^{n - j - 1} \paren {b^2}^j}
      | c = Difference of Two Powers
}}
{{eqn | r = \paren {a - b} \paren {a + b} \sum_{j \mathop = 0}^{n - 1} a^{2 \paren {n - j - 1} } b^{2 j}
      | c = Difference of Two Squares
}}
{{end-eqn}}
whence the result.
{{qed}}
Theorem: Factors of Difference of Two Odd Powers

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
{{begin-eqn}}
{{eqn | l = x^{2 n + 1} - y^{2 n + 1}
      | r = \paren {x - y} \prod_{k \mathop = 1}^n \paren {x^2 - 2 x y \cos \dfrac {2 \pi k} {2 n + 1} + y^2}
      | c = 
}}
{{eqn | r = \paren {x - y} \paren {x^2 - 2 x y \cos \dfrac {2 \pi} {2 n + 1} + y^2} \paren {x^2 - 2 x y \cos \dfrac {4 \pi} {2 n + 1} + y^2} \dotsm \paren {x^2 - 2 x y \cos \dfrac {2 n \pi} {2 n + 1} + y^2}
      | c = 
}}
{{end-eqn}}

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

Let $n \in \Z_{>0}$ be a (strictly) positive integer.
Then:
{{begin-eqn}}
{{eqn | l = x^{2 n + 1} + y^{2 n + 1}
      | r = \paren {x + y} \prod_{k \mathop = 1}^n \paren {x^2 + 2 x y \cos \dfrac {2 \pi k} {2 n + 1} + y^2}
      | c = 
}}
{{eqn | r = \paren {x + y} \paren {x^2 + 2 x y \cos \dfrac {2 \pi} {2 n + 1} + y^2} \paren {x^2 + 2 x y \cos \dfrac {4 \pi} {2 n + 1} + y^2} \dotsm \paren {x^2 + 2 x y \cos \dfrac {2 n \pi} {2 n + 1} + y^2}
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = x^{2 n + 1} + y^{2 n + 1}
      | r = x^{2 n + 1} - \paren {-\paren {y^{2 n + 1} } }
      | c = 
}}
{{eqn | r = x^{2 n + 1} - \paren {-y}^{2 n + 1}
      | c = 
}}
{{eqn | r = \paren {x - \paren {-y} } \prod_{k \mathop = 1}^n \paren {x^2 - 2 x \paren {-y} \cos \dfrac {2 \pi k} {2 n + 1} + \paren {-y}^2}
      | c = Factors of Difference of Two Odd Powers
}}
{{eqn | r = \paren {x + y} \prod_{k \mathop = 1}^n \paren {x^2 + 2 x y \cos \dfrac {2 \pi k} {2 n + 1} + y^2}
      | c = simplification
}}
{{end-eqn}}
{{qed}}
Theorem: Factors of Difference of Two Even Powers

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

Proof:
From Factorisation of $z^n - a$:
:$\ds z^{2 n} - y^{2 n} = \prod_{k \mathop = 0}^{2 n - 1} \paren {x - \alpha^k y}$
where $\alpha$ is a primitive complex $2 n$th roots of unity, for example:
{{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 $x - y$.
The case $k = n$ is taken care of by setting $\alpha^k = -1$, from whence we have the factor $x + y$.
Taking the product of each of the remaining factors of $x^{2 n} - y^{2 n}$ in pairs:
{{begin-eqn}}
{{eqn | l = \paren {x - \alpha^k y} \paren {x - \alpha^{2 n - k} y}
      | r = \paren {x - \alpha^k y} \paren {x - \overline {\alpha^k} y}
      | c = Complex Roots of Unity occur in Conjugate Pairs
}}
{{eqn | r = x^2 - x y \paren {\alpha^k + \overline {\alpha^k} } + \alpha^k y \overline {\alpha^k} y
      | c = 
}}
{{eqn | r = x^2 - x y \paren {\alpha^k + \overline {\alpha^k} } + \cmod {\alpha^k}^2 y^2
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = x^2 - x y \paren {\alpha^k + \overline {\alpha^k} } + y^2
      | c = Modulus of Complex Root of Unity equals 1
}}
{{eqn | r = x^2 - x y \paren {\cos \dfrac {k \pi} n + i \sin \dfrac {k \pi} n + \cos \dfrac {k \pi} n - i \sin \dfrac {k \pi} n} + y^2
      | c = Definition of $\alpha$
}}
{{eqn | r = x^2 - 2 x y \cos \dfrac {k \pi} n + y^2
      | c = simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Topological Properties of Non-Archimedean Division Rings/Spheres are Clopen

:The $r$-sphere of $x$, $\map {S_r} x$, is both open and closed in the metric induced by $\norm {\,\cdot\,}$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \map {S_r} x
      | r = \set {y \in R : \norm {y - x} = r}
      | c = {{Defof|Sphere in Normed Division Ring}}
}}
{{eqn | r = \set {y \in R : \norm {y - x} \le r} \cap \set {y \in R : \norm{y - x} \ge r}
}}
{{eqn | r = \map { {B_r}^-} x \cap \paren {R \setminus \map {B_r} x}
      | c = {{Defof|Open Ball of Normed Division Ring}} and {{Defof|Closed Ball of Normed Division Ring}}
}}
{{end-eqn}}
Let $d$ be the metric induced by the norm $\norm {\,\cdot\,}$.
By Open Balls Are Clopen then $\map {B_r} x$ is both open and closed in $d$.
By Metric Induces Topology then $R \setminus \map {B_r} x$ is is both open and closed in $d$.
By Closed Balls Are Clopen then $\map { {B_r}^-} x$ is both open and closed in $d$.
By Metric Induces Topology then the intersection of a finite number of open sets is open.   
Hence $\map {S_r} x$ is open in the metric space $\struct {R, d}$.
By Intersection of Closed Sets is Closed in Topological Space then $\map {S_r} x$ is closed in $\struct {R, d}$.
The result follows.
{{qed}}
Theorem: Existence of Real Polynomial with no Real Root

There exist polynomials in real numbers $\R$ which have no roots in $\R$.

Proof:
Proof by Counterexample
Take the quadratic equation:
:$(1): \quad x^2 + 1 = 0$
From the Quadratic Formula, the solution to $(1)$ is:
{{begin-eqn}}
{{eqn | l = x
      | r = \dfrac {-0 \pm \sqrt {0^2 - 4 \times 1 \times 1} } {2 \times 1}
      | c = 
}}
{{eqn | r = \pm \sqrt {-1}
      | c = 
}}
{{end-eqn}}
But there is no real number $x$ such that:
:$x^2 = -1$
Hence the result.
{{qed}}
Theorem: Magnitude of Projection of Complex Number on Another

Let $z_1$ and $z_2$ denote complex numbers in vector form.
Let $\map {\pr_1} {z_1, z_2}$ denote the projection of $z_1$ on $z_2$.
{{explain|We really need another page to explain the concept of Definition:Projection in Plane in the context of the Definition:Complex Plane}}
Then:
:$\cmod {\map {\pr_1} {z_1, z_2} } = \dfrac {\cmod {z_1 \circ z_2} } {\cmod {z_2} }$
where:
:$z_1 \circ z_2$ denotes complex dot product
:$\cmod {z_2}$ denotes complex modulus.

Proof:
{{ProofWanted|Needs a proper explanation of the nature of Definition:Projection in Plane}}
Theorem: Non-Archimedean Division Ring is Totally Disconnected

Let $\struct {R, \norm{\,\cdot\,} }$ be a non-Archimedean normed division ring.
Let $\tau$ be the topology induced by the norm $\norm{\,\cdot\,}$.
Then the topological space $\struct {R, \tau}$ is totally disconnected.

Proof:
Let $S$ be a subset of $R$ such that:
:$\exists x, y \in S: x \ne y$
Let $r \in \R_{>0} : r = \norm {x - y}$
Consider the open ball $\map {B_r} x$ such that:
:$x \in \map {B_r} x$
:$y \notin \map {B_r} x$
By Open Balls are Clopen then $\map {B_r} x$ is both open and closed.
By Complement of Clopen Set is Clopen then $R \setminus \map {B_r} x$ is open.
Let:
:$A = S \cap \map {B_r} x$
and
:$B = S \cap \paren{R \setminus \map {B_r} x}$
We have:
:$x \in A \subseteq \map {B_r} x$
and
:$y \in B \subseteq \paren{R \setminus \map {B_r} x}$
By definition of separated sets:
:$A$ and $B$ are separated sets
As $S = A \cup B$ then:
:$S$ is the union of two non-empty separated sets of $\struct{R,\tau}$
By definition of connected subset:
:$S$ is not a connected subset.
Since $S$ was an arbitrary subset of $\struct{R,\tau}$ with two distinct elements:
:no set $S$ with two distinct elements is connected.
From Singleton is Connected in Topological Space:
:the only connected subsets of $\struct{R,\tau}$ are the singletons
By definition of totally disconnected:
:$\struct{R,\tau}$ is totally disconnected
{{qed}}
Theorem: Distance between Points in Complex Plane

Let $A$ and $B$ be points in the complex plane such that:
:$A = \tuple {x_1, y_1}$
:$B = \tuple {x_2, y_2}$
Then the distance between $A$ and $B$ is given by:
{{begin-eqn}}
{{eqn | l = \size {AB}
      | r = \sqrt {\paren {x_2 - x_1}^2 + \paren {y_2 - y_1}^2}
      | c = 
}}
{{eqn | r = \cmod {z_1 - z_2}
      | c = 
}}
{{end-eqn}}
where $z_1$ and $z_2$ are represented by the complex numbers $z_1$ and $z_2$ respectively.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = AB
      | r = z_2 - z_1
      | c = Geometrical Interpretation of Complex Subtraction
}}
{{eqn | r = \paren {x_2 + i y_2} - \paren {x_1 + i y_1}
      | c = 
}}
{{eqn | r = \paren {x_2 - x_1} + \paren {y_2 - y_1} i
      | c = {{Defof|Complex Subtraction}}
}}
{{eqn | ll= \leadsto
      | l = \size {AB}
      | r = \cmod {\paren {x_2 - x_1} + \paren {y_2 - y_1} i}
      | c = 
}}
{{eqn | r = \sqrt {\paren {x_2 - x_1}^2 + \paren {y_2 - y_1}^2}
      | c = {{Defof|Complex Modulus}}
}}
{{end-eqn}}
{{qed}}
Theorem: Linear Combination of Non-Parallel Complex Numbers is Zero if Factors are Both Zero

Let $z_1$ and $z_2$ be complex numbers expressed as vectors such taht $z_1$ is not parallel to $z_2$.
Let $a, b \in \R$ be real numbers such that:
:$a z_1 + b z_2 = 0$
Then $a = 0$ and $b = 0$.

Proof:
Suppose it is not the case that $a = b = 0$.
Then:
{{begin-eqn}}
{{eqn | l = a z_1 + b z_2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a \paren {x_1 + i y_1} + b \paren {x_2 + i y_2}
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a x_1 + b x_2
      | r = 0
      | c = 
}}
{{eqn | l = a y_1 + b y_2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a x_1
      | r = -b x_2
      | c = 
}}
{{eqn | l = a y_1
      | r = -b y_2
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac {y_1} {x_1}
      | r = \dfrac {y_2} {x_2}
      | c = 
}}
{{end-eqn}}
and $z_1$ and $z_2$ are parallel.
{{qed}}
Theorem: Equation for Line through Two Points in Complex Plane/Formulation 1

$L$ can be expressed by the equation:
:$\map \arg {\dfrac {z - z_1} {z_2 - z_1} } = 0$

Proof:
Let $z$ be a point on the $L$.
Then:
:$z - z_1 = b \paren {z - z_2}$
where $b$ is some real number.
Then:
{{begin-eqn}}
{{eqn | l = b
      | r = \frac {z - z_1} {z - z_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \arg {\frac {z - z_1} {z_2 - z_1} }
      | r = \arg b
      | c = 
}}
{{eqn | r = 0
      | c = as $b$ is real
}}
{{end-eqn}}
{{qed}}
Theorem: Equation for Line through Two Points in Complex Plane/Parametric Form 1

$L$ can be expressed by the equation:
:$z = z_1 + t \paren {z_2 - z_1}$
or:
:$z = \paren {1 - t} z_1 + t z_2$
This form of $L$ is known as the '''parametric form''', where $t$ is the '''parameter'''.

Proof:
Let $z_1$ and $z_2$ be represented by the points $A = \tuple {x_1, y_1}$ and $B = \tuple {x_2, y_2}$ respectively in the complex plane.
Let $z$ be an arbitrary point on $L$ represented by the point $P$.
:500px
From Geometrical Interpretation of Complex Addition:
{{begin-eqn}}
{{eqn | l = OA + AP
      | r = OP
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 + AP
      | r = z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AP
      | r = z - z_1
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = OA + AB
      | r = OB
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z_1 + AB
      | r = z_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = AB
      | r = z_2 - z_1
      | c = 
}}
{{end-eqn}}
As $AP$ and $AB$ are collinear:
:$AP = t AB$
and so:
:$z - z_1 = t \paren {z_2 - z_1}$
The given expressions follow after algebra.
{{qed}}
Theorem: Equation for Line through Two Points in Complex Plane/Symmetric Form

$L$ can be expressed by the equation:
:$z = \dfrac {m z_1 + n z_2} {m + n}$
This form of $L$ is known as the '''symmetric form'''.

Proof:
Let $z_1$ and $z_2$ be represented by the points $A = \tuple {x_1, y_1}$ and $B = \tuple {x_2, y_2}$ respectively in the complex plane.
Let $z$ be an arbitrary point on $L$ represented by the point $P$.
:500px
As $AP$ and $AB$ are collinear:
:$m AP = n PB$
and so:
:$m \paren {z - z_1} = n \paren {z_2 - z_1}$
The result follows.
{{qed}}
Theorem: Valuation Ring of Non-Archimedean Division Ring is Subring

Let $\struct {R, \norm{\,\cdot\,}}$ be a non-Archimedean normed division ring with zero $0_R$ and unity $1_R$.
Let $\OO$ be the valuation ring induced by the non-Archimedean norm $\norm {\,\cdot\,}$, that is:
:$\OO = \set {x \in R : \norm{x} \le 1}$
Then $\OO$ is a subring of $R$:
:with a unity: $1_R$
:in which there are no (proper) zero divisors, that is:
:::$\forall x, y \in \OO: x \circ y = 0_R \implies x = 0_R \text{ or } y = 0_R$

Proof:
To show that $\OO$ is a subring the Subring Test is used by showing:
:$(1): \quad \OO \ne \O$
:$(2): \quad \forall x, y \in \OO: x + \paren {-y} \in \OO$
:$(3): \quad \forall x, y \in \OO: x y \in \OO$
'''(1)'''
By Norm of Unity,
:$\norm{1_R} = 1$
Hence:
:$1_R \in \OO \ne \O$
{{qed|lemma}}
'''(2)'''
Let $x, y \in \OO$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {x + \paren{-y} } 
      | o = \le
      | r = \max \set {\norm x, \norm{-y} }
      | c = {{NormAxiomNonArch|4}}
}}
{{eqn | r = \max \set {\norm x, \norm y}
      | c = Norm of Negative
}}
{{eqn | o = \le
      | r = 1
      | c = Since $x, y \in \OO$
}}
{{end-eqn}}
Hence:
:$x + \paren {-y} \in \OO$
{{qed|lemma}}
'''(3)'''
Let $x, y \in \OO$.
Then:
{{begin-eqn}}
{{eqn | l = \norm{x y} 
      | o = \le
      | r = \norm x \norm y
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | o = \le
      | r = 1
      | c = Since $x, y \in \OO$
}}
{{end-eqn}}
Hence:
:$x y \in \OO$
{{qed|lemma}}
By Subring Test it follows that $\OO$ is a subring of $R$.
Since $1_R \in S$ and $1_R$ is the unity of $R$ then $1_R$ is the unity of $\OO$.
By Division Ring has No Proper Zero Divisors then $R$ has no proper zero divisors.
Hence $\OO$ has no proper zero divisors.
{{qed}}
Theorem: Valuation Ideal is Maximal Ideal of Induced Valuation Ring

Let $\struct {R, \norm {\,\cdot\,} }$ be a non-Archimedean normed division ring with zero $0_R$ and unity $1_R$.
Let $\OO$ be the valuation ring induced by the non-Archimedean norm $\norm {\,\cdot\,}$, that is:
:$\OO = \set{x \in R : \norm x \le 1}$
Let $\PP$ be the valuation ideal induced by the non-Archimedean norm $\norm {\,\cdot\,}$, that is:
:$\PP = \set{x \in R : \norm x < 1}$
Then $\PP$ is an ideal of $\OO$:
:$(a):\quad \PP$ is a maximal left ideal
:$(b):\quad \PP$ is a maximal right ideal
:$(c):\quad$ the quotient ring $\OO / \PP$ is a division ring.

Proof:
First it is shown that $\PP$ is an ideal of $\OO$ by applying Test for Ideal.
That is, it is shown that:
:$(1): \quad \PP \ne \O$
:$(2): \quad \forall x, y \in \PP: x + \paren {-y} \in \PP$
:$(3): \quad \forall x \in \PP, y \in \OO: x y \in \PP$
By Maximal Left and Right Ideal iff Quotient Ring is Division Ring the statements '''(a)''', '''(b)''' and '''(c)''' above are equivalent.
So then it is shown:
:$(4): \quad \PP$ is a maximal left ideal
Theorem: Sequence of Imaginary Reciprocals/Boundedness

The set $S$ is bounded in $\C$.

Proof:
Let $z \in S$.
Then, for example:
:$\cmod z \le 2$
That is, $S$ is contained entirely within a circle of radius $2$ whose center is at the origin.
{{qed}}