avewright/proofwiki-math huggingface dataset:
Theorem: Isomorphism Preserves Right Cancellability

Let $\struct {S, \circ}$ and $\struct {T, *}$ be algebraic structures.
Let $\phi: \struct {S, \circ} \to \struct {T, *}$ be an isomorphism.
Then:
:$a \in S$ is right cancellable in $\struct {S, \circ}$ {{iff}} $\map \phi a \in T$ is right cancellable in $\struct {T, *}$.

Proof:
Let $a$ be right cancellable in $\struct {S, \circ}$.
Let $x \in S$ and $y \in S$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi x * \map \phi a
      | r = \map \phi y * \map \phi a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \phi {x \circ a}
      | r = \map \phi {y \circ a}
      | c = Morphism property
}}
{{eqn | ll= \leadsto
      | l = \map \phi x
      | r = \map \phi y
      | c = as $a$ is right cancellable
}}
{{end-eqn}}
That is, $\map \phi a$ is right cancellable in $T$.
As $\phi$ is an isomorphism, then so is $\phi^{-1}$.
So the same proof works in reverse in exactly the same way.
{{qed}}
Theorem: Differentiation of Real Power Series

Let $\xi \in \R$ be a real number.
Let $\sequence {a_n}$ be a sequence in $\R$.
Let $\ds \sum_{m \mathop \ge 0} a_m \paren {x - \xi}^m$ be the power series in $x$ about the point $\xi$.
Then within the interval of convergence:
:$\ds \frac {\d^n} {\d x^n} \sum_{m \mathop \ge 0} a_m \paren {x - \xi}^m = \sum_{m \mathop \ge n} a_m m^{\underline n} \paren {x - \xi}^{m - n}$
where $m^{\underline n}$ denotes the falling factorial.

