avewright/proofwiki-math huggingface dataset:
Theorem: Double of Antiperiod is Period

Let $f: \R \to \R$ be a real antiperiodic function with an anti-period of $A$.
Then $f$ is also periodic with a period of $2A$.

Proof:
Let $L_f$ be the set of all periodic elements of $f$.
By Periodic Element is Multiple of Antiperiod and Absolute Value of Real Number is not less than Divisors:
:$\forall p \in L_f: A \divides p \land A \le p$
Suppose there is a $p \in L_f$ such that $p = A$. 
Then: 
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \map f {x + A}
      | c = 
}}
{{eqn | r = -\map f x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f x
      | r = 0
      | c = 
}}
{{end-eqn}}
which contradicts Constant Function has no Period.
Therefore $\forall p \in L_f: A \divides p \land A < p$.
The smallest number $r$ such that $A < r \land A \divides r$ is $2A$.
But by Double of Antiperiodic Element is Periodic, this is a periodic element of $f$.
Hence the result.
{{qed}}
Category:Antiperiodic Functions
pxadvxwzz1zmlusjb4y16ki1i7b7gg3
Theorem: Principal Ideal in Integral Domain generated by Power Plus One is Subset of Principal Ideal generated by Power

Let $\struct {D, +, \circ}$ be an integral domain whose unity is $1_D$.
Let $a \in D$ be a proper element of $D$.
Then:
:$\forall n \in \Z_{\ge 0}: \ideal {a^{n + 1} } \subsetneq \ideal {a_n}$
where $\ideal x$ denotes the principal ideal of $D$ generated by $x$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \ideal {a^{n + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in D
      | l = x
      | r = r \circ a^{n + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \paren {r \circ a} \circ a^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \in
      | r = \ideal {a^n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \ideal {a^{n + 1} }
      | o = \subseteq
      | r = \ideal {a^n}
      | c = 
}}
{{end-eqn}}
It remains to be shown that $\ideal {a^{n + 1} } \ne \ideal {a^n}$.
{{AimForCont}} $\ideal {a^{n + 1} } = \ideal {a^n}$.
Then:
{{begin-eqn}}
{{eqn | l = \ideal {a^{n + 1} }
      | r = \ideal {a^n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a^n
      | o = \in
      | r = \ideal {a^{n + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists x \in D
      | l = a^n
      | r = x \circ a^{n + 1} 
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1_D
      | r = x \circ a 
      | c = Cancellation Law for Ring Product of Integral Domain
}}
{{end-eqn}}
That is, $a$ is a unit of $D$.
This contradicts the assertion that $a$ is a proper element of $D$.
The result follows by Proof by Contradiction.
{{qed}}
Theorem: Non-Field Integral Domain has Infinite Number of Ideals

Let $\struct {D, +, \circ}$ be an integral domain which is not a field.
Then $\struct {D, +, \circ}$ has an infinite number of distinct ideals.

Proof:
Let $a \in D$ be a proper element of $D$.
Because $\struct {D, +, \circ}$ is not a field, such an element is known to exist.
From Principal Ideal in Integral Domain generated by Power Plus One is Subset of Principal Ideal generated by Power:
:$\forall n \in \Z_{\ge 0}: \ideal {a^{n + 1} } \subsetneq \ideal {a_n}$
where $\ideal x$ denotes the principal ideal of $D$ generated by $x$.
Hence the set:
:$S = \set {\ideal {1_D}, \ideal a, \ideal {a^2}, \ideal {a^3}, \dotsc}$
is infinite.
{{qed}}
Theorem: Ring Homomorphism from Ring with Unity to Integral Domain Preserves Unity

Let $\struct {R, +_R, \circ_R}$ be a ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $\struct {D, +_D, \circ_D}$ be an integral domain whose zero is $0_D$ and whose unity is $1_D$.
Let $\phi: R \to D$ be a ring homomorphism such that:
:$\map \ker \phi \ne R$
where $\map \ker \phi$ denotes the kernel of $\phi$.
Then $\map \phi {1_R} = 1_D$.

Proof:
{{AimForCont}} $\map \phi {1_R} = 0_D$.
Let $x \in R$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi x
      | r = \map \phi {x \circ_R 1_R}
      | c = {{Defof|Unity of Ring}}
}}
{{eqn | r = \map \phi x \circ_D \map \phi {1_R}
      | c = {{Defof|Ring Homomorphism}}
}}
{{eqn | r = \map \phi x \circ_D 0_D
      | c = by hypothesis
}}
{{eqn | r = 0_D
      | c = {{Defof|Ring Zero}}
}}
{{end-eqn}}
But this contradicts the assertion that $\map \ker \phi \ne R$.
It follows that $\map \phi {1_R} \ne 0_D$.
Then we have:
{{begin-eqn}}
{{eqn | l = 1_D \circ_D \map \phi {1_R}
      | r = \map \phi {1_R}
      | c = {{Defof|Unity of Ring}}
}}
{{eqn | r = \map \phi {1_R \circ_R 1_R}
      | c = {{Defof|Unity of Ring}}
}}
{{eqn | r = \map \phi {1_R} \circ_D \map \phi {1_R}
      | c = {{Defof|Ring Homomorphism}}
}}
{{eqn | ll= \leadsto
      | l = 1_D
      | r = \map \phi {1_R}
      | c = Cancellation Law for Ring Product of Integral Domain
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Unity plus Negative of Nilpotent Ring Element is Unit

Let $\struct {R, +, \circ}$ be a ring with unity whose zero is $0_R$ and whose unity is $1_R$.
Let $x \in R$ be nilpotent.
Then $1_R - x$ is a unit of $R$.

Proof:
By definition of nilpotent element:
:$x^n = 0_R$
for some $n \in \Z_{>0}$.
From Difference of Two Powers:
{{begin-eqn}}
{{eqn | l = a^n - b^n
      | r = \paren {a - b} \circ \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} \circ b^j
      | c = 
}}
{{eqn | r = \paren {a - b} \circ \paren {a^{n - 1} + a^{n - 2} \circ b + a^{n - 3} \circ b^2 + \dotsb + a \circ b^{n - 2} + b^{n - 1} }
      | c = 
}}
{{end-eqn}}
for $a, b \in R$.
Putting $a = 1_R$ and $b = x$, we have:
{{begin-eqn}}
{{eqn | l = \paren {1_R}^n - x^n
      | r = \paren {1_R - x} \circ \paren {1_R^{n - 1} + 1_R^{n - 2} \circ x + 1_R^{n - 3} \circ x^2 + \dotsb + 1_R \circ x^{n - 2} + x^{n - 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1_R - 0_R
      | r = \paren {1_R - x} \circ \paren {1_R + 1_R \circ x + 1_R \circ x^2 + \dotsb + 1_R \circ x^{n - 2} + x^{n - 1} }
      | c = as $x^n = 0_R$, $1_R^k = 1_R$
}}
{{eqn | ll= \leadsto
      | l = 1_R
      | r = \paren {1_R - x} \circ \paren {1_R + x + x^2 + \dotsb + x^{n - 2} + x^{n - 1} }
      | c = 
}}
{{end-eqn}}
Thus by definition $1_R - x$ has a product inverse $1_R + x + x^2 + \dotsb + x^{n - 2} + x^{n - 1}$.
Hence by definition $1_R - x$ is a unit of $R$.
{{qed}}
Theorem: Quotient of Commutative Ring by Nilradical is Reduced

Let $\struct {R, +, \circ}$ be a commutative ring whose zero is $0_R$ and whose unity is $1_R$.
Let $\struct {N, +, \circ}$ denote the nilradical of $R$.
The quotient ring $R / N$ is a reduced ring.

Proof:
From Nilpotent Elements of Commutative Ring form Ideal, $\struct {N, +, \circ}$ is an ideal of $\struct {R, +, \circ}$.
Hence the quotient ring $R / N$ is defined.
By definition of the ideal of $\struct {R, +, \circ}$, $N$ is the zero of $R / N$.
Let $\paren {x + N}^n \in N$.
Then:
:$x^n \in N$
and so:
:$\paren {x^n}^m = 0_R$
for some $m \in \Z_{>0}$.
Hence:
:$x \in N$
and so:
:$x + N = N$
That is, if a (left) coset of $N$ is nilpotent in $R / N$ that (left) coset is $N$ itself.
The result follows.
{{qed}}
Theorem: Self-Inverse Element of Integral Domain is Unity or its Negative

Let $\struct {D, +, \circ}$ be an integral domain whose zero is $0_D$ and whose unity is $1_D$.
Let $x \in D$ such that $x^2 = 1_D$.
Then either $x = 1_D$ or $x = -1_D$.

Proof:
{{begin-eqn}}
{{eqn | l = x^2
      | r = 1_D
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x + 1_D} \paren {x + \paren {-1_D} }
      | r = 0_D
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x + 1_D
      | r = 0_D
      | c = 
}}
{{eqn | lo= \lor
      | l = x + \paren {-1_D}
      | r = 0_D
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = -1_D
      | c = 
}}
{{eqn | lo= \lor
      | l = x
      | r = 1_D
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Product of Units of Integral Domain with Finite Number of Units

Let $\struct {D, +, \circ}$ be an integral domain whose zero is $0_D$ and whose unity is $1_D$.
Let $D$ have a finite number of units.
Let $U_D$ be the set of units of $\struct {D, +, \circ}$.
Then:
:$\ds \prod_{x \mathop \in U_D} x = -1_D$

Proof:
Consider the set $S$ defined as:
:$S = U_R \setminus \set {1_D, -1_D}$
If $S$ has even cardinality, it can be partitioned into doubletons of the form $\set {u, u^{-1} }$.
Each of these doubletons has a product of $1_D$.
The product of all these with $1_D$ and $-1_D$ is $-1_D$.
It remains to be shown that $S$ cannot be of odd cardinality.
{{AimForCont}} $S$ has an odd number of elements.
Then after pairing off each $u \in D$ with its product inverse $u^{-1}$, we are left with one element of $S$ which is self-inverse.
But from Self-Inverse Element of Integral Domain is Unity or its Negative, this self-inverse element is either $1_D$ or $-1_D$.
These have already been counted.
Hence there cannot be an odd number of elements of $S$.
{{qed}}
Theorem: Prime Ideals of Ring of Integers

Let $\struct {\Z, +, \times}$ denote the ring of integers.
Let $J$ be a prime ideal of $\Z$.
Then either:
:$J = \set 0$
or:
:$J = \ideal p$
where:
:$p$ is a prime number
:$\ideal p$ denotes the principal ideal of $\Z$ generated by $p$.

Proof:
From Prime Ideal iff Quotient Ring is Integral Domain:
:$J$ is a prime ideal of $\Z$ {{iff}} $\Z / J$ is an integral domain.
From Quotient Ring of Integers and Zero:
:$\Z / \set 0 \cong \Z$
As $\Z$ is an integral domain, it follows that $\set 0$ is a prime ideal of $\Z$.
From Quotient Ring of Integers with Principal Ideal:
:$\struct {\Z, +, \times} / \ideal p$ is isomorphic to $\struct {\Z_p, +_p, \times_p}$, the ring of integers modulo $p$.
From Ring of Integers Modulo Prime is Integral Domain:
:$\struct {\Z_n, +_n, \times_p}$ is an integral domain {{iff}} $p$ is prime.
The result follows.
{{qed}}
Theorem: Prime Power Mapping on Galois Field is Automorphism

Let $\GF$ be a Galois field whose zero is $0_\GF$ and whose characteristic is $p$.
Let $\sigma: \GF \to \GF$ be defined as:
:$\forall x \in \GF: \map \sigma x = x^p$
Then $\sigma$ is an automorphism of $\GF$.

Proof:
Let $x, y \in \GF$.
Then:
{{begin-eqn}}
{{eqn | l = \map \sigma {x y}
      | r = \paren {x y}^p
      | c = Definition of $\sigma$
}}
{{eqn | r = x^p y^p
      | c = Power of Product of Commutative Elements in Group
}}
{{eqn | r = \map \sigma x \map \sigma y
      | c = Definition of $\sigma$
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map \sigma {x + y}
      | r = \paren {x + y}^p
      | c = Definition of $\sigma$
}}
{{eqn | r = \sum_{k \mathop = 0}^p \dbinom p k x^k y^{p - k}
      | c = Binomial Theorem
}}
{{eqn | o = \equiv
      | r = x^p + y^p
      | rr= \pmod p
      | c = Power of Sum Modulo Prime
}}
{{eqn | r = \map \sigma x + \map \sigma y
      | c = Definition of $\sigma$
}}
{{end-eqn}}
Thus it has been demonstrated that $\sigma$ is a homomorphism.
Then we have:
{{begin-eqn}}
{{eqn | l = \map \ker \sigma
      | r = \set {x \in \GF: \map \sigma x = 0_\GF}
      | c = {{Defof|Kernel of Ring Homomorphism}}
}}
{{eqn | r = \set {x \in \GF: x^p = 0_\GF}
      | c = Definition of $\sigma$
}}
{{eqn | r = \set {x \in \GF: x = 0_\GF}
      | c = Congruence of Powers
}}
{{eqn | r = \set {0_\GF}
      | c = Congruence of Powers
}}
{{end-eqn}}
From Kernel is Trivial iff Monomorphism, $\sigma$ is a monomorphism.
That is, $\sigma$ is an injection.
Then from Injection from Finite Set to Itself is Surjection, $\sigma$ is a surjection.
Thus $\sigma$ is a bijective homomorphism to itself.
The result follows by definition of automorphism.
{{qed}}
Theorem: Additive Group and Multiplicative Group of Field are not Isomorphic

Let $\struct {F, +, \times}$ be a field whose zero is $0_F$ and whose unity is $1_F$.
Let $\struct {F, +}$ denote the additive group of $F$.
Let $\struct {F_{\ne 0_F}, \times}$ denote the multiplicative group of $F$.
Then $\struct {F, +}$ and $\struct {F_{\ne 0_F}, \times}$ are not isomorphic to each other.

Proof:
{{AimForCont}} $\phi: \struct {F_{\ne 0_F}, \times} \to \struct {F, +}$ is an isomorphism.
By definition:
:$0_F$ is the identity of $\struct {F, +}$
and
:$1_F$ is the identity of $\struct {F_{\ne 0_F}, \times}$.
We have that:
{{begin-eqn}}
{{eqn | l = 0_F
      | r = \map \phi {1_F}
      | c = Epimorphism Preserves Identity
}}
{{eqn | r = \map \phi {\paren {-1_F} \times \paren {-1_F} }
      | c = 
}}
{{eqn | r = \map \phi {-1_F} + \map \phi {-1_F}
      | c = {{Defof|Group Isomorphism}}
}}
{{end-eqn}}
and so by definition $F$ has characteristic $2$.
Let $x \in \struct {F_{\ne 0_F}, \times}$.
Then:
{{begin-eqn}}
{{eqn | l = \map \phi {x^2}
      | r = \map \phi x + \map \phi x
      | c = {{Defof|Group Isomorphism}}
}}
{{eqn | r = 0_F
      | c = as $F$ has characteristic $2$
}}
{{end-eqn}}
As $\phi$ is an isomorphism, it is also a monomorphism.
From Kernel is Trivial iff Monomorphism:
:$\map \ker \phi = \set {1_F}$
and so $x^2 = 1$.
Thus $x = 1$ and so $\order F = 2$.
Thus $\order {F_{\ne 0_F} } = 1$.
So $\phi$ is a bijection from a set of cardinality $1$ to a set of cardinality $2$.
So $\phi$ cannot be a bijection and so cannot be an isomorphism.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: First Central Moment is Zero

Let $X$ be a random variable on some probability space with mean $\mu$. 
Then the first central moment $\mu_1$ of $X$ is equal to $0$.

Proof:
{{begin-eqn}}
{{eqn | l = \mu_1
      | r = \expect {X - \mu}
      | c = {{Defof|Central Moment}}
}}
{{eqn | r = \expect X - \mu
      | c = Expectation is Linear
}}
{{eqn | r = \mu - \mu
      | c = $\expect X = \mu$
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Category:Expectation
9gwdh5c494qd88bkn754udl1c7f0djq
Theorem: Principal Ideal Domain cannot have Infinite Strictly Increasing Sequence of Ideals

Let $\struct {D, +, \circ}$ be a principal ideal domain.
Then $D$ cannot have an infinite sequence of ideals $\sequence {j_n}_{n \mathop \in \N}$ such that:
:$\forall n \in \N: J_n \subsetneq j_{n + 1}$

Proof:
Let $K = \ds \bigcup_{n \mathop \in \N} J_n$.
Then from Increasing Union of Sequence of Ideals is Ideal, $K$ is an ideal of $D$.
We have that $D$ is a principal ideal domain.
Hence there exists $a \in D$ such that:
:$K = \ideal a$
where $\ideal a$ is the principal ideal of $D$ generated by $a$.
But $a \in J_m$ for some $m \in \N$.
Thus $K \subseteq J_m$
Thus it follows that $J_{m + 1} \subseteq J_m$ which contradicts our initial assertion that:
:$\forall n \in \N: J_n \subsetneq j_{n + 1}$
Hence the result.
{{qed}}
Theorem: Field Norm of Complex Number is Positive Definite

Let $\C$ denote the set of complex numbers.
Let $N: \C \to \R_{\ge 0}$ denote the field norm on complex numbers:
:$\forall z \in \C: \map N z = \cmod z^2$
where $\cmod z$ denotes the complex modulus of $z$.
Then $N$ is positive definite on $\C$.

Proof:
First it is shown that $\map N z = 0 \iff z = 0$.
{{begin-eqn}}
{{eqn | l = z
      | r = 0
      | c = 
}}
{{eqn | r = 0 + 0 i
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map N z
      | r = 0^2 + 0^2
      | c = Definition of $N$
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
Let $z = x + i y$.
{{begin-eqn}}
{{eqn | l = \map N z
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map N {x + i y}
      | r = 0
      | c = Definition of $z$
}}
{{eqn | ll= \leadsto
      | l = x^2 + y^2
      | r = 0
      | c = Definition of $N$
}}
{{eqn | ll= \leadsto
      | l = a
      | r = 0
      | c = Square of Real Number is Non-Negative
}}
{{eqn | l = b
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z
      | r = 0
      | c = Definition of $z$
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \map N z
      | r = \map N {x + i y}
      | c = Definition of $z$
}}
{{eqn | r = x^2 + y^2
      | c = Definition of $N$
}}
{{eqn | 0 = \ge
      | r = 0
      | c = Square of Real Number is Non-Negative
}}
{{end-eqn}}
Hence the result by definition of positive definite.
{{qed}}
Category:Field Norm of Complex Number
fgrcmu847s49n7be08imferkgspbgaq
Theorem: Second Standardized Moment is One

Let $X$ be a random variable on some probability space with standard deviation $\sigma$. 
Then the second standardized moment $\alpha_2$ of $X$ is equal to $1$.

Proof:
{{begin-eqn}}
{{eqn | l = \alpha_2
      | r = \frac {\mu_2} {\sigma^2}
      | c = {{Defof|Standardized Moment}}
}}
{{eqn | r = \frac {\sigma^2} {\sigma^2}
      | c = {{Defof|Central Moment}}
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Category:Expectation
dlu8n91xg9zxqqrmbrwvdx0oozdkyaq
Theorem: Field Norm of Complex Number is Multiplicative Function

Let $\C$ denote the set of complex numbers.
Let $N: \C \to \R_{\ge 0}$ denote the field norm on complex numbers:
:$\forall z \in \C: \map N z = \cmod z^2$
where $\cmod z$ denotes the complex modulus of $z$.
Then $N$ is a multiplicative function on $\C$.

Proof:
{{begin-eqn}}
{{eqn | l = \map N {z_1 z_2}
      | r = \cmod {z_1 z_2}^2
      | c = Definition of $N$
}}
{{eqn | r = \paren {\cmod {z_1} \cmod {z_2} }^2
      | c = Complex Modulus of Product of Complex Numbers
}}
{{eqn | r = \cmod {z_1}^2 \cmod {z_2}^2
      | c = 
}}
{{eqn | r = \map N {z_1} \map N {z_2}
      | c = Definition of $N$
}}
{{end-eqn}}
So $N$ is a multiplicative function by definition.
{{qed}}
Theorem: Field Norm of Complex Number is not Norm

Let $\C$ denote the set of complex numbers.
Let $N: \C \to \R_{\ge 0}$ denote the field norm on complex numbers:
:$\forall z \in \C: \map N z = \cmod z^2$
where $\cmod z$ denotes the complex modulus of $z$.
Then $N$ is not a norm on $\C$.

Proof:
Proof by Counterexample:
Let $z_1 = z_2 = 1$.
Then:
{{begin-eqn}}
{{eqn | l = \map N {z_1 + z_2}
      | r = \cmod {z_1 + z_2}^2
      | c = Definition of $N$
}}
{{eqn | r = 2^2
      | c = 
}}
{{eqn | r = 4
      | c = 
}}
{{end-eqn}}
But:
{{begin-eqn}}
{{eqn | l = \map N {z_1} + \map N {z_2}
      | r = \cmod {z_1}^2 + \cmod {z_2}^2
      | c = Definition of $N$
}}
{{eqn | r = 1^2 + 1^2
      | c = 
}}
{{eqn | r = 2
      | c = 
}}
{{end-eqn}}
So we have that for these instances of $z_1$ and $z_2$:
:$\map N {z_1 + z_2} > \map N {z_1} + \map N {z_2}$
and so the triangle inequality is not satisfied.
Hence by definition $N$ is not a norm on $\C$.
{{qed}}
Category:Field Norm of Complex Number
dofpceh1eri25d4elz5bhvmm0obtoo4
Theorem: Units of 5th Cyclotomic Ring

Let $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ denote the $5$th cyclotomic ring.
The units of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ are $1$ and $-1$.

Proof:
Let $\map N z$ denote the field norm of $z \in \Z \sqbrk {i \sqrt 5}$.
Let $z_1 \in \Z \sqbrk {i \sqrt 5}$ be a unit of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$.
Thus by definition:
:$\exists z_2 \in \Z \sqbrk {i \sqrt 5}: z_1 \times z_2 = 1$
Let $z_1 = x_1 + i y_1$ and $z_2 = x_2 + i y_2$.
Then:
{{begin-eqn}}
{{eqn | l = 1
      | r = \map N 1
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | r = \map N {z_1 \times z_2}
      | c = 
}}
{{eqn | r = \map N {z_1} \times \map N {z_2}
      | c = 
}}
{{eqn | r = \paren { {x_1}^2 + 5 {y_1}^2} \paren { {x_2}^2 + 5 {y_2}^2}
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | ll= \leadsto
      | l = {x_1}^2
      | r = 1
      | c = 
}}
{{eqn | lo= \land
      | l = {x_2}^2
      | r = 1
      | c = 
}}
{{eqn | lo= \land
      | l = y_1
      | r = y_2 = 0
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Field Norm on 5th Cyclotomic Ring

Let $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ denote the $5$th cyclotomic ring.
Let $\alpha = a + i b \sqrt 5$ be an arbitrary element of $\Z \sqbrk {i \sqrt 5}$.
The field norm of $\alpha$ is given by:
:$\map N \alpha = a^2 + 5 b^2$

Proof:
{{begin-eqn}}
{{eqn | l = \map N \alpha
      | r = \cmod \alpha^2
      | c = {{Defof|Field Norm of Complex Number}}
}}
{{eqn | r = \paren {\sqrt {a^2 + \paren {b \sqrt 5}^2} }^2
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = a^2 + 5 b^2
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: 5th Cyclotomic Ring has no Elements with Field Norm of 2 or 3

Let $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ denote the $5$th cyclotomic ring.
There are no elements of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ whose field norm is either $2$ or $3$.

Proof:
Let $\map N z$ denote the field norm of $z \in \Z \sqbrk {i \sqrt 5}$.
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = \map N z
      | r = 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2 + 5 y^2
      | r = 2
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | ll= \leadsto
      | l = x^2
      | r = 2
      | c = as $y$ is an integer and has to equal $0$
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \sqrt 2
      | c = 
}}
{{end-eqn}}
But Square Root of Prime is Irrational so $x \notin \Z$.
Similarly for $\map N z = 3$.
{{qed}}
Theorem: Irreducible Elements of 5th Cyclotomic Ring

Let $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ denote the $5$th cyclotomic ring.
The following elements of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ are irreducible:
:$2$
:$3$
:$1 + i \sqrt 5$
:$1 - i \sqrt 5$

Proof:
{{TheoremWanted|For the concept of irreducibility to be defined, it needs to be demonstrated that $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ is actually an integral domain.}}
Let $z = x + i y$ be an element of $\Z \sqbrk {i \sqrt 5}$ in the set $S$, where:
:$S := \set {2, 3, 1 + i \sqrt 5, 1 - i \sqrt 5}$
Let $z$ have a non-trivial factorization:
:$z = z_1 z_2$
where neither $z_1$ nor $z_2$ are units of $\Z \sqbrk {i \sqrt 5}$.
Let $\map N z$ denote the field norm of $z \in \Z \sqbrk {i \sqrt 5}$.
Then:
{{begin-eqn}}
{{eqn | l = \map N z
      | r = \map N {z_1 z_2}
      | c = 
}}
{{eqn | r = \map N {z_1} \map N {z_2}
      | c = {{Defof|Field Norm of Complex Number}}
}}
{{end-eqn}}
Then we have:
{{begin-eqn}}
{{eqn | l = \map N 2
      | r = 2^2 + 5 \times 0^2
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | r = 4
      | c = 
}}
{{eqn | l = \map N 3
      | r = 3^2 + 5 \times 0^2
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | r = 9
      | c = 
}}
{{eqn | l = \map N {1 + i \sqrt 5}
      | r = 1^2 + 5 \times 1^2
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | r = 6
      | c = 
}}
{{eqn | l = \map N {1 - i \sqrt 5}
      | r = 1^2 + 5 \times 1^2
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | r = 6
      | c = 
}}
{{end-eqn}}
From Elements of 5th Cyclotomic Ring with Field Norm 1, the only elements of $\Z \sqbrk {i \sqrt 5}$ whose field norm is $1$ are the units of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$: $1$ and $-1$.
From 5th Cyclotomic Ring has no Elements with Field Norm of 2 or 3, none of $4$, $6$ and $9$ have proper divisors which are field norms of elements of $\Z \sqbrk {i \sqrt 5}$.
Thus either $z_1$ or $z_2$ is a unit of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$.
So none of the elements of $S$ has a non-trivial factorization in $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$.
Hence the result, by definition of irreducible.
{{qed}}
Theorem: Value of Field Norm on 5th Cyclotomic Ring is Integer

Let $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ denote the $5$th cyclotomic ring.
Let $\alpha = a + i b \sqrt 5$ be an arbitrary element of $\Z \sqbrk {i \sqrt 5}$.
Let $\map N \alpha$ denoted the field norm of $\alpha$.
Then $\map N \alpha$ is an integer.

Proof:
From Field Norm on 5th Cyclotomic Ring:
:$\map N \alpha = a^2 + 5 b^2$
From the definition of the $5$th cyclotomic ring:
:$\Z \sqbrk {i \sqrt 5} = \set {a + i \sqrt 5 b: a, b \in \Z}$
That is, both $a$ and $b$ are integers.
Hence $a^2 + 5 b^2$ is also an integer.
{{Qed}}
Theorem: Elements of 5th Cyclotomic Ring with Field Norm 1

Let $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ denote the $5$th cyclotomic ring.
The only elements of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ whose field norm equals $1$ are the units of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$: $1$ and $-1$.

Proof:
From Units of 5th Cyclotomic Ring, $1$ and $-1$ are the only units of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$.
Let $\map N z$ denote the field norm of $z \in \Z \sqbrk {i \sqrt 5}$.
Let $z \in \Z \sqbrk {i \sqrt 5}$ such that $\map N z = 1$.
Let $z = x + i y$.
Then:
{{begin-eqn}}
{{eqn | l = \map N z
      | r = 1
      | c = Field Norm on 5th Cyclotomic Ring
}}
{{eqn | ll= \leadsto
      | l = x^2 + 5 y^2
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2
      | r = 1
      | c = 
}}
{{eqn | lo= \land
      | l = y
      | r = 0
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}