avewright/proofwiki-math huggingface dataset:
Theorem: Weierstrass Product Theorem

Let $\sequence {a_k}$ be a sequence of non-zero complex numbers such that:
:$\cmod {a_n} \to \infty$ as $n \to \infty$
Let $\sequence {p_n}$ be a sequence of non-negative integers for which the series:
:$\ds \sum_{n \mathop = 1}^\infty \size {\dfrac r {a_n} }^{1 + p_n}$
converges for every $r \in \R_{> 0}$.
Let:
:$\ds \map f z = \prod_{n \mathop = 1}^\infty \map {E_{p_n} } {\frac z {a_n} }$
where $E_{p_n}$ are Weierstrass elementary factors.
Then $f$ is entire and its zeroes are the points $a_n$, counted with multiplicity.

Proof:
By:
:Locally Uniformly Absolutely Convergent Product is Locally Uniformly Convergent
:Infinite Product of Analytic Functions is Analytic
:Zeroes of Infinite Product of Analytic Functions
it suffices to show that the product $\ds \prod_{n \mathop = 1}^\infty \map {E_{p_n} } {\frac z {a_n} }$ converges locally uniformly absolutely.
By Bounds for Weierstrass Elementary Factors and Weierstrass M-Test, this is the case.
{{stub}}
{{qed}}
Theorem: Isomorphism between Gaussian Integer Units and Rotation Matrices Order 4

Let $\struct {U_\C, \times}$ be the group of Gaussian integer units under complex multiplication.
Let $\struct {R_4, \times}$ be the group of rotation matrices of order $4$ under modulo addition.
Then $\struct {U_\C, \times}$ and $\struct {R_4, \times}$ are isomorphic algebraic structures.

Proof:
Establish the mapping $f: U_C \to R_4$ as follows:
{{begin-eqn}}
{{eqn | l = \map f 1
      | r = r_0
}}
{{eqn | l = \map f i
      | r = r_1
}}
{{eqn | l = \map f {-1}
      | r = r_2
}}
{{eqn | l = \map f {-i}
      | r = r_3
}}
{{end-eqn}}
From Isomorphism by Cayley Table, the two Cayley tables can be compared by eye to ascertain that $f$ is an isomorphism:
Theorem: Isomorphism between Gaussian Integer Units and Reduced Residue System Modulo 5 under Multiplication