Proof:
First we can make the substitution $z = x - \xi$ and convert the expression into:
:$\ds \dfrac {\d^n} {\d x^n} \sum_{m \mathop \ge 0} a_m z^m$
We then use $n$th Derivative of $m$th Power:
:$\dfrac {\d^n} {\d z^n} z^m = \begin{cases} m^{\underline n} z^{m - n} & : n \le m \\ 0 & : n > m \end{cases}$
$x$ is {{hypothesis}} within the interval of convergence.
It follows from Abel's Theorem that:
:$\ds \frac {\d^n} {\d z^n} \sum_{m \mathop \ge 0} a_m z^m = \sum_{m \mathop \ge n} a_m m^{\underline n} z^{m - n}$
Then from Derivative of Identity Function and others, we have:
:$\map {\dfrac \d {\d x} } {x - \xi} = 1$
The result follows from the Chain Rule for Derivatives.
{{qed}}
{{Handwaving|An explanation needed for how Abel's Theorem allows term-by-term differentiation of the infinite power series.}}
Category:Differentiation of Real Power Series
Category:Differential Calculus
Category:Real Power Series
bu6k253yne8hxrdk3yxhyrsn1kzu3j5
Theorem: General Associativity Theorem/Formulation 1

Let $\struct {S, \circ}$ be a semigroup.
Let $\sequence {a_k}_{p + 1 \mathop \le k \mathop \le p + n}$ be a sequence of elements of $S$.
Let $\sequence {r_k}_{0 \mathop \le k \mathop \le s}$ be a strictly increasing sequence of natural numbers such that $r_0 = p$ and $r_s = p+n$.
Suppose:
:$\ds \forall k \in \closedint 1 s: b_k = \prod_{j \mathop = r_{k - 1} \mathop + 1}^{r_k} {a_j}$
Then:
:$\ds \forall n \in \N_{>0}: \prod_{k \mathop = 1}^s {b_k} = \prod_{k \mathop = p \mathop + 1}^{p \mathop + n} {a_k}$
That is:
:$\ds \forall n \in \N_{>0}: \prod_{k \mathop = 1}^s \paren {a_{r_{k - 1} + 1} \circ a_{r_{k - 1} + 2} \circ \ldots \circ a_{r_k} } = a_{p + 1} \circ \ldots \circ a_{p + n}$

Proof:
The proof will proceed by the Principle of Mathematical Induction on $\N$.
Let $T$ be the set of all $n \in \N_{>0}$ such that:
:$(1): \quad$ for every sequence $\sequence {a_k}_{p + 1 \mathop \le k \mathop \le p + n}$ of elements of $S$
and:
:$(2): \quad$ for every strictly increasing sequence $\sequence {r_k}_{0 \mathop \le k \mathop \le s}$ of natural numbers such that $r_0 = p$ and $r_s = p + n$:
the statement:
:$\ds b_k = \prod_{j \mathop = r_{k - 1} \mathop + 1}^{r_k} a_j$
holds.
Theorem: General Associativity Theorem/Formulation 2

Let $n \in \N_{>0}$ and let $a_1, \ldots, a_n$ be elements of a set $S$.
Let $\circ$ be an associative operation on $S$.
Let the set $\map {P_n} {a_1, a_2, \ldots, a_n}$ be defined inductively by:
:$\map {P_1} {a_1} = \set {a_1}$
:$\map {P_2} {a_1, a_2} = \set {a_1 \circ a_2}$
:$\map {P_n} {a_1, a_2, \ldots, a_n} = \set {x \circ y: x \in \map {P_r} {a_1, a_2, \ldots, a_r} \land y \in \map {P_s} {a_{r + 1}, a_{r + 2}, \ldots, a_{r + s} }, n = r + s}$
Then $\map {P_n} {a_1, a_2, \ldots, a_n}$ consists of a unique entity which we can denote $a_1 \circ a_2 \circ \ldots \circ a_n$.

Proof:
The cases where $n = 1$ and $n = 2$ are clear.
Let $a = x \circ y \in P_n: x \in P_r, y \in P_s$.
If $r > 1$ then we write $x = a_1 \circ z$ where $z = a_2 \circ a_3 \circ \ldots \circ a_r$ by induction.
Then $x \circ y = \paren {a_1 \circ z} \circ y = a_1 \circ \paren {z \circ y} = a_1 \circ \paren {a_2 \circ a_3 \circ \ldots \circ a_n}$ (again by induction).
If $r = 1$, then by induction $x \circ y = a_1 \circ y = a_1 \circ \paren {a_2 \circ a_3 \circ \ldots \circ a_n}$.
Thus in either case, $x \circ y = a_1 \circ \paren {a_2 \circ a_3 \circ \ldots \circ a_n}$ which is a single element of $P_n$.
Hence we see that $\map {P_n} {a_1, a_2, \ldots, a_n}$ consists of a single element.
{{Qed}}
Theorem: Monoid of Self-Inverse Elements is Abelian Group

Let $\struct {S, \circ}$ be a monoid such that:
:$\forall x \in S: x \circ x = e$
where $e$ is the identity element of $\struct {S, \circ}$.
Then $\struct {S, \circ}$ is an abelian group.

Proof:
From Equivalence of Definitions of Self-Inverse, $x \circ x = e \implies x = x^{-1}$.
From Inverse in Monoid is Unique, it follows that every element of $\struct {S, \circ}$ has a unique inverse.
So by definition, $\struct {S, \circ}$ is a group.
From All Elements Self-Inverse then Abelian, it follows that $\struct {S, \circ}$ is an abelian group.
{{qed}}
Theorem: Product is Left Identity Therefore Left Cancellable

Let $\struct {S, \circ}$ be a semigroup.
Let $e_L \in S$  be a left identity of $S$.
Let $a \in S$ such that:
:$\exists b \in S: b \circ a = e_L$
Then $a$ is left cancellable in $\struct {S, \circ}$.

Proof:
Let $x, y \in S$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = a \circ x
      | r = a \circ y
      | c = {{Semigroup-axiom|0}}
}}
{{eqn | ll= \leadsto
      | l = b \circ \paren {a \circ x}
      | r = b \circ \paren {a \circ y}
      | c = {{Semigroup-axiom|0}}
}}
{{eqn | ll= \leadsto
      | l = \paren {b \circ a} \circ x
      | r = \paren {b \circ a} \circ y
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = e_L \circ x
      | r = e_L \circ y
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = {{Defof|Left Identity}}
}}
{{end-eqn}}
The result follows by definition of left cancellable.
{{qed}}
Theorem: Product is Right Identity Therefore Right Cancellable

Let $\struct {S, \circ}$ be a semigroup.
Let $e_R \in S$  be a right identity of $S$.
Let $a \in S$ such that:
:$\exists b \in S: a \circ b = e_R$
Then $a$ is right cancellable in $\struct {S, \circ}$.

