avewright/proofwiki-math huggingface dataset:
Theorem: Derivative of Arctangent Function

:$\dfrac {\map \d {\arctan x} } {\d x} = \dfrac 1 {1 + x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\map \d {\arctan x} } {\d x} 
      | r = \lim_{h \mathop \to 0} \frac {\map \arctan {x + h} - \arctan x} h 
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map \arctan {x + h} + \map \arctan {-x} } h	
      | c = Arctangent Function is Odd
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac 1 h \map \arctan {\frac {x + h - x} {1 + x \paren {x + h} } }
      | c = Sum of Arctangents
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac 1 h \map \arctan {\frac h {1 + x^2 + h x} }
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac 1 h \paren {\frac h {1 + x^2 + h x} - \frac 1 3 \paren {\frac h {1 + x^2 + h x} }^3 + \frac 1 5 \paren {\frac h {1 + x^2 + h x} }^5 + \map \OO {h^7} }
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \paren {\frac 1 {1 + x^2 + h x} - \frac {h^2} {3 \paren {1 + x^2 + h x}^3} + \frac {h^4} {5 \paren {1 + x^2 + h x}^5} + \map \OO {h^6} }
}}
{{eqn | r = \frac 1 {1 + x^2 + 0 x} - \frac {0^2} {3 \paren {1 + x^2 + 0 x}^3} + \frac {0^4} {5 \paren {1 + x^2 + 0 x}^5}
}}
{{eqn | r = \frac 1 {1 + x^2} 
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Numbers form Field

Consider the algebraic structure $\struct {\C, +, \times}$, where:
:$\C$ is the set of all complex numbers
:$+$ is the operation of complex addition
:$\times$ is the operation of complex multiplication
Then $\struct {\C, +, \times}$ forms a field.

Proof:
From Complex Numbers under Addition form Infinite Abelian Group, we have that $\struct {\C, +}$ forms an abelian group.
From Non-Zero Complex Numbers under Multiplication form Infinite Abelian Group, we have that $\struct {\C_{\ne 0}, \times}$ forms an abelian group.
Finally, we have that Complex Multiplication Distributes over Addition.
Thus all the criteria are fulfilled, and $\struct {\C, +, \times}$ is a field.
{{qed}}
Theorem: Complex Multiplication is Commutative

The operation of multiplication on the set of complex numbers $\C$ is commutative:
:$\forall z_1, z_2 \in \C: z_1 z_2 = z_2 z_1$

Proof:
From the definition of complex numbers, we define the following:
{{begin-eqn}}
{{eqn | l = z
      | o = :=
      | r = \tuple {x_1, y_1}
}}
{{eqn | l = w
      | o = :=
      | r = \tuple {x_2, y_2}
}}
{{end-eqn}}
where $x_1, x_2, y_1, y_2 \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = z_1 z_2
      | r = \tuple {x_1, y_1} \tuple {x_2, y_2}
      | c = {{Defof|Complex Number|index = 2}}
}}
{{eqn | r = \tuple {x_1 x_2 - y_1 y_2, x_1 y_2 + x_2 y_1}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = \tuple {x_2 x_1 - y_2 y_1, x_1 y_2 + x_2 y_1}
      | c = Real Multiplication is Commutative
}}
{{eqn | r = \tuple {x_2 x_1 - y_2 y_1, x_2 y_1 + x_1 y_2}
      | c = Real Addition is Commutative
}}
{{eqn | r = \tuple {x_2, y_2} \tuple {x_1, y_1}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = z_2 z_1
      | c = {{Defof|Complex Number|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Multiplication Distributes over Addition

The operation of multiplication on the set of complex numbers $\C$ is distributive over the operation of addition.
:$\forall z_1, z_2, z_3 \in \C:$
::$z_1 \paren {z_2 + z_3} = z_1 z_2 + z_1 z_3$
::$\paren {z_2 + z_3} z_1 = z_2 z_1 + z_3 z_1$

Proof:
From the definition of complex numbers, we define the following:
{{begin-eqn}}
{{eqn | l = z_1
      | o = :=
      | r = \tuple {x_1, y_1}
}}
{{eqn | l = z_2
      | o = :=
      | r = \tuple {x_2, y_2}
}}
{{eqn | l = z_3
      | o = :=
      | r = \tuple {x_3, y_3}
}}
{{end-eqn}}
where $x_1, x_2, x_3, y_1, y_2, y_3 \in \R$.
Thus:
{{begin-eqn}}
{{eqn | l = z_1 \paren {z_2 + z_3}
      | r = \tuple {x_1, y_1} \paren {\tuple {x_2, y_2} + \tuple {x_3, y_3} }
      | c = {{Defof|Complex Number|index = 2}}
}}
{{eqn | r = \tuple {x_1, y_1} \tuple {x_2 + x_3, y_2 + y_3}
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \tuple {x_1 \paren {x_2 + x_3} - y_1 \paren {y_2 + y_3}, x_1 \paren {y_2 + y_3} + y_1 \paren {x_2 + x_3} }
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = \tuple {x_1 x_2 + x_1 x_3 - y_1 y_2 - y_1 y_3, x_1 y_2 + x_1 y_3 + y_1 x_2 + y_1 x_3}
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | r = \tuple {\paren {x_1 x_2 - y_1 y_2}\ + \paren {x_1 x_3 - y_1 y_3}, \paren {x_1 y_2 + y_1 x_2} + \paren {x_1 y_3 + y_1 x_3} }
      | c = Real Addition is Commutative
}}
{{eqn | r = \tuple {x_1 x_2 - y_1 y_2, x_1 y_2 + y_1 x_2} + \tuple {x_1 x_3 - y_1 y_3, x_1 y_3 + y_1 x_3}
      | c = {{Defof|Complex Number/Definition 2/Addition|Complex Addition}}
}}
{{eqn | r = \tuple {x_1, y_1} \tuple {x_2, y_2} + \tuple {x_1, y_1} \tuple {x_3, y_3}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | r = z_1 z_2 + z_1 z_3
      | c = {{Defof|Complex Number|index = 2}}
}}
{{end-eqn}}
The result $\paren {z_2 + z_3} z_1 = z_2 z_1 + z_3 z_1$ follows directly from the above, and the fact that Complex Multiplication is Commutative.
{{qed}}
Theorem: Complex Modulus of Product of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ be the modulus of $z$.
Then:
:$\cmod {z_1 z_2} = \cmod {z_1} \cdot \cmod {z_2}$

Proof:
Let $z_1 = x_1 + i y_1$ and $z_2 = x_2 + i y_2$, where $x_1, y_1, x_2, y_2 \in \R$.
{{begin-eqn}}
{{eqn | l = \cmod {z_1 z_2}
      | r = \sqrt {\paren {x_1 x_2 - y_1 y_2}^2 + \paren {x_1 y_2 + x_2 y_1}^2}
      | c = {{Defof|Complex Modulus}}, {{Defof|Complex Multiplication}}
}}
{{eqn | r = \sqrt {\paren {x_1^2 x_2^2 + y_1^2 y_2^2 - 2 x_1 x_2 y_1 y_2} + \paren {x_1^2 y_2^2 + x_2^2 y_1^2 + 2 x_1 x_2 y_1 y_2} }
      | c = 
}}
{{eqn | r = \sqrt {x_1^2 x_2^2 + y_1^2 y_2^2 + x_1^2 y_2^2 + x_2^2 y_1^2}
      | c = 
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \cmod {z_1} \cdot \cmod {z_2}
      | r = \sqrt {x_1^2 + y_1^2}  \sqrt {x_2^2 + y_2^2}
      | c = 
}}
{{eqn | r = \sqrt {\paren {x_1^2 + y_1^2} \paren {x_2^2 + y_2^2} }
      | c = 
}}
{{eqn | r = \sqrt {x_1^2 x_2^2 + y_1^2 y_2^2 + x_1^2 y_2^2 + x_2^2 y_1^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus of Product of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ be the modulus of $z$.
Then:
:$\cmod {z_1 z_2} = \cmod {z_1} \cdot \cmod {z_2}$

Proof:
Let $\overline z$ denote the complex conjugate of $z$. 
Then:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 z_2}
      | r = \sqrt {\paren {z_1 z_2} \overline {\paren {z_1 z_2} } }
      | c = Modulus in Terms of Conjugate
}}
{{eqn | r = \sqrt {z_1 \overline {z_1} z_2 \overline {z_2} }
      | c = Product of Complex Conjugates, Complex Multiplication is Commutative
}}
{{eqn | r = \sqrt {z_1 \overline {z_1} } \sqrt {z_2 \overline {z_2} }
      | c = Power of Product
}}
{{eqn | r = \cmod {z_1} \cmod {z_2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Modulus of Product of Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\cmod z$ be the modulus of $z$.
Then:
:$\cmod {z_1 z_2} = \cmod {z_1} \cdot \cmod {z_2}$

Proof:
Let:
:$z_1 = r_1 \paren {\cos \theta_1 + i \sin \theta_1}$
:$z_2 = r_2 \paren {\cos \theta_2 + i \sin \theta_2}$
Then:
{{begin-eqn}}
{{eqn | l = \cmod {z_1 z_2}
      | r = \cmod {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 = \cmod {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
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{eqn | r = \cmod {z_1} \cmod {z_2}
      | c = {{Defof|Polar Form of Complex Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Complex Conjugates

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\overline z$ denote the complex conjugate of the complex number $z$.
Then:
:$\overline {z_1 + z_2} = \overline {z_1} + \overline {z_2}$

Proof:
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
Then:
{{begin-eqn}}
{{eqn | l = \overline {z_1 + z_2}
      | r = \overline {\paren {x_1 + x_2} + i \paren {y_1 + y_2} }
      | c = 
}}
{{eqn | r = \paren {x_1 + x_2} - i \paren {y_1 + y_2}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = \paren {x_1 - i y_1} + \paren {x_2 - i y_2}
      | c = {{Defof|Complex Addition}}
}}
{{eqn | r = \overline {z_1} + \overline {z_2}
      | c = {{Defof|Complex Conjugate}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Complex Conjugates

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\overline z$ denote the complex conjugate of the complex number $z$.
Then:
:$\overline {z_1 z_2} = \overline {z_1} \cdot \overline {z_2}$

Proof:
Let $z_1 = x_1 + i y_1$ and $z_2 = x_2 + i y_2$, where $x_1, y_1, x_2, y_2 \in \R$.
Then:
{{begin-eqn}}
{{eqn | l = \overline {z_1 z_2}
      | r = \overline {\paren {x_1 x_2 - y_1 y_2} + i \paren {x_2 y_1 + x_1 y_2} }
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = \paren {x_1 x_2 - y_1 y_2} - i \paren {x_2 y_1 + x_1 y_2}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = \paren {x_1 x_2 - \paren {-y_1} \paren {-y_2} } + i \paren {x_2 \paren {-y_1} + x_1 \paren {-y_2} }
      | c = 
}}
{{eqn | r = \paren {x_1 - i y_1} \paren {x_2 - i y_2}
      | c = {{Defof|Complex Multiplication}}
}}
{{eqn | r = \overline {z_1} \cdot \overline {z_2}
      | c = {{Defof|Complex Conjugate}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Complex Conjugates

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\overline z$ denote the complex conjugate of the complex number $z$.
Then:
:$\overline {z_1 z_2} = \overline {z_1} \cdot \overline {z_2}$

Proof:
From Product of Complex Conjugates: General Result:
:$\ds \overline {\prod_{j \mathop = 1}^n z_j} = \prod_{j \mathop = 1}^n \overline {z_j}$
The result follows by setting $n = 3$.
Theorem: Sum of Complex Number with Conjugate

Let $z \in \C$ be a complex number.
Let $\overline z$ be the complex conjugate of $z$.
Let $\map \Re z$ be the real part of $z$.
Then:
:$z + \overline z = 2 \, \map \Re z$

Proof:
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = z + \overline z
      | r = \paren {x + i y} + \paren {x - i y}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = 2 x
}}
{{eqn | r = 2 \, \map \Re z
      | c = {{Defof|Real Part}}
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Complex Number with Conjugate

Let $z \in \C$ be a complex number.
Let $\overline z$ be the complex conjugate of $z$.
Let $\map \Im z$ be the imaginary part of $z$.
Then
:$z - \overline z = 2 i \, \map \Im z$

Proof:
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = z - \overline z
      | r = \paren {x + i y} - \paren {x - i y}
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | r = x + i y - x + i y
}}
{{eqn | r = 2 i y
}}
{{eqn | r = 2 i \, \map \Im z
      | c = {{Defof|Imaginary Part}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Number equals Conjugate iff Wholly Real

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

Proof:
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = \overline z
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + i y
      | r = x - i y
      | c = {{Defof|Complex Conjugate}}
}}
{{eqn | ll= \leadsto
      | l = +y
      | r = -y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = y
      | r = 0
      | c = 
}}
{{end-eqn}}
Hence by definition, $z$ is wholly real.
{{qed|lemma}}
Now suppose $z$ is wholly real.
Then:
{{begin-eqn}}
{{eqn | l = z
      | r = x + 0 i
      | c = 
}}
{{eqn | r = x
      | c = 
}}
{{eqn | r = x - 0 i
      | c = 
}}
{{eqn | r = \overline z
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Complex Numbers cannot be Ordered Compatibly with Ring Structure

Let $\struct {\C, +, \times}$ be the field of complex numbers.
There exists no total ordering on $\struct {\C, +, \times}$ which is compatible with the structure of $\struct {\C, +, \times}$.

Proof:
{{AimForCont}} there exists a relation $\preceq$ on $\C$ which is ordering compatible with the ring structure of $\C$.
That is:
:$(1): \quad z \ne 0 \implies 0 \prec z \lor z \prec 0$, but not both
:$(2): \quad 0 \prec z_1, z_2 \implies 0 \prec z_1 z_2 \land 0 \prec z_1 + z_2$
By Totally Ordered Ring Zero Precedes Element or its Inverse, $(1)$ can be replaced with:
:$(1'): \quad z \ne 0 \implies 0 \prec z \lor 0 \prec -z$, but not both.
As $i \ne 0$, it follows that:
:$0 \prec i$ or $0 \prec -i$
Suppose $0 \prec i$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | o = \prec
      | r = i \times i
      | c = from $(2)$
}}
{{eqn | r = -1
      | c = {{Defof|Complex Number|index = 1}}
}}
{{end-eqn}}
Otherwise, suppose $0 \prec \paren {-i}$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | o = \prec
      | r = \paren {-i} \times \paren {-i}
      | c = from $(2)$
}}
{{eqn | r = -1
      | c = {{Defof|Complex Number|index = 1}}
}}
{{end-eqn}}
Thus by Proof by Cases:
:$0 \prec -1$
Thus it follows that:
{{begin-eqn}}
{{eqn | l = 0
      | o = \prec
      | r = \paren {-1} \times \paren {-1}
      | c = from $(2)$
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
Thus both:
:$0 \prec -1$
and:
:$0 \prec 1$
This contradicts hypothesis $(1')$:
:$(1): \quad z \ne 0 \implies 0 \prec z \lor 0 \prec -z$, but not both
Hence, by Proof by Contradiction, there can be no such ordering.
{{qed}}
Theorem: Complex Numbers cannot be Ordered Compatibly with Ring Structure

Let $\struct {\C, +, \times}$ be the field of complex numbers.
There exists no total ordering on $\struct {\C, +, \times}$ which is compatible with the structure of $\struct {\C, +, \times}$.

Proof:
{{AimForCont}} such a total ordering $\preceq$ exists.
By the definition of a total ordering, $\preceq$ is connected.
That is:
:$0 \preceq i \lor i \preceq 0$
Using Proof by Cases, we will prove that:
:$0 \preceq -1$
;Case 1
Assume that $0 \preceq i$.
By definition of an ordering compatible with the ring structure of $\C$:
:$\forall x, y \in \C: \left({0 \preceq x \land 0 \preceq y}\right) \implies 0 \preceq x \times y$
Substituting $x = i$ and $y = i$ gives:
:$0 \preceq i \times i$
Simplifying:
:$0 \preceq -1$
which is the result required.
;Case 2
Assume that $i \preceq 0$.
By definition of compatibility with addition:
:$\forall x, y, z \in \C: x \preceq y \implies \paren {x + z} \preceq \paren {y + z}$
Substituting $x = i$, $y = 0$, $z = -i$ gives:
:$i + \paren {-i} \preceq 0 + \paren {-i}$
Simplifying:
:$0 \preceq -i$
By definition of an ordering compatible with the ring structure of $\C$:
:$\forall x, y \in \C: \paren {0 \preceq x \land 0 \preceq y} \implies 0 \preceq x \times y$
Substituting $x = -i$ and $y = -i$ gives:
:$0 \preceq \paren {-i} \times \paren {-i}$
Simplifying:
:$0 \preceq -1$
This has been demonstrated to follow from both cases, and so by Proof by Cases:
:$0 \preceq -1$
{{qed|lemma}}
By definition of an ordering compatible with the ring structure of $\C$:
:$\forall x, y \in \C: \paren {0 \preceq x \land 0 \preceq y} \implies 0 \preceq x \times y$
Substituting $x = -1$ and $y = -1$:
:$0 \preceq \paren {-1} \times \paren {-1}$
Simplifying:
:$0 \preceq 1$
By definition of compatibility with addition:
:$\forall x, y, z \in \C: x \preceq y \implies \paren {x + z} \preceq \paren {y + z}$
Substituting $x = 0$, $y = 1$, $z = -1$ gives:
:$0 + \paren {-1} \preceq 1 + \paren {-1}$
Simplifying:
:$-1 \preceq 0$
From the definition of ordering:
:$\forall a, b \in \C: \paren {a \preceq b \land b \preceq a} \implies a = b$
Substituting $a = -1$ and $b = 0$ gives:
:$-1 = 0$
which is a contradiction.
Hence, from Proof by Contradiction, there can be no such ordering.
{{qed}}
Theorem: Complex Numbers cannot be Ordered Compatibly with Ring Structure

Let $\struct {\C, +, \times}$ be the field of complex numbers.
There exists no total ordering on $\struct {\C, +, \times}$ which is compatible with the structure of $\struct {\C, +, \times}$.

Proof:
From Complex Numbers form Integral Domain, $\struct {\C, +, \times}$ is an integral domain.
{{AimForCont}} that $\struct {\C, +, \times}$ can be ordered.
Thus, by definition, it possesses a (strict) positivity property $P$.
Then from Strict Positivity Property induces Total Ordering, let $\le$ be the total ordering induced by $P$.
From Unity of Ordered Integral Domain is Strictly Positive:
:$1$ is strictly positive.
Thus by strict positivity, axiom $3$:
:$-1$ is not strictly positive.
Consider the element $i \in \C$.
By definition of strict positivity, axiom $3$, either:
:$i$ is strictly positive
or:
:$-i$ is strictly positive.
Suppose $i$ is strictly positive.
Then by Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive:
:$i^2 = -1$ is strictly positive.
Similarly, suppose $-i$ is strictly positive.
Then by Square of Non-Zero Element of Ordered Integral Domain is Strictly Positive:
:$\paren {-i}^2 = -1$ is strictly positive.
In both cases we have that $-1$ is strictly positive.
But it has already been established that $-1$ is not strictly positive.
Hence, by Proof by Contradiction, there can be no such ordering.
{{qed}}
Theorem: Limit of Complex Function is Unique

Let $f: S \to \C$ be a complex function.
Let $z_0$ be a limit point of $S$.
Suppose that $\ds \lim_{z \mathop \to z_0} \map f z = L$.
Then that limit $L$ is unique.

Proof:
{{AimForCont}} $L' \ne L$ is another limit point of $\map f z$ at $z_0$.
Let us take $\epsilon = \dfrac {\cmod {L - L'} } 2$.
Then we can find $\delta_1 > 0, \delta_2 > 0$ such that:
:$z \in S, 0 < \cmod {z - z_0} < \delta_1 \implies \cmod {\map f z - L} < \epsilon$
:$z \in S, 0 < \cmod {z - z_0} < \delta_2 \implies \cmod {\map f z - L'} < \epsilon$
Because $z_0$ is a limit point:
:$\exists z^* \in S: 0 < \cmod {z - z_0} < \min \set {\delta_1, \delta_2}$
Then:
{{begin-eqn}}
{{eqn | l = \cmod {L - L'}
      | r = \cmod {L - \map f {z^*} + \map f {z^*} - L'}
      | c = 
}}
{{eqn | o = \le
      | r = \cmod {L - \map f {z^*} } + \cmod {\map f {z^*} - L'}
      | c = Triangle Inequality
}}
{{eqn | o = <
      | r = \epsilon + \epsilon
      | c = 
}}
{{eqn | r = 2 \epsilon
      | c = 
}}
{{end-eqn}}
This contradicts the choice we made of $\epsilon$.
Hence the result by Proof by Contradiction.
{{qed}}
{{wtd|Expand the context to include the more general result for metric spaces etc.}}
Category:Limits of Complex Functions
lss15qo97yke3058fqigrr5zcvp6e77
Theorem: Complex Plane is Metric Space

Let $\C$ be the set of all complex numbers.
Let $d: \C \times \C \to \R$ be the function defined as:
:$\map d {z_1, z_2} = \size {z_1 - z_2}$
where $\size z$ is the modulus of $z$.
Then $d$ is a metric on $\C$ and so $\struct {\C, d}$ is a metric space.

Proof:
Let $z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$.
From the definition of modulus:
:$\size {z_1 - z_2} = \sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2}$
This is the euclidean metric on the real number plane.
This is shown in Euclidean Metric on Real Vector Space is Metric to be a metric.
Thus the complex plane is a 2-dimensional Euclidean space.
{{qed}}
Theorem: Real Number Line is Metric Space

Let $\R$ be the real number line.
Let $d: \R \times \R \to \R$ be defined as:
:$\map d {x_1, x_2} = \size {x_1 - x_2}$
where $\size x$ is the absolute value of $x$.
Then $d$ is a metric on $\R$ and so $\struct {\R, d}$ is a metric space.

Proof:
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map d {x, x}
      | r = \size {x - x}
      | c = Definition of $d$
}}
{{eqn | r = 0
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d$.
{{qed|lemma}}
Theorem: P-Product Metric on Real Vector Space is Metric

Let $\R^n$ be an $n$-dimensional real vector space.
Let $p \in \R_{\ge 1}$.
Let $d_p: \R^n \times \R^n \to \R$ be the $p$-product metric on $\R^n$:
:$\ds \map {d_p} {x, y} := \paren {\sum_{i \mathop = 1}^n \size {x_i - y_i}^p}^{\frac 1 p}$
where $x = \tuple {x_1, x_2, \ldots, x_n}, y = \tuple {y_1, y_2, \ldots, y_n} \in \R^n$.
Then $d_p$ is a metric.

Proof:
This is an instance of $p$-Product Metric is Metric.
{{qed}}
Theorem: Taxicab Metric is Metric

The taxicab metric is a metric.

Proof:
From the definition, the taxicab metric is as follows:
Let $M_{1'} = \struct {A_{1'}, d_{1'} }, M_{2'} = \struct {A_{2'}, d_{2'} }, \ldots, M_{n'} = \struct {A_{n'}, d_{n'} }$ be a finite number of metric spaces.
Let $\AA$ be the Cartesian product $\ds \prod_{i \mathop = 1}^n A_{i'}$.
The taxicab metric on $\AA$ is:
:$\ds \map {d_1} {x, y} = \sum_{i \mathop = 1}^n \map {d_{i'} } {x_{i'}, y_{i'} }$
for $x = \tuple {x_1, x_2, \ldots, x_n}, y = \tuple {y_1, y_2, \ldots, y_n} \in \AA$.
=== Proof of {{Metric-space-axiom|1|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_1} {x, x}
      | r = \sum_{i \mathop = 1}^n \map {d_{i'} } {x_{i'}, x_{i'} }
      | c = Definition of $d_1$
}}
{{eqn | r = \sum_{i \mathop = 1}^n 0
      | c = as $d_{i'}$ fulfills {{Metric-space-axiom|1}}
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
So {{Metric-space-axiom|1}} holds for $d_1$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|2|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_1} {x, y} + \map {d_1} {y, z}
      | r = \sum_{i \mathop = 1}^n \map {d_{i'} } {x_{i'}, y_{i'} } + \sum_{i \mathop = 1}^n \map {d_{i'} } {y_{i'}, z_{i'} }
      | c = Definition of $d_1$
}}
{{eqn | r = \sum_{i \mathop = 1}^n \paren {\map {d_{i'} } {x_{i'}, y_{i'} } + \map {d_{i'} } {y_{i'}, z_{i'} } }
      | c = 
}}
{{eqn | o = \ge
      | r = \sum_{i \mathop = 1}^n \map {d_{i'} } {x_{i'}, z_{i'} }
      | c = as $d_{i'}$ fulfills {{Metric-space-axiom|2}}
}}
{{eqn | r = \map {d_1} {x, z}
      | c = Definition of $d_1$
}}
{{end-eqn}}
So {{Metric-space-axiom|2}} holds for $d_1$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|3|nolink}} ===
{{begin-eqn}}
{{eqn | l = \map {d_1} {x, y}
      | r = \sum_{i \mathop = 1}^n \map {d_{i'} } {x_{i'}, y_{i'} }
      | c = Definition of $d_1$
}}
{{eqn | r = \sum_{i \mathop = 1}^n \map {d_{i'} } {y_{i'}, x_{i'} }
      | c = as $d_{i'}$ fulfills {{Metric-space-axiom|3}}
}}
{{eqn | r = \map {d_1} {y, x}
      | c = Definition of $d_1$
}}
{{end-eqn}}
So {{Metric-space-axiom|3}} holds for $d_1$.
{{qed|lemma}}
=== Proof of {{Metric-space-axiom|4|nolink}} ===
{{begin-eqn}}
{{eqn | l = x
      | o = \ne
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists i \in \set {1, 2, \ldots, n}
      | l = x_i
      | o = \ne
      | r = y_i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_{i'} } {x_{i'}, y_{i'} }
      | o = >
      | r = 0
      | c = as $d_{i'}$ fulfills {{Metric-space-axiom|4}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{i \mathop = 1}^n \map {d_{i'} } {x_{i'}, y_{i'} }
      | o = >
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map {d_1} {x, y}
      | o = >
      | r = 0
      | c = Definition of $d_1$
}}
{{end-eqn}}
So {{Metric-space-axiom|4}} holds for $d_1$.
{{qed}}
Theorem: Taxicab Metric is Metric

The taxicab metric is a metric.

Proof:
Follows directly from P-Product Metric is Metric, where in this case $p = 1$.
{{qed}}
Theorem: Zero and One are the only Consecutive Perfect Squares

If $n$ is a perfect square other than $0$, then $n+1$ is not a perfect square.

Proof:
Let $x$ and $h$ be integers such that:
:$x^2 + 1 = \paren {x - h}^2$
Then:
{{begin-eqn}}
{{eqn | l = x^2 + 1
      | r = \paren {x - h}^2
}}
{{eqn | l = 1
      | r = -2 x h + h^2
}}
{{eqn | l = 2 x h
      | r = h^2 - 1
}}
{{eqn | l = 2 x h
      | r = \paren {h - 1} \paren {h + 1}
}}
{{end-eqn}}
We have that Consecutive Integers are Coprime.
However by the Fundamental Theorem of Arithmetic, both sides must have the same unique prime decomposition.
Therefore $h$ cannot have any prime factors since they cannot be shared by $\paren {h - 1} \paren {h + 1}$.
This leaves $h = -1$, $h = 0$, or $h = 1$ as the only possibilities since they are the only integers with no prime factors.
If $h = -1$ then $h + 1 = 0$, so $2 x h = 0$.
It follows that $x = 0$.
If $h = 1$ then $h - 1 = 0$, so $2 x h = 0$.
It follows that $x = 0$.
If $h = 0$, then $2 x \cdot 0 = \paren {-1} \paren 1$, which is a contradiction.
Therefore the only pairs of consecutive squares are:
:$0^2 = 0$ and $\paren {0 + \paren {-1} }^2 = \paren {-1}^2 = 1$
and:
:$0^2 = 0$ and $\paren {0 + 1}^2 = 1^2 = 1$
{{qed}}