Let $\struct {U_\C, \times}$ be the group of Gaussian integer units under complex multiplication.
Let $\struct {\Z'_5, \times_5}$ be the multiplicative group of reduced residues modulo $5$.
Then $\struct {U_\C, \times}$ and $\struct {\Z'_5, \times_5}$ are isomorphic algebraic structures.

Proof:
Establish the mapping $f: U_C \to \Z'_5$ as follows:
{{begin-eqn}}
{{eqn | l = \map f 1
      | r = \eqclass 1 5
}}
{{eqn | l = \map f i
      | r = \eqclass 2 5
}}
{{eqn | l = \map f {-1}
      | r = \eqclass 4 5
}}
{{eqn | l = \map f {-i}
      | r = \eqclass 3 5
}}
{{end-eqn}}
From Isomorphism by Cayley Table, the two Cayley tables can be compared by eye to ascertain that $f$ is an isomorphism:
Theorem: Group Generated by Reciprocal of z and Minus z is Klein Four-Group

Let $K_4$ denote the Klein $4$-group.
Let $S$ be the group generated by $1 / z$ and $-z$.
Then $K_4$ and $S$ are isomorphic algebraic structures.

Proof:
Establish the mapping $\phi: K_4 \to S$ as follows:
{{begin-eqn}}
{{eqn | l = \map \phi e
      | r = z
}}
{{eqn | l = \map \phi a
      | r = -z
}}
{{eqn | l = \map \phi b
      | r = \dfrac 1 z
}}
{{eqn | l = \map \phi c
      | r = -\dfrac 1 z
}}
{{end-eqn}}
From Isomorphism by Cayley Table, the two Cayley tables can be compared by eye to ascertain that $\phi$ is an isomorphism:
Theorem: Group of Reflection Matrices Order 4 is Klein Four-Group

Let $K_4$ denote the Klein $4$-group.
Let $R_4$ be the Group of Reflection Matrices Order $4$.
Then $K_4$ and $R_4$ are isomorphic algebraic structures.

Proof:
Establish the mapping $\phi: K_4 \to R_4$ as follows:
{{begin-eqn}}
{{eqn | l = \map \phi e
      | r = r_0
}}
{{eqn | l = \map \phi a
      | r = r_1
}}
{{eqn | l = \map \phi b
      | r = r_2
}}
{{eqn | l = \map \phi c
      | r = r_3
}}
{{end-eqn}}
From Isomorphism by Cayley Table, the two Cayley tables can be compared by eye to ascertain that $\phi$ is an isomorphism:
Theorem: Multiplicative Group of Reduced Residues Modulo 8 is Klein Four-Group

Let $K_4$ denote the Klein $4$-group.
Let $R_4$ be the multiplicative group of reduced residues Modulo $8$.
Then $K_4$ and $R_4$ are isomorphic algebraic structures.

Proof:
Establish the mapping $\phi: K_4 \to R_4$ as follows:
{{begin-eqn}}
{{eqn | l = \map \phi e
      | r = \eqclass 1 8
}}
{{eqn | l = \map \phi a
      | r = \eqclass 3 8
}}
{{eqn | l = \map \phi b
      | r = \eqclass 5 8
}}
{{eqn | l = \map \phi c
      | r = \eqclass 7 8
}}
{{end-eqn}}
From Isomorphism by Cayley Table, the two Cayley tables can be compared by eye to ascertain that $\phi$ is an isomorphism:
Theorem: Klein Four-Group and Group of Cyclic Group of Order 4 are not Isomorphic

The Klein $4$-group $K_4$ and the cyclic group of order $4$ $C_4$ are not isomorphic.

Proof:
Recall the Cayley table for $K_4$:
{{:Klein Four-Group/Cayley Table}}
From Finite Cyclic Group is Isomorphic to Integers under Modulo Addition, $C_4$ can be exemplified using the additive group of integers modulo $4$.
Recall the Cayley table for $\struct {\Z_4, +_4}$:
{{:Modulo Addition/Cayley Table/Modulo 4}}
Note that all elements of $K_4$ are self-inverse.
However, for example:
:$\eqclass 1 4 +_4 \eqclass 1 4 = \eqclass 2 4$
and so $\eqclass 1 4$ is not self-inverse.
Thus there can be no bijection between $K_4$ and $\struct {\Z_4, +_4}$ such that:
:$\forall a, b \in K_4: \map \phi a +_4 \map \phi b = \map \phi {a b}$
Hence the result.
{{qed}}
Theorem: Klein Four-Group and Group of Cyclic Group of Order 4 are not Isomorphic

The Klein $4$-group $K_4$ and the cyclic group of order $4$ $C_4$ are not isomorphic.

Proof:
Note that both $C_4$ and $K_4$ are of order $4$.
Also note that both $C_4$ and $K_4$ are abelian.
By definition, $C_4$ has elements of order $4$.
From Group Isomorphism Preserves Order of Group Element, the image of an element of $C_4$ under an isomorphism to $K_4$ would also be of order $4$.
But $K_4$ has no elements of order $4$.
Hence $C_4$ and $K_4$ are not isomorphic.
{{qed}}
Theorem: Order Generating iff Not Preceding implies There Exists Element Preceding and Not Preceding

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X$ be a subset of $S$.
Then
:$X$ is order generating
{{iff}}
:$\forall x, y \in S: \paren {y \npreceq x \implies \exists p \in X: x \preceq p \land y \npreceq p}$

Proof:
=== Sufficient Condition ===
Let $X$ be order generating.
Let $x, y \in S$ such that:
:$y \npreceq x$
By Order Generating iff Every Element is Infimum:
:$\exists P \subseteq X: x = \inf P$
By definition of infimum:
:$y$ is lower bound for $P \implies y \preceq x$
By definition of lower bound:
:$\exists p \in P: y \npreceq p$
Thus by definition of subset:
:$p \in X$
By definition of infimum:
:$x$ is lower bound for $P$.
Thus by definition of lower bound:
:$x \preceq p$
Thus
:$y \npreceq p$
{{qed|lemma}}
Theorem: Permutation Induces Equivalence Relation/Corollary

:$i \mathrel {\RR_\pi} j$ {{iff}} $i$ and $j$ are in the same cycle of $\pi$.

Proof:
We have that Permutation Induces Equivalence Relation.
The equivalence classes of that equivalence relation are the cycles of $\pi$.
Hence the result by definition of equivalence class.
{{qed}}
Category:Symmetric Groups
Category:Examples of Equivalence Relations
o3tk79kr9ipf4kqz1tdnyyic21qg3h0
Theorem: Order of Group Element not less than Order of Power

Let $\left({G, \circ}\right)$ be a group whose identity is $e$.
Let $g \in G$ be an element of $g$.
Let $\left\lvert{g}\right\rvert$ denote the order of $g$ in $G$.
Then:
:$\forall m \in \Z: \left\lvert{g^m}\right\rvert \le \left\lvert{g}\right\rvert$
where $g^m$ denotes the $m$th power of $g$ in $G$.

Proof:
Let $\left\lvert{g}\right\rvert = n$.
Then from Order of Power of Group Element:
:$\forall m \in \Z: \left\lvert{g^m}\right\rvert = \dfrac n {\gcd \left\{ {m, n}\right\} }$
where $\gcd \left\{ {m, n}\right\}$ denotes the greatest common divisor of $m$ and $n$.
The result follows from Greatest Common Divisor is at least 1.
{{qed}}
Theorem: Order of Group Element not less than Order of Power

Let $\left({G, \circ}\right)$ be a group whose identity is $e$.
Let $g \in G$ be an element of $g$.
Let $\left\lvert{g}\right\rvert$ denote the order of $g$ in $G$.
Then:
:$\forall m \in \Z: \left\lvert{g^m}\right\rvert \le \left\lvert{g}\right\rvert$
where $g^m$ denotes the $m$th power of $g$ in $G$.

Proof:
Let $g^n = e$.
Let $h = g^m$.
Then:
:$h^n = g^{m n} = \paren {g^n}^m = e^m = e$
Hence by definition of order of group element:
:$\order h \le n$
Hence the result.
{{qed}}
Theorem: Order of Group Element equals Order of Coprime Power

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $g \in G$ be an element of $g$.
Let $\order g$ denote the order of $g$ in $G$.
Then:
:$\forall m \in \Z: \order {g^m} = \order g \iff m \perp \order g$
where:
:$g^m$ denotes the $m$th power of $g$ in $G$
:$\perp$ denotes coprimality.

Proof:
Let $\order g = n$.
Then from Order of Power of Group Element:
:$\forall m \in \Z: \order {g^m} = \dfrac n {\gcd \set {m, n}}$
where $\gcd \set {m, n}$ denotes the greatest common divisor of $m$ and $n$.
Thus:
:$\order {g^m} = \order g \iff \gcd \set {m, n} = 1$
The result follows by definition of coprime integers.
{{qed}}
Theorem: Order of Group Element equals Order of Coprime Power

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $g \in G$ be an element of $g$.
Let $\order g$ denote the order of $g$ in $G$.
Then:
:$\forall m \in \Z: \order {g^m} = \order g \iff m \perp \order g$
where:
:$g^m$ denotes the $m$th power of $g$ in $G$
:$\perp$ denotes coprimality.

Proof:
Let $\order g = n$.
=== Necessary Condition ===
Let $m \perp n$.
Then by Bézout's Identity:
:$\exists x, y \in \Z: x m + y n = 1$
Let $h = g^m$.
Then:
:$h^x = g^{m x} = g^{1 - y n} = g g^{- y n} = g e = g$
and so $g$ is also a power of $h$.
Hence from Order of Group Element not less than Order of Power:
:$\order g \le \order h \le \order g$
and it follows that:
:$\order g = \order h$
{{qed|lemma}}
=== Sufficient Condition ===
We prove the contrapositive.
Suppose $m \not \perp n$.
Then:
:$\exists d \in \Z_{>1}: \exists a, b \in \Z: m = a d \land n = b d$
Let $h = g^m$.
Then:
:$h^b = \paren {g^m}^{n/d} = g^{a n} = \paren {g^n}^a = e^a = e$
Hence:
:$\order h \le b < n$
and it follows that:
:$\order g \ne \order h$
{{qed}}
Theorem: Unique Composition of Group Element whose Order is Product of Coprime Integers

Let $\struct {G, \circ}$ be a group whose identity is $e$.
Let $g \in G$ be an element of $g$.
Let:
:$\order g = m n$
where:
:$\order g$ denotes the order of $g$ in $G$
:$m$ and $n$ are coprime integers.
Then $g$ can be expressed uniquely as the product of two commuting elements $a$ and $b$ of order $m$ and $n$ respectively.

Proof:
Let $g_1 = g^n$ and $g_2 = g^m$.
By Powers of Group Element Commute, $g_1$ and $g_2$ commute.
We have:
:${g_1}^m = g^{n m} = e$
:${g_2}^n = g^{m n} = e$
It follows that:
:the order of $g_1$ is $m$
:the order of $g_2$ is $n$
otherwise if either $g_1$ or $g_2$ were of a smaller order then $g$ would also be of a smaller order.
By Bézout's Identity:
:$\exists u, v \in \Z: u n + v m = 1$
as $m \perp n$.
Thus:
:$g = g^{u n + v m} = \paren {g^n}^u \paren {g^m}^v = {g_1}^u {g_2}^v$
Also by Bézout's Identity:
:$u \perp m$
and:
:$v \perp n$
Thus by Order of Group Element equals Order of Coprime Power:
:$\order { {g_1}^u} = m$
and:
:$\order { {g_2}^v} = n$
We have that $g_1$ and $g_2$ commute.
So by Commutativity of Powers in Group, ${g_1}^u$ and ${g_2}^v$ also commute.
Putting $a = g_1^u$ and $b = g_2^v$, we have $a$ and $b$ which satisfy the required conditions.
It remains to prove uniqueness.
Suppose that:
:$(1): \quad g = r_1 r_2 = s_1 s_2$
where:
:$r_1$ and $r_2$ commute
:$s_1$ and $s_2$ commute
:$\order {r_1} = \order {s_1} = m$
:$\order {r_2} = \order {s_2} = n$
Raising $(1)$ to the $n u$th power:
:$g^{n u} = {r_1}^{n u} {r_2}^{n u} = {s_1}^{n u} {s_2}^{n u}$
and so:
{{begin-eqn}}
{{eqn | l = {r_1}^{n u} {r_2}^{n u}
      | r = {s_1}^{n u} {s_2}^{n u}
      | c = 
}}
{{eqn | l = {r_1}^{n u} \paren { {r_2}^n}^u
      | r = {s_1}^{n u} \paren { {s_2}^n}^u
      | c = 
}}
{{eqn | l = {r_1}^{n u} e^u
      | r = {s_1}^{n u} e^u
      | c = as $\order {r_2} = \order {s_2} = n$
}}
{{eqn | ll= \leadsto
      | l = {r_1}^{n u}
      | r = {s_1}^{n u}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {r_1}^{1 - m v}
      | r = {s_1}^{1 - m v}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r_1 \paren { {r_1}^m}^{-v}
      | r = s_1 \paren { {s_1}^m}^{-v}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r_1 e^{-v}
      | r = s_1 e^{-v}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r_1
      | r = s_1
      | c = 
}}
{{end-eqn}}
It follows directly from $(1)$ that $r_2 = s_2$.
Hence the result.
{{qed}}
Theorem: Order of Cyclic Group equals Order of Generator

Let $G$ be a finite cyclic group which is generated by $a \in G$.
Then:
:$\order a = \order G$
where:
:$\order a$ denotes the order of $a$ in $G$
:$\order G$ denotes the order of $G$.

Proof:
Let $\order a = n$.
From List of Elements in Finite Cyclic Group:
:$G = \set {a_0, a_1, \ldots, a_{n - 1} }$
Hence the result.
{{qed}}
Theorem: Group whose Order equals Order of Element is Cyclic

Let $G$ be a finite group of order $n$.
Let $g \in G$ have order $n$.
Then $G$ is a cyclic group which is generated by $g$.

Proof:
The subgroup of $G$ generated by $g$ is:
:$\gen g = \set {g^0, g^1, g^2, \ldots, g^{n - 1} }$
This contains $n$ elements.
Thus:
:$\gen g = G$
and the result follows by definition of cyclic group.
{{qed}}
Theorem: Integer Powers of 2 under Multiplication form Infinite Abelian Group

Let $S$ be the set of integers defined as:
:$S = \set {2^k: k \in \Z}$
Then $\struct {S, \times}$ is an infinite abelian group.

Proof:
It can be seen by inspection that $S \subseteq \Q_{>0}$.
That is, all the elements of $S$ are strictly positive rational numbers.
From Strictly Positive Rational Numbers under Multiplication form Countably Infinite Abelian Group:
:$\struct {\Q_{>0}, \times}$ is an infinite abelian group.
It is noted that $S$ is an infinite set and so trivially $S \ne \O$.
Let $a, b \in S$.
Then:
:$\exists k_1 \in \Z: a = 2^{k_1}$
:$\exists k_2 \in \Z: b = 2^{k_2}$
We have that:
:$\dfrac 1 {2^{k_2} } 2^{k_2} = 1$
and so $\dfrac 1 {2^{k_2} } = 2^{-k_2} = b^{-1}$ is the inverse of $b \in \struct {\Q_{>0}, \times}$.
Then we have:
{{begin-eqn}}
{{eqn | l = a \times b^{-1}
      | r = 2^{k_1} \times \dfrac 1 {2^{k_2} }
      | c = 
}}
{{eqn | r = 2^{k_1 - k_2}
      | c = 
}}
{{end-eqn}}
We have that:
:$k_1 + k_2 \in \Z$
and so $a \times b^{-1} \in \S$.
Hence by the One-Step Subgroup Test, $\struct {S, \times}$ is a subgroup of $\struct {\Q_{>0}, \times}$.
It has been established that $S$ is an infinite set.
Hence by definition $\struct {S, \times}$ is an infinite group.
Finally, from Subgroup of Abelian Group is Abelian, $\struct {S, \times}$ is an abelian group.
{{qed}}
Theorem: Numbers of form 1 + 2m over 1 + 2n form Infinite Abelian Group under Multiplication

Let $S$ be the set of integers defined as:
:$S = \set {\dfrac {1 + 2 m} {1 + 2 n}: m, n \in \Z}$
Then $\struct {S, \times}$ is an infinite abelian group.

Proof:
Let $k \in \Z$.
Then $1 + 2 k \ne 0$.
Thus:
:$\forall x \in S: x \in \Q_{\ne 0}$
Thus by definition of subset:
:$S \subseteq \Q_{\ne 0}$
From Non-Zero Rational Numbers under Multiplication form Infinite Abelian Group:
:$\struct {\Q_{\ne 0}, \times}$ is an infinite abelian group.
It is noted that $S$ is an infinite set and so trivially $S \ne \O$.
Consider $a = \dfrac {1 + 2 m} {1 + 2 n} \in S$.
We have that:
:$\dfrac {1 + 2 m} {1 + 2 n} \times \dfrac {1 + 2 n} {1 + 2 m} = 1$
and so $\dfrac {1 + 2 n} {1 + 2 m}$ is the inverse of $b \in \struct {\Q_{>0}, \times}$.
By inspection it can be seen that $b^{-1} \in S$.
Let $a, b \in S$.
Then:
:$\exists m_1, n_1 \in \Z: a = \dfrac {1 + 2 m_1} {1 + 2 n_1}$
:$\exists m_2, n_2 \in \Z: b = \dfrac {1 + 2 m_2} {1 + 2 n_2}$
Then we have:
{{begin-eqn}}
{{eqn | l = a \times b
      | r = \dfrac {1 + 2 m_1} {1 + 2 n_1} \dfrac {1 + 2 m_2} {1 + 2 n_2}
      | c = 
}}
{{eqn | r = \dfrac {\paren {1 + 2 m_1} \paren {1 + 2 m_2} } {\paren {1 + 2 n_1} \paren {1 + 2 n_2} }
      | c = 
}}
{{eqn | r = \dfrac {1 + 2 m_1 + 2 m_2 + 4 m_1 m_2} {1 + 2 n_1 + 2 n_2 + 4 n_1 n_2}
      | c = 
}}
{{eqn | r = \dfrac {1 + 2 \paren {m_1 + m_2 + 2 m_1 m_2} } {1 + 2 \paren {n_1 + n_2 + 2 n_1 n_2} }
      | c = 
}}
{{eqn | r = \dfrac {1 + 2 m} {1 + 2 n}
      | c = where $m = m_1 + m_2 + 2 m_1 m_2, n = n_1 + n_2 + 2 n_1 n_2$
}}
{{end-eqn}}
Hence by the Two-Step Subgroup Test, $\struct {S, \times}$ is a subgroup of $\struct {\Q_{>0}, \times}$.
It has been established that $S$ is an infinite set.
Hence by definition $\struct {S, \times}$ is an infinite group.
Finally, from Subgroup of Abelian Group is Abelian, $\struct {S, \times}$ is an abelian group.
{{qed}}
Theorem: Circle Group is Group

The circle group $\struct {K, \times}$ is a group.

Proof:
First we note that $K \subseteq \C$.
So to show that $K$ is a group it is sufficient to show that $K$ is a subgroup of the multiplicative group of complex numbers $\struct {\C_{\ne 0}, \times}$.
From Complex Multiplication Identity is One, the identity element $1 + 0 i$ is in $K$.
Thus $K \ne \O$.
We now show that $z, w \in K \implies z w \in K$:
{{begin-eqn}}
{{eqn | l = z, w
      | o = \in
      | r = K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod z
      | r = 1 = \cmod w
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {z w}
      | r = \cmod z \cmod w
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z w
      | o = \in
      | r = K
      | c = 
}}
{{end-eqn}}
Next we see that $z \in K \implies z^{-1} \in K$:
:$\cmod z = 1 \implies \cmod {\dfrac 1 z} = 1$
Thus by the Two-Step Subgroup Test:
:$K \le \C_{\ne 0}$
Thus $K$ is a group.
{{qed}}
Theorem: Circle Group is Group

The circle group $\struct {K, \times}$ is a group.

Proof:
We note that $K \ne \O$ as the identity element $1 + 0 i \in K$.
Since all $z \in K$ have modulus $1$, they have, for some $\theta \in \hointr 0 {2 \pi}$, the polar form:
:$z = \map \exp {i \theta} = \cos \theta + i \sin \theta$
Conversely, if a complex number has such a polar form, it has modulus $1$.
Observe the following property of the complex exponential function:
:$\forall a, b \in \C: \map \exp {a + b} = \map \exp a \map \exp b$
We must show that if $x, y \in K$ then $x \cdot y^{-1} \in K$.
Let $x, y \in K$ be arbitrary.
Choose suitable $s, t \in \hointr 0 {2 \pi}$ such that:
:$x = \map \exp {i s}$
:$y = \map \exp {i t}$
We compute:
{{begin-eqn}}
{{eqn | l = \map \exp {i t} \map \exp {-i t}
      | r = \map \exp {i \paren {t - t} }
}}
{{eqn | r = \map \exp 0
}}
{{eqn | r = 1
}}
{{end-eqn}}
So $y^{-1} = \map \exp {-i t}$.
We note that this lies in $K$.
Furthermore, we have:
{{begin-eqn}}
{{eqn | l = x y
      | r = \map \exp {i s} \map \exp {-2 \pi i t}
}}
{{eqn | r = \map \exp {i \paren {s - t} }
}}
{{end-eqn}}
We conclude that $x y \in K$.
By the Two-Step Subgroup Test, $K$ is a subgroup of $\C$ under complex multiplication.
{{Qed}}
Theorem: Circle Group is Group

The circle group $\struct {K, \times}$ is a group.

Proof:
Taking the group axioms in turn:
=== {{Group-axiom|0|nolink}} ===
{{begin-eqn}}
{{eqn | l = z, w
      | o = \in
      | r = K
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod z
      | r = 1 = \cmod w
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cmod {z w}
      | r = \cmod z \cmod w
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z w
      | o = \in
      | r = K
      | c = 
}}
{{end-eqn}}
So $\struct {K, \times}$ is closed.
{{qed|lemma}}
=== {{Group-axiom|1|nolink}} ===
Complex Multiplication is Associative.
{{qed|lemma}}
=== {{Group-axiom|2|nolink}} ===
From Complex Multiplication Identity is One we have that the identity element of $K$ is $1 + 0 i$.
{{qed|lemma}}
=== {{Group-axiom|3|nolink}} ===
We have that:
:$\cmod z = 1 \implies \dfrac 1 {\cmod z} = \cmod {\dfrac 1 z} = 1$
But:
:$z \times \dfrac 1 z = 1 + 0 i$
So the inverse of $z$ is $\dfrac 1 z$.
{{qed|lemma}}
All the group axioms are satisfied, and the result follows.
{{qed}}
Theorem: Circle Group is Group

The circle group $\struct {K, \times}$ is a group.

Proof:
Consider the complex modulus function $\cmod {\, \cdot \,}: \C \to \R, z \mapsto \cmod z$.
By Complex Modulus is Norm, we have that $\cmod z \ge 0$ for all $z \in \C$, and:
:$\cmod z = 0 \iff z = 0$
Let $\C_{\ne 0} := \C \setminus \set 0$ denote the complex numbers without zero.
From Group of Units of Field and Complex Numbers form Field, we have that $\struct {\C_{\ne 0}, \times}$ is a group.
By the above observation, the modulus has a restriction to $\C_{\ne 0}$:
:$\cmod {\, \cdot \,}: \C_{\ne 0} \to \R_{>0}, z \mapsto \cmod z$
From $\cmod 1 = 1$ and Modulus of Product, it follows that $\phi$ is in fact a group homomorphism:
:$\phi: \struct {C_{\ne 0}, \times} \to \struct {\R_{>0}, \times}, z \mapsto \cmod z$
Now $K$ is by definition the kernel of $\phi$.
Hence, by Kernel of Group Homomorphism is Subgroup, $\struct {K, \times}$ is a subgroup of $\struct {\C_{\ne 0}, \times}$.
{{qed}}
Theorem: Set of Meet Irreducible Elements Excluded Top is Order Generating

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a continuous complete lattice.
Let $X = \map {\mathit {IRR} } L \setminus \set \top$
where:
:$\map {\mathit {IRR} } L$ denotes the set of all meet irreducible element of $S$
:$\top$ denotes the top of $L$.
Then $X$ is order generating.

Proof:
We will prove that:
:$\forall x, y \in S: \paren {y \npreceq x \implies \exists p \in X: x \preceq p \land y \npreceq p}$
Let $x, y \in S$ such that:
:$y \npreceq x$
By Not Preceding implies There Exists Meet Irreducible Element Not Preceding:
:$\exists p \in S: p$ is meet irreducible and $x \preceq p$ and $y \npreceq p$
By definition of greatest element:
:$p \ne \top$ and $p \in \map {\mathit {IRR} } L$
By definitions of difference and singleton:
:$p \in X$
Thus
:$\exists p \in X: x \preceq p \land y \npreceq p$
{{qed|lemma}}
Hence by Order Generating iff Not Preceding implies There Exists Element Preceding and Not Preceding:
:$X$ is order generating.
{{qed}}
Theorem: Superset of Order Generating is Order Generating

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $X, Y$ be subsets of $S$ such that
:$X$ is order generating
and
:$X \subseteq Y$
Then $Y$ is order generating.

Proof:
Let $x \in S$.
Thus by definition of complete lattice:
:$x^\succeq \cap Y$ admits an infimum.
By definition of complete lattice:
:$x^\succeq$ admits an infimum
and
:$x^\succeq \cap X$ admits an infimum.
By Intersection is Subset:
:$x^\succeq \cap Y \subseteq x^\succeq$
By Infimum of Subset:
:$\map \inf {x^\succeq} \preceq \map \inf {x^\succeq \cap Y}$
By Infimum of Upper Closure of Element:
:$x \preceq \map \inf {x^\succeq \cap Y}$
By Set Intersection Preserves Subsets/Corollary:
:$x^\succeq \cap X \subseteq x^\succeq \cap Y$
By Infimum of Subset:
:$\map \inf {x^\succeq \cap Y} \preceq \map \inf {x^\succeq \cap X}$
By definition of order generating:
:$\map \inf {x^\succeq \cap Y} \preceq  x$
Thus by definition of antisymmetry:
:$x = \map \inf {x^\succeq \cap Y}$
{{qed}}