Proof:
Let $x, y \in S$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = x \circ a
      | r = y \circ a
      | c = {{Semigroup-axiom|0}}
}}
{{eqn | ll= \leadsto
      | l = \paren {x \circ a} \circ b
      | r = \paren {y \circ a} \circ b
      | c = {{Semigroup-axiom|0}}
}}
{{eqn | ll= \leadsto
      | l = x \circ \paren {a \circ b}
      | r = y \circ \paren {a \circ b}
      | c = {{Semigroup-axiom|1}}
}}
{{eqn | ll= \leadsto
      | l = x \circ e_R
      | r = y \circ e_R
      | c = {{hypothesis}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = {{Defof|Right Identity}}
}}
{{end-eqn}}
The result follows by definition of right cancellable.
{{qed}}
Theorem: Integer Multiples Greater than Positive Integer Closed under Addition

Let $n \Z$ be the set of integer multiples of $n$.
Let $p \in \Z: p \ge 0$ be a positive integer.
Let $S \subseteq n \Z$  be defined as:
:$S := \set {x \in n \Z: x > p}$
that is, the set of integer multiples of $n$ greater than $p$.
Then the algebraic structure $\struct {S, +}$ is closed under addition.

Proof:
Let $x, y \in S$.
From Integer Multiples Closed under Addition, $x + y \in n \Z$.
As $x, y > p$ we have that:
:$\exists r \in \Z_{>0}: x = p + r$
:$\exists s \in \Z_{>0}: y = p + s$
Thus it follows that:
{{begin-eqn}}
{{eqn | l = x + y
      | r = \paren {p + r} + \paren {p + s}
      | c = 
}}
{{eqn | r = 2 p + r + s
      | c = 
}}
{{eqn | o = >
      | r = p
      | c = as $r, s > 0$
}}
{{end-eqn}}
So $x + y > p$ and $x + y \in n \Z$.
Hence by definition $x + y \in S$, and so $S$ is closed under addition.
{{qed}}
Theorem: Integer Multiples Greater than Positive Integer Closed under Multiplication

Let $n \Z$ be the set of integer multiples of $n$.
Let $p \in \Z: p \ge 0$ be a positive integer.
Let $S \subseteq n \Z$  be defined as:
:$S := \set {x \in n \Z: x > p}$
that is, the set of integer multiples of $n$ greater than $p$.
Then the algebraic structure $\struct {S, \times}$ is closed under multiplication.

Proof:
Let $x, y \in S$.
From Integer Multiples Closed under Multiplication, $x y \in n \Z$.
As $x, y > p$ we have that:
:$\exists r \in \Z_{>0}: x = p + r$
:$\exists s \in \Z_{>0}: y = p + s$
Thus it follows that:
{{begin-eqn}}
{{eqn | l = x + y
      | r = \paren {p + r} \paren {p + s}
      | c = 
}}
{{eqn | r = p^2 + p \paren {r + s} + r s
      | c = 
}}
{{eqn | o = >
      | r = p
      | c = as $r, s > 0$
}}
{{end-eqn}}
So $x y > p$ and $x y \in n \Z$.
Hence by definition $x y \in S$, and so $S$ is closed under multiplication.
{{qed}}
Theorem: Non-Zero Rational Numbers Closed under Multiplication

The set of non-zero rational numbers is closed under multiplication.

Proof:
Recall that Rational Numbers form Field under the operations of addition and multiplication.
By definition of a field, the algebraic structure $\struct {\Q_{\ne 0}, \times}$ is a group.
Thus, by definition, $\times$ is closed in $\struct {\Q_{\ne 0}, \times}$.
{{qed}}
Theorem: Non-Zero Real Numbers Closed under Multiplication

The set of non-zero real numbers is closed under multiplication:
:$\forall x, y \in \R_{\ne 0}: x \times y \in \R_{\ne 0}$

Proof:
Recall that Real Numbers form Field under the operations of addition and multiplication.
By definition of a field, the algebraic structure $\struct {\R_{\ne 0}, \times}$ is a group.
Thus, by definition, $\times$ is closed in $\struct {\R_{\ne 0}, \times}$.
{{qed}}
Theorem: Non-Zero Real Numbers Closed under Multiplication

The set of non-zero real numbers is closed under multiplication:
:$\forall x, y \in \R_{\ne 0}: x \times y \in \R_{\ne 0}$

Proof:
Let $x \times y = 0$.
{{WLOG}}, suppose that $x \ne 0$.
Then:
{{begin-eqn}}
{{eqn | l = x \times y
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 1 x \times \paren {x \times y}
      | r = \frac 1 x \times 0
      | c = as $x \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \paren {\frac 1 x \times x} \times y
      | r = \frac 1 x \times 0
      | c = {{Real-number-axiom|M1}}
}}
{{eqn | ll= \leadsto
      | l = 1 \times y
      | r = \frac 1 x \times 0
      | c = {{Real-number-axiom|M4}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = \frac 1 x \times 0
      | c = {{Real-number-axiom|M3}}
}}
{{eqn | ll= \leadsto
      | l = y
      | r = 0
      | c = Real Zero is Zero Element
}}
{{end-eqn}}
Thus:
:$x \times y = 0, x \ne 0 \implies y = 0$
And {{mutatis}}:
:$x \times y = 0, y \ne 0 \implies x = 0$
and so:
:$x \times y = 0 \implies y = 0 \lor x = 0$
So:
{{begin-eqn}}
{{eqn | o = 
      | r = x \times y = 0
      | c = 
}}
{{eqn | o = \leadsto
      | r = \paren {x = 0} \lor \paren {y = 0}
      | c = 
}}
{{eqn | o = \leadsto
      | r = \neg \paren {x \ne 0 \land y \ne 0}
      | c = De Morgan's Laws: Disjunction
}}
{{end-eqn}}
The result follows by the Rule of Transposition.
{{qed}}
Theorem: Non-Zero Complex Numbers are Closed under Multiplication

The set of non-zero complex numbers is closed under multiplication.

Proof:
Recall that Complex Numbers form Field under the operations of addition and multiplication.
By definition of a field, the algebraic structure $\struct {\C_{\ne 0}, \times}$ is a group.
Thus, by definition, $\times$ is closed in $\struct {\C_{\ne 0}, \times}$.
{{qed}}
Theorem: Non-Zero Complex Numbers are Closed under Multiplication

The set of non-zero complex numbers is closed under multiplication.

Proof:
Let $z_1, z_2 \in \C_{\ne 0}$.
Then by definition of complex number:
:$z_1 = x_1 + i y_1, z_2 = x_2 + i y_2$
for some $x_1, y_1, x_2, y_2 \in \R$ such that:
:$x_1 \ne 0$ or $y_1 \ne 0$
:$x_2 \ne 0$ or $y_2 \ne 0$
Expressing $z_1$ and $z_2$ in exponential form (although polar form is equally adequate):
:$z_1 = r_1 e^{i \theta_1}$ and $z_2 = r_2 e^{i \theta_2}$
for some $r_1, r_2, \theta_1, \theta_2 \in \R$.
Then by Product of Complex Numbers in Polar Form:
:$z_1 \times z_2 = \paren {r_1 \times r_2} e^{i \paren {\theta_1 + \theta_2} }$
By definition of exponential form:
:$r_1 = \sqrt {x_1^2 + y_1^2}$
:$r_2 = \sqrt {x_2^2 + y_2^2}$
Thus $r_1 > 0$ and $r_2 > 0$.
Hence $r_1 \times r_2 > 0$ and so $z_1 \times z_2 \ne 0$.
{{qed}}
Theorem: Non-Zero Complex Numbers are Closed under Multiplication

The set of non-zero complex numbers is closed under multiplication.

Proof:
Equivalently this is to say:
:$z_1 z_2 = 0 \implies z_1 = 0 \lor z_2 = 0$
Let $z_1 z_2 = 0$.
{{begin-eqn}}
{{eqn | l = z_1
      | r = \tuple {x_1, y_1}
      | c = {{Defof|Complex Number|index = 2}}: for some $x_1, y_1 \in \R$
}}
{{eqn | l = z_2
      | r = \tuple {x_2, y_2}
      | c = {{Defof|Complex Number|index = 2}}: for some $x_2, y_2 \in \R$
}}
{{eqn | ll= \leadsto
      | l = z_1 z_2
      | r = \tuple {x_1 x_2 - y_1 y_2, x_1 y_2 + y_1 x_2}
      | c = {{Defof|Complex Number/Definition 2/Multiplication|Complex Multiplication}}
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = x_1 x_2
      | r = y_1 y_2
      | c = 
}}
{{eqn | n = 2
      | lo= \land
      | l = x_1 y_2
      | r = -y_1 x_2
      | c = as $z_1 z_2 = 0$
}}
{{end-eqn}}
{{WLOG}}, let $\tuple {x_2, y_2} \ne \tuple {0, 0}$.
Then:
{{begin-eqn}}
{{eqn | l = x_1 x_2 y_2
      | r = y_1 y_2^2
      | c = Multiply $(1)$ by $y_2$
}}
{{eqn | l = x_1 x_2 y_2
      | r = -y_1 x_2^2
      | c = Multiply $(2)$ by $x_2$
}}
{{eqn | ll= \leadsto
      | l = y_1 y_2^2
      | r = -y_1 x_2^2
      | c = Equality is Transitive
}}
{{eqn | ll= \leadsto
      | l = y_1 y_2^2 + y_1 x_2^2
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = y_1 \paren {y_2^2 + x_2^2}
      | r = 0
      | c = Real Multiplication Distributes over Addition
}}
{{eqn | ll= \leadsto
      | l = y_1 = 0
      | o = \vee
      | r = y_2^2 + x_2^2 = 0
      | c = Non-Zero Real Numbers Closed under Multiplication
}}
{{eqn | ll= \leadsto
      | l = y_1 = 0
      | o = 
      | c = $\tuple {x_2, y_2} \neq \tuple {0, 0}$
}}
{{end-eqn}}
From here, we can now write $(1)$ and $(2)$ as
{{begin-eqn}}
{{eqn | n = 1
      | l = x_1 x_2
      | r = 0
}}
{{eqn | n = 2
      | l = x_1 y_2
      | r = 0
}}
{{end-eqn}}
Since Non-Zero Real Numbers Closed under Multiplication, and at least one of $x_2$ and $y_2$ is not zero, $x_1 = 0$.
Thus:
:$\tuple {x_1, y_1} = \tuple {0, 0}$
{{qed}}
Theorem: Non-Zero Modulo Numbers Closed under Multiplication then Modulo is Prime

Let $\struct {\Z_m, +_m, \times_m}$ be the ring of integers modulo $m$ for $m > 1$.
Let $\Z'_m$ be the set of non-zero integers modulo $m$.
Let $\struct {\Z_m, \times_m}$ be closed under modulo multiplication.
Then $m$ is prime.

Proof:
Suppose $m$ is not prime.
Then $m = r s$ for some $r, s \in \Z: 1 < r < m, 1 < s < m$.
So $r, s \in \Z'_m$.
But:
:$r \times_m s \equiv 0 \pmod m$
and so $r \times_m s \notin \Z'_m$.
So if $m$ is not prime, $\struct {\Z_m, \times_m}$ is not closed.
The result follows from the Rule of Transposition.
{{qed}}
Theorem: Magma is Submagma of Itself

Let $\struct {S, \circ}$ be a magma.
Then $\struct {S, \circ}$ is a submagma of itself.

Proof:
By definition, a magma is an algebraic structure $\struct {S, \circ}$ where $\circ$ is closed.
That is:
:$\forall x, y \in S: x \circ y \in S$
From Set is Subset of Itself, $S \subseteq S$.
By definition, $\struct {T, \circ}$ is a submagma of $S$ if:
:$\forall x, y \in T: x \circ y \in T$
It follows from the above that $\struct {S, \circ}$ is, by definition, a submagma of itself.
{{qed}}
Theorem: Empty Set is Submagma of Magma

Let $\struct {S, \circ}$ be a magma.
Then:
:$\struct {\O, \circ}$ is a submagma of $\struct {S, \circ}$
where $\O$ is the empty set.

Proof:
By definition, a magma is an algebraic structure $\struct {S, \circ}$ where $\circ$ is closed.
That is:
:$\forall x, y \in S: x \circ y \in S$
By definition, $\struct {T, \circ}$ is a submagma of $S$ if:
:$\forall x, y \in T: x \circ y \in T$
But:
:$\not \exists x, y \in \O: x \circ y \notin \O$
it follows vacuously that:
:$\forall x, y \in \O: x \circ y \in \O$
Hence the result.
{{Qed}}
Theorem: Max Operation on Toset forms Semigroup

Let $\struct{S, \preceq}$ be a totally ordered set.
Let $\map \max {x, y}$ denote the max operation on $x, y \in S$.
Then $\struct{S, \max}$ is a semigroup.

Proof:
By the definition of the max operation, either:
:$\map \max {x, y}= x$
or
:$\map \max {x, y}= y$
So $\max$ is closed on $S$.
From Max Operation is Associative:
:$\forall x, y, z \in S: \map \max {x, \map \max {y, z}} = \map \max {\map \max {x, y}, z}$
Hence the result, by definition of semigroup.
{{qed}}
Theorem: Min Semigroup on Toset forms Semilattice

Let $\struct {S, \preceq}$ be a totally ordered set. 
Then the min semigroup $\struct {S, \min}$ is a semilattice.

Proof:
We have:
:Min Semigroup is Commutative
:Min Semigroup is Idempotent.
Hence the result, by definition of a semilattice.
{{qed}}
Theorem: Min Semigroup is Commutative

Let $\struct {S, \preceq}$ be a totally ordered set. 
Then the semigroup $\struct {S, \min}$ is commutative.

Proof:
Let $x, y \in S$. 
From Min Operation is Commutative:
:$\map \min {x, y} = \map \min {y, x}$
Hence the result, by definition of commutative semigroup.
{{qed}}
Theorem: Min Semigroup is Idempotent

Let $\struct {S, \preceq}$ be a totally ordered set.
Then the semigroup $\struct {S, \min}$ is an idempotent semigroup.

Proof:
The fact that $\struct {S, \min}$ is a semigroup is demonstrated in Min Operation on Toset forms Semigroup.
Then the min operation is idempotent:
:$\forall x \in S: \min \set {x, x} = x$
The result follows by the definition of idempotent semigroup.
{{qed}}
Theorem: Max Operation on Woset is Monoid

Let $\struct {S, \preceq}$ be a well-ordered set.
Let $\max \set {x, y}$ denote the max operation on $x, y \in S$.
Then $\struct {S, \max}$ is a monoid.
Its identity element is the smallest element of $S$.

Proof:
From Well-Ordering is Total Ordering, we have that $\struct {S, \preceq}$ is a totally ordered set.
Thus, by Max Operation on Toset forms Semigroup, $\struct {S, \max}$ is a semigroup.
By definition, a well-ordered set has a smallest element.
So:
:$\exists m \in S: \forall x \in S: m \preceq x$
where $m$ is that smallest element.
It follows by definition of the max operation that:
:$\forall x \in S: \max \set {m, x} = x$
Thus $m$ is the identity element of $\struct {S, \max}$.
Hence the result, by definition of monoid.
{{qed}}
Category:Max Operation
Category:Well-Orderings
Category:Examples of Monoids
m4kk4nl50mmwkkzqf4q2i0ogmwwpw22
Theorem: Max Operation on Natural Numbers forms Monoid

Let $\struct {\N, \max}$ denote the algebraic structure formed from the natural numbers $\N$ and the max operation.
Then $\struct {\N, \max}$ is a monoid.
Its identity element is zero.

Proof:
By the Well-Ordering Principle, $\N$ is a well-ordered set.
The result follows from Max Operation on Woset is Monoid.
{{qed}}
Theorem: Complex Modulus Function is Continuous

Let $z_0 \in \C$ be a complex number.
Then the complex modulus function is continuous at $z_0$.

Proof:
Let $\epsilon>0$.
Let $z \in \C$ be a complex number satisfying $\left\vert{z - z_0}\right\vert < \epsilon$.
By the Reverse Triangle Inequality:
: $\left\vert{ \left\vert{z}\right\vert - \left\vert{z_0}\right\vert }\right\vert \le \left\vert{z - z_0}\right\vert < \epsilon$
Hence the result, by the $\epsilon$-$\delta$ definition of continuity (taking $\delta = \epsilon$).
{{qed}}
Category:Complex Modulus
Category:Continuous Functions
c5b85ilzan02knmwpgg6iyhjvy62lag
Theorem: Subset of Natural Numbers under Max Operation is Monoid

Let $S \subseteq \N$ be a subset of the natural numbers $\N$.
Let $\struct {S, \max}$ denote the algebraic structure formed from $S$ and the max operation.
Then $\struct {S, \max}$ is a monoid.
Its identity element is the smallest element of $S$.

Proof:
By the Well-Ordering Principle, $\N$ is a well-ordered set.
By definition, every subset of a well-ordered set is also well-ordered.
Thus $S$ is a well-ordered set.
The result follows from Max Operation on Woset is Monoid.
{{qed}}
Theorem: Euclidean Space is Banach Space

Let $m$ be a positive integer.
Then the Euclidean space $\R^m$, along with the Euclidean norm, forms a Banach space over $\R$.

Proof:
The Euclidean space $\R^m$ is a vector space over $\R$.
That the norm axioms are satisfied is proven in Euclidean Space is Normed Vector Space.
Then we have Euclidean Space is Complete Metric Space.
The result follows by the definition of a Banach space.
{{qed}}
Theorem: Euclidean Space is Banach Space

Let $m$ be a positive integer.
Then the Euclidean space $\R^m$, along with the Euclidean norm, forms a Banach space over $\R$.

Proof:
By definition, Euclidean norm is the same as $p$-norm with $p = 2$.
Let $\sequence {\mathbf x_n}_{n \mathop \in \N} = \sequence {\tuple {x_n^{\paren 1}, x_n^{\paren 2}, \ldots, x_n^{\paren m} } }_{n \mathop \in \N} $ be a Cauchy sequence in $\R^m$.
Let $k \in \N_{> 0} : k \le m$.
Then:
{{begin-eqn}}
{{eqn | l = \size {x_n^{\paren k} - x_m^{\paren k} }
      | r = \paren {\paren {x_n^{\paren k} - x_m^{\paren k} }^2}^{\frac 1 2}
}}
{{eqn | o = \le
      | r = \paren {\sum_{k \mathop = 0}^m \paren {x_n^{\paren k} - x_m^{\paren k} }^2}^{\frac 1 2}
}}
{{eqn | r = \norm { {\bf x}_n - {\bf x}_m}_2
}}
{{end-eqn}}
Hence, $\sequence {x_n^{\paren k} }_{n \mathop \in \N}$ is a Cauchy sequence in $\R$.
Then:
:$\ds \lim_{n \mathop \to \infty} x_n^{\paren k} = L^{\paren k}$
Let $\mathbf L = \tuple {L^{\paren 1}, \ldots, L^{\paren m}} \in \R^m$
We have that for all $n > N$:
{{begin-eqn}}
{{eqn | l = \norm {\mathbf x_n - \mathbf L}
      | r = \paren {\sum_{k \mathop = 1}^m \size {x^{\paren k}_n - x^{\paren k} }^2}^{\frac 1 2}
}}
{{eqn | o = \le
      | r = \paren {\sum_{k \mathop = 1}^m \frac {\epsilon^2} m}^{\frac 1 2}
}}
{{eqn | r = \epsilon
}}
{{end-eqn}}
Therefore, $\sequence {\mathbf x_n}_{n \mathop \in \N}$ converges to $\mathbf L$ in $\struct {\R^m, \norm {\, \cdot \,}_2}$.
{{qed}}
Theorem: Complex Plane is Complete Metric Space

The complex plane, along with the metric induced by the norm given by the complex modulus, forms a complete metric space.

Proof:
Let $z = x + iy$ be a complex number, where $x, y \in \R$.
Now, we can identify the complex number $z$ with the ordered pair $\left( x, y \right) \in \R^2$.
The norm on $\C$ given by the complex modulus is then identical to the Euclidean norm on $\R^2$.
Therefore, metric on $\C$ induced by the norm given by the complex modulus is identical to the Euclidean metric on $\R^2$ induced by the Euclidean norm.
By Euclidean Space is Complete Metric Space, $\C$ is a complete metric space.
{{qed}}
Theorem: Euclidean Space is Complete Metric Space

Let $m$ be a positive integer.
Then the Euclidean space $\R^m$, along with the Euclidean metric, forms a complete metric space.

Proof:
Let $\sequence {\tuple {x_{n, 1}, x_{n, 2}, \ldots, x_{n, m} } }_{n \mathop \in \N} $ be a Cauchy sequence in $\R^m$.
Let $\epsilon > 0$.
Then $\dfrac \epsilon m > 0$.
We have that Real Number Line is Complete Metric Space.
Therefore:
:$\exists y_1, y_2, \ldots, y_m \in \R$ and $N_1, N_2, \ldots, N_m \in \N$ (depending on $\epsilon$)
such that:
:$\forall k \in \N: 1 \le k \le m: \forall n_k > N_k: \sequence {x_{n, k} – y_k}  < \dfrac \epsilon m$
From Euclidean Space is Normed Vector Space:
:$\ds \norm {\tuple {x_{n, 1}, x_{n, 2}, \ldots, x_{n, m} } - \tuple {y_1, y_2, \ldots, y_m} } \le \sum_{k \mathop = 1}^m \size {x_{n, k} – y_k} < \epsilon$
Hence the Euclidean space is a complete metric space.
{{qed}}