avewright/proofwiki-math huggingface dataset:
Theorem: 5th Cyclotomic Ring is not a Unique Factorization Domain

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

Proof:
By definition, a unique factorization domain $D$ is an integral domain with the properties that:
:For all $x \in D$ such that $x$ is non-zero and not a unit of $D$:
::$(1): \quad x$ possesses a complete factorization in $D$
::$(2): \quad$ Any two complete factorizations of $x$ are equivalent.
A complete factorization is a tidy factorization 
:$x = u \circ y_1 \circ y_2 \circ \cdots \circ y_n$
such that:
:$u$ is a unit of $D$
:all of $y_1, y_2, \ldots, y_n$ are irreducible.
{{TheoremWanted|It needs to be demonstrated that $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ is actually an integral domain.}}
From Units of 5th Cyclotomic Ring, the only units of $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ are $1$ and $-1$.
From Irreducible Elements of 5th Cyclotomic Ring, all of the elements of the set $S$, where:
:$S := \set {2, 3, 1 + i \sqrt 5, 1 - i \sqrt 5}$
are irreducible in $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$
Then we have:
{{begin-eqn}}
{{eqn | l = 6
      | r = 1 \times 2 \times 3
      | c = 
}}
{{eqn | r = 1 \times \paren {1 + i \sqrt 5} \paren {1 - i \sqrt 5} 
      | c = 
}}
{{end-eqn}}
So there are two tidy factorizations of $6$ in $\struct {\Z \sqbrk {i \sqrt 5}, +, \times}$ which are not equivalent.
Hence the result.
{{qed}}
Theorem: Quotient of Ring of Polynomials in Ring Element on Integral Domain by that Polynomial is that Domain

Let $\struct {D, +, \times}$ be an integral domain.
Let $X \in R$ be transcencental over $D$.
Let $D \sqbrk X$ be the ring of polynomials in $X$ over $D$.
Let $D \sqbrk X / \ideal X$ denote the quotient ring of $D \sqbrk X$ by the ideal of $D$ generated by $X$.
Then:
:$D \sqbrk X / \ideal X \cong D$

Proof:
Let $n \in \Z_{> 0}$ be arbitrary.
Let $P = a_n X^n + a_{n - 1} X^{n - 1} + \dotsb + a_1 X + a_0$ be a polynomial over $D$ in $X$.
Consider the mapping $\phi: D \sqbrk X \to D$ defined as:
:$\forall P \in D \sqbrk X: \map \phi P = a_0$
Let:
:$P_1 = a_m X^m + a_{m - 1} X^{m - 1} + \dotsb + a_1 X + a_0$
:$P_2 = b_m X^m + b_{m - 1} X^{m - 1} + \dotsb + b_1 X + b_0$
We have that:
{{begin-eqn}}
{{eqn | l = \map \phi {P_1 \times P_2}
      | r = a_0 \times b_0
      | c = 
}}
{{eqn | r = \map \phi {P_1} \times \map \phi {P_2}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \map \phi {P_1 + P_2}
      | r = a_0 + b_0
      | c = 
}}
{{eqn | r = \map \phi {P_1} + \map \phi {P_2}
      | c = 
}}
{{end-eqn}}
Thus it is seen that $\phi$ is a homomorphism.
The First Ring Isomorphism Theorem can then be used.
{{finish}}
Theorem: Polynomials in Integers with Even Constant Term forms Ideal

Let $\Z \sqbrk X$ be the ring of polynomials in $X$ over $\Z$.
Let $S \subseteq \Z \sqbrk X$ be the set of polynomials over $\Z$ in $X$ which have a constant term which is even.
Then $S$ is an ideal of $\Z \sqbrk X$.

Proof:
For example, $X + 2$ is a polynomials over $\Z$ in $X$ with an even constant term.
So $S$ is not empty.
Let $P_1 = \ds \sum_{k \mathop = 0}^n a_k X^k$ and $P_2 = \ds \sum_{k \mathop = 0}^n b_k X^k$ be elements of $S$.
We have:
{{begin-eqn}}
{{eqn | l = P_1 - P_2
      | r = \sum_{k \mathop = 0}^n a_k X^k + \sum_{k \mathop = 0}^n b_k X^k
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 0}^{\max \set {m, n} } \paren {a_k - b_k} X^k
      | c = 
}}
{{end-eqn}}
The constant term of $P_1 - P_2$ is $a_0 - b_0$ which is even.
Thus $P_1 - P_2 \in S$.
Let $P_3 = \sum_{k \mathop = 0}^s c_k X^k \in \Z \sqbrk X$.
Then the constant term of $P_3 \times P_1$ is $c_0 \times a_0$.
As $a_0$ is even, so is $c_0 \times a_0$.
The result follows by Test for Ideal.
{{qed}}
Theorem: Polynomials in Integers is not Principal Ideal Domain

Let $\Z \sqbrk X$ be the ring of polynomials in $X$ over $\Z$.
Then $\Z \sqbrk X$ is not a principal ideal domain.

Proof:
Let $J$ be the ideal formed from the set of polynomials over $\Z$ in $X$ which have a constant term which is even.
From Polynomials in Integers with Even Constant Term forms Ideal, $J$ is indeed an ideal.
{{AimForCont}} $J$ is a principal ideal of $\Z \sqbrk X$ such that $J = \ideal f$.
But $2 \in J$, and so $2$ is a multiple of $f$ in $\Z \sqbrk X$.
So $f = \pm 2$ or $f = \pm 1$.
But this contradicts the fact that $J = \ideal f$.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Polynomials in Integers is Unique Factorization Domain

Let $\Z \sqbrk X$ be the ring of polynomials in $X$ over $\Z$.
Then $\Z \sqbrk X$ is a unique factorization domain.

Proof:
We have that Integers form Unique Factorization Domain.
The result follows from Gauss's Lemma on Unique Factorization Domains.
{{qed}}
Theorem: Ideal of Ring of Polynomials over Field has Unique Monic Polynomial forming Principal Ideal

Let $F$ be a field.
Let $F \sqbrk X$ be the ring of polynomials in $X$ over $F$.
Let $J$ be a non-null ideal of $F \sqbrk X$.
Then there exists exactly one monic polynomial $f \in F \sqbrk X$ such that:
:$J = \ideal f$
where $\ideal f$ is the principal ideal generated by $f$ in $F \sqbrk X$.

Proof:
{{MissingLinks}}
{{Proofread}}
Theorem: Gaussian Integers form Principal Ideal Domain

The ring of Gaussian integers:
:$\struct {\Z \sqbrk i, +, \times}$
forms a principal ideal domain.

Proof:
Follows immediately from:
:Gaussian Integers form Euclidean Domain
:Euclidean Domain is Principal Ideal Domain.
{{qed}}
Theorem: Polynomial X^2 + 1 is Irreducible in Ring of Real Polynomials

Let $\R \sqbrk X$ be the ring of polynomials in $X$ over the real numbers $\R$.
Then the polynomial $X^2 + 1$ is an irreducible element of $\R \sqbrk X$.

Proof:
{{AimForCont}} $x^2 + 1$ has a non-trivial factorization in $\R \sqbrk X$.
Then:
:$\exists \alpha, \beta \in \R: \paren {X - \alpha} \paren {X - \beta}$
and from the Polynomial Factor Theorem:
:$\alpha^2 + 1 = 0$
But that means:
:$\alpha^2 = -1$
and such an $\alpha$ does not exist in $\R$.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Matrix Multiplication is not Commutative

Let $R$ be a ring with unity.
Let $n \in \Z_{>0}$ be a (strictly) positive integer such that $n \ne 1$.
Let $\map {\MM_R} n$ denote the $n \times n$ matrix space over $R$.
Then (conventional) matrix multiplication over $\map {\MM_R} n$ is not commutative:
:$\exists \mathbf A, \mathbf B \in \map {\MM_R} n: \mathbf {A B} \ne \mathbf {B A}$
If $R$ is specifically not commutative, then the result holds when $n = 1$ as well.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:$\exists \mathbf A, \mathbf B \in \map {\MM_R} n: \mathbf {A B} \ne \mathbf {B A}$
Theorem: Matrix Multiplication on Square Matrices over Trivial Ring is Commutative

Let $\struct {R, +, \circ}$ be the trivial ring over an underlying set.
Let $\map {\MM_R} n$ denote the $n \times n$ matrix space over $R$.
Then (conventional) matrix multiplication is commutative over $\map {\MM_R} n$:
:$\forall \mathbf A, \mathbf B \in \map {\MM_R} n: \mathbf {A B} = \mathbf {B A}$

Proof:
Let $\mathbf A = \sqbrk a_n$ and $\mathbf B = \sqbrk b_n$ be order $n$ square matrices over $R$.
By definition of matrix multiplication, $\mathbf A \mathbf B = \mathbf C = \sqbrk c_n$ where:
:$\ds \forall i \in \closedint 1 n, j \in \closedint 1 n: c_{i j} = \sum_{k \mathop = 1}^n a_{i k} \circ b_{k j}$
But by definition of the trivial ring:
:$\forall a, b \in R: a \circ b = 0_R$
where $0_R$ is the zero of $R$.
Thus $\mathbf A \mathbf B$ is the zero $n \times n$ matrix.
The same applies to $\mathbf B \mathbf A$, which is also the zero $n \times n$ matrix.
That is:
:$\mathbf A \mathbf B = \mathbf B \mathbf A = \bszero_n$
and the result follows by definition of commutative operation.
{{qed}}
Category:Conventional Matrix Multiplication
Category:Trivial Rings
83bu7wme7j53wphq53g50xm8cq4ftjc
Theorem: Ring Subtraction equals Zero iff Elements are Equal

Let $\struct {R, +, \circ}$ be a ring whose zero is $0_R$
Then:
:$\forall a, b \in R: a - b = 0_R \iff a = b$
where $a - b$ denotes ring subtraction.

Proof:
{{begin-eqn}}
{{eqn | l = a - b
      | r = 0_R
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a + \paren {-b}
      | r = 0_R
      | c = {{Defof|Ring Subtraction}}
}}
{{eqn | ll= \leadstoandfrom
      | l = \paren {a + \paren {-b} } + b
      | r = 0_R + b
      | c = Cancellation Laws
}}
{{eqn | ll= \leadstoandfrom
      | l = a + \paren {b^{-1} + b}
      | r = 0_R \circ b
      | c = {{Group-axiom|1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = a
      | r = b
      | c = {{Group-axiom|2}} and {{Group-axiom|3}}
}}
{{end-eqn}}
{{qed}}
Theorem: Preordering of Products under Operation Compatible with Preordering

Let $\struct {S, \circ}$ be an algebraic structure.
Let $\precsim$ be a preordering on $S$.
Then $\precsim$ is compatible with $\circ$ {{iff}}:
:$\forall x_1, x_2, y_1, y_2 \in S: x_1 \precsim x_2 \land y_1 \precsim y_2 \implies \paren {x_1 \circ y_1} \precsim \paren {x_2 \circ y_2}$

Proof:
By definition, $\precsim$ is compatible with $\circ$ {{iff}}:
{{begin-eqn}}
{{eqn | q = \forall x, y, z \in S
      | l = x \precsim y
      | o = \implies
      | r = \paren {x \circ z} \precsim \paren {y \circ z}
}}
{{eqn | l = x \precsim y
      | o = \implies
      | r = \paren {z \circ x} \precsim \paren {z \circ y}
}}
{{end-eqn}}
Theorem: P-adic Norm not Complete on Rational Numbers/Proof 2/Lemma 1

:$\exists x \in \Z_{>0}:  p \nmid x, x \ge \dfrac {p + 1} 2$

Proof:
Let $x = p + 1$.
Then $p \nmid x$ and:
:$x = p + 1 > p > 0$
{{qed}}
Category:P-adic Norm not Complete on Rational Numbers
klt8vnjgaediwd7qt6bk8eururfgx8p
Theorem: P-adic Norm not Complete on Rational Numbers/Proof 2/Lemma 5

:$\ds \lim_{n \mathop \to \infty} {x_n}^k = a$ in $\struct {\Q, \norm {\,\cdot\,}_p}$

Proof:
By assumption:
:$\forall n \in \N: p^n \divides \paren { {x_n}^k - a}$
By the definition of the $p$-adic norm:
:$\forall n \in \N: \norm { {x_n}^k - a}_p \le \dfrac 1 {p^n}$
By Sequence of Powers of Number less than One:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 {p^n} = 0$
By Squeeze Theorem for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \norm { {x_n}^k - a}_p = 0$
By the definition of convergence in $\struct {\Q, \norm {\,\cdot\,}_p}$:
:$\ds \lim_{n \mathop \to \infty} {x_n}^k = a$
{{qed}}
Category:P-adic Norm not Complete on Rational Numbers
l8azvtyo3l16yc4d4yxxddz5ro6il5t
Theorem: Characterisation of Cauchy Sequence in Non-Archimedean Norm/Corollary 1

Let $\norm {\,\cdot\,}_p$ be the $p$-adic norm on the rationals $\Q$ for some prime $p$.
Let $\sequence {x_n}$ be a sequence of integers such that:
:$\forall n: x_{n + 1} \equiv x_n \pmod {p^n}$
Then:
:$\sequence {x_n}$ is a Cauchy sequence in $\struct {\Q, \norm {\,\cdot\,}_p}$.

Proof:
By hypothesis:
:$\forall n \in \N: p^n \divides \paren {x_{n + 1} - x_n}$
By the definition of the $p$-adic norm:
:$\forall n \in \N: \norm {x_{n + 1} - x_n}_p \le \dfrac 1 {p^n}$
From Sequence of Powers of Number less than One:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 {p^n} = 0$
From the Squeeze Theorem for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \norm{x_{n+1} - x_n}_p = 0$.
From P-adic Norm on Rational Numbers is Non-Archimedean Norm, the $p$-adic norm is  non-Archimedean.
From Characterisation of Cauchy Sequence in Non-Archimedean Norm:
:$\sequence {x_n}$ is a Cauchy sequence in $\struct {\Q, \norm {\,\cdot\,}_p}$.
{{qed}}
Category:Characterisation of Cauchy Sequence in Non-Archimedean Norm
kadszi663rvq9nre8w8m0pr3qv0w33b
Theorem: P-adic Norm not Complete on Rational Numbers/Proof 2/Lemma 2

:$a \in \Z_{> 0}: \nexists \,c \in \Z : c^k = a$

Proof:
Since $x, p > 0$ then $a > 0$.
{{AimForCont}} for some $c \in \Z:c^k = a$.
Since $c^k \in \Z$, by Nth Root of Integer is Integer or Irrational then:
:$c \in \Z$
Suppose $k$ is odd.
Since $a > 0$, by Odd Power Function is Strictly Increasing then $c > 0$
Hence $a = \size c^k$
On the other hand, suppose $k$ is even, that is $k = 2l$ for some $l \in Z_{> 0}$.
Then:
{{begin-eqn}}
{{eqn | l = a
      | r = c^{2l}
}}
{{eqn | r = \paren {c^2}^l
}}
{{eqn | r = \paren {\size c^2}^l
      | c = Equivalence of Definitions of Absolute Value Function
}}
{{eqn | r = \size c^{2l}
}}
{{eqn | r = \size c^k
}}
{{end-eqn}}
In either case $\size c \in \Z_{> 0}$ and $\size c^k = a$
Let $d = \size c$
By the definition of $a$ it follows that $d^k = x^k + p$
Hence:
{{begin-eqn}}
{{eqn | l = p 
      | r = d^k - x^k
}}
{{eqn | r = \paren {d - x} \paren {d^{k - 1} + d^{k - 2} x + d^{k - 3} x^2 + \dotsb + c x^{k - 2} + x^{k - 1} }
      | c = Difference of Two Powers
}}
{{end-eqn}}
Let $y = d^{k - 1} + d^{k - 2} x + d^{k - 3} x^2 + \dotsb + d x^{k - 2} + x^{k - 1}$
Since $d, x \in \Z_{> 0}$ then $d - x \in \Z$ and $y \in \Z$
So $d - x$ and $y$ are factors of $p$
The factors of $p$ by definition are:
:$\pm 1$ and $\pm p$
Since $d, x \in \Z_{> 0}$ then:
{{begin-eqn}}
{{eqn | l = d^{k - 1} + d^{k - 2} x + d^{k - 3} x^2 + \dotsb + d x^{k - 2} + x^{k - 1}
      | o = \ge 
      | r = d^{k - 1} + x^{k - 1}
}}
{{eqn | o = \ge 
      | r = d + x
}}
{{eqn | o = \ge 
      | r = 1 + 1
}}
{{eqn | o = \ge 
      | r = 2
}}
{{end-eqn}}
Hence $y = p$
Then:
{{begin-eqn}}
{{eqn | l = p 
      | r = d^{k - 1} + d^{k - 2} x + d^{k - 3} x^2 + \dotsb + d x^{k - 2} + x^{k - 1}
}}
{{eqn | o = \ge 
      | r = d^{k - 1} + x^{k - 1}
}}
{{eqn | o = \ge 
      | r = d + x
}}
{{end-eqn}}
It also follows that $d - x = 1$, that is, $d = x + 1$
Then
{{begin-eqn}}
{{eqn | l = d + x
      | r = \paren {x + 1} + x
}}
{{eqn | r = 2x + 1
}}
{{eqn | o = >
      | r = 2x
}}
{{eqn | o = >
      | r = p + 1
}}
{{eqn | o = >
      | r = p
}}
{{end-eqn}}
This contradicts the previous conclusion that $p \ge d + x$
So:
:$\nexists \,c \in \Z : c^k = a$
{{qed}}
Category:P-adic Norm not Complete on Rational Numbers
phaadqtr1ve7gbf201hybvqikj8ieqs
Theorem: P-adic Norm not Complete on Rational Numbers/Proof 2/Lemma 3

:$\map f {x_1} \equiv 0 \pmod p$

Proof:
{{begin-eqn}}
{{eqn | l = \map f {x_1}
      | r = x_1^k - \paren {x_1^k + p}
}}
{{eqn | r = \paren {x_1^k - x_1^k} - p
}}
{{eqn | r = -p
}}
{{eqn | o = \equiv
      | r = 0 \pmod p
}}
{{end-eqn}}
{{qed}}
Category:P-adic Norm not Complete on Rational Numbers
4y313yewjfwjz6avent2oo6zfqueega
Theorem: P-adic Norm not Complete on Rational Numbers/Proof 2/Lemma 4

:$\map {f'} {x_1} \not \equiv 0 \pmod p$

Proof:
By Euclid's Lemma for Prime Divisors:
:$p \nmid k x_1^{k - 1}$
Hence:
:$k x_1^{k - 1} \not \equiv 0 \mod p$
The formal derivative $\map {f'} X \in \Z \sqbrk X$ of $\map f X$ is by definition:
:$k X^{k - 1}$
Then:
:$\map {f'} {x_1} = k x_1^{k - 1} \not \equiv 0 \pmod p$
{{qed}}
Category:P-adic Norm not Complete on Rational Numbers
nvzcpl2u0gv7vtca4wdgk9kegsflq64
Theorem: Surjection from Natural Numbers iff Countable/Corollary 1

Let $T$ be a countably infinite set.
Let $S$ be a non-empty set.
Then $S$ is countable {{iff}} there exists a surjection $f: T \to S$.

Proof:
Let $g: T \to \N$ be a bijection from $T$ to $\N$.
By Inverse of Bijection is Bijection, $g^{-1}: \N \to T$ is a bijection from $\N$ to $T$.
Theorem: Surjection from Natural Numbers iff Countable/Corollary 2

Let $T$ be a countably infinite set.
Let $S$ be an uncountable set.
Let $f:T \to S$ be a mapping.
Then $f$ is not a surjection.

Proof:
By Corollary 1 no mapping from $T$ to $S$ is a surjection.
{{qed}}
Category:Countable Sets
Category:Surjections
220auysxelec96dq78xe8ymn2ex26jk
Theorem: P-adic Numbers are Uncountable

Let $p$ be any prime number.
The set of $p$-adic numbers $\Q_p$ is an uncountable set.

Proof:
Let $P$ be the set of sequences on $\set{i : i \in \N : 0 \le i < p}$.
That is:
:$P = \set{\sequence{d_n} : d_n \in \N : 0 \le d_n < p}$
From Cantor's Diagonal Argument:
:$P$ is an uncountable set
Let $f: P \to \Q_p$ be the mapping from $P$ to $\Z_p$ defined by:
:$\forall \sequence{d_n} \in P : \map f {\sequence{d_n}} = \ds \sum_{n = 0}^\infty d_n p^n$
where $Z_p$ denotes the $p$-adic integers and $\ds \sum_{n = 0}^\infty d_n p^n$ denotes a $p$-adic expansion
From P-adic Integer has Unique P-adic Expansion Representative:
:$f$ is bijective
Hence:
:$\Z_p$ is an uncountable set
Recall that $\Z_p \subseteq \Q_p$.
From Sufficient Conditions for Uncountability:
:$\Q_p$ is an uncountable set
{{qed}}
Theorem: Ordered Integral Domain is Totally Ordered Ring

Let $\struct {D, +, \times, \le}$ be an ordered integral domain.
Then $\struct {D, +, \times, \le}$ is a totally ordered ring.

Proof:
By definition, $\struct {D, +, \times, \le}$ is an integral domain endowed with a strict positivity property.
From Strict Positivity Property induces Total Ordering, the ordering $\le$ on $\struct {D, +, \times, \le}$ is a total ordering.
Hence the result by definition of totally ordered ring.
{{qed}}
Category:Ordered Integral Domains
Category:Totally Ordered Rings
aunzqytajll4lim3grktfz3nxvzq9dr
Theorem: Strict Negativity is equivalent to Strictly Preceding Zero

:$\map N a \iff a < 0$

Proof:
{{begin-eqn}}
{{eqn | l = \map N a
      | o = \leadstoandfrom
      | r = \map P {-a}
      | c = {{Defof|Strict Negativity Property}}
}}
{{eqn | o = \leadstoandfrom
      | r = \map P {-a + 0}
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = a < 0
      | c = Strict Positivity Property induces Total Ordering
}}
{{end-eqn}}
{{qed}}
Theorem: Strict Negativity is equivalent to Strict Positivity of Negative

:$\map P a \iff \map N {-a}$

Proof:
{{begin-eqn}}
{{eqn | l = \map P a
      | o = \leadstoandfrom
      | r = \map P {-\paren {-a} }
      | c = 
}}
{{eqn | o = \leadstoandfrom
      | r = \map N {-a}
      | c = {{Defof|Strict Negativity Property}}
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Strictly Negative Elements is Strictly Negative

:$\map N a, \map N b \implies \map N {a + b}$

Proof:
{{begin-eqn}}
{{eqn | l = \map N a, \map N b
      | o = \leadsto
      | r = \map P {-a}, \map P {-b}
      | c = {{Defof|Strict Negativity Property}}
}}
{{eqn | o = \leadsto
      | r = \map P {\paren {-a} + \paren {-b} }
      | c = Strict Positivity Property: $(P \, 1)$
}}
{{eqn | o = \leadsto
      | r = \map P {-\paren {a + b} }
      | c = 
}}
{{eqn | o = \leadsto
      | r = \map N {a + b}
      | c = {{Defof|Strict Negativity Property}}
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Two Strictly Negative Elements is Strictly Positive

:$\map N a, \map N b \implies \map P {a \times b}$

Proof:
{{begin-eqn}}
{{eqn | l = \map N a, \map N b
      | o = \leadsto
      | r = \map P {-a}, \map P {-b}
      | c = {{Defof|Strict Negativity Property}}
}}
{{eqn | o = \leadsto
      | r = \map P {\paren {-a} \times \paren {-b} }
      | c = Strict Positivity Property: $(P \, 2)$
}}
{{eqn | o = \leadsto
      | r = \map P {a \times b}
      | c = Product of Ring Negatives
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Strictly Negative Element with Strictly Positive Element is Strictly Negative

:$\map N a, \map P b \implies \map N {a \times b}$

Proof:
{{begin-eqn}}
{{eqn | l = \map N a, \map P b
      | o = \leadsto
      | r = \map P {-a}, \map P b
      | c = {{Defof|Strict Negativity Property}}
}}
{{eqn | o = \leadsto
      | r = \map P {\paren {-a} \times b}
      | c = Strict Positivity Property: $(P \, 2)$
}}
{{eqn | o = \leadsto
      | r = \map P {-\paren {a \times b} }
      | c = Product with Ring Negative
}}
{{eqn | o = \leadsto
      | r = \map N {a \times b}
      | c = {{Defof|Strict Negativity Property}}
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Well-Ordered Integral Domain

{{TFAE|def = Well-Ordered Integral Domain}}
Let $\struct {D, +, \times \le}$ be an ordered integral domain whose zero is $0_D$.

Proof:
=== $(1)$ implies $(2)$ ===
Let $\struct {D, +, \times \le}$ be a well-ordered integral domain by definition 1.
Then by definition the ordering $\le$ is a well-ordering on the set $P$ of (strictly) positive elements of $D$.
Let $S \subseteq P$.
Thus by definition of well-ordering, $S$ has a minimal element.
Thus $\struct {D, +, \times \le}$ is a well-ordered integral domain by definition 2.
{{qed|lemma}}
Theorem: Principle of Mathematical Induction/Zero-Based

Let $\map P n$ be a propositional function depending on $n \in \N$.
Suppose that:
:$(1): \quad \map P 0$ is true
:$(2): \quad \forall k \in \N: k \ge 0 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \N$.

Proof:
Consider $\N$ defined as a Peano structure.
The result follows from Principle of Mathematical Induction for Peano Structure.
{{qed}}
Theorem: Principle of Mathematical Induction/One-Based

Let $\map P n$ be a propositional function depending on $n \in \N_{>0}$.
Suppose that:
:$(1): \quad \map P 1$ is true
:$(2): \quad \forall k \in \N_{>0}: k \ge 1 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \N_{>0}$.

Proof:
Let $S$ be the set defined as:
:$S := \set {n \in \N_{>0}: \map P n \text { is false} }$
{{AimForCont}} $S \ne \O$.
From the Well-Ordering Principle it follows that $S$ has a minimal element $m$.
From $(1)$ we have that $\map P 1$ holds.
Hence $1 \notin S$.
Therefore $m \ne 1$.
Therefore $m - 1 \in \N_{>0}$.
But $m$ is the minimal element of $S$.
So $m - 1 \notin S$.
Therefore $\map P {m - 1}$ is true.
Hence by $(2)$ it follows that $\map P m$.
But then $m \notin S$.
This contradicts our supposition that $m \in S$.
Hence there can be no such $m \in S$.
So $S = \O$ and the result follows.
{{qed}}
Theorem: Principle of Mathematical Induction/One-Based

Let $\map P n$ be a propositional function depending on $n \in \N_{>0}$.
Suppose that:
:$(1): \quad \map P 1$ is true
:$(2): \quad \forall k \in \N_{>0}: k \ge 1 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \N_{>0}$.

Proof:
Let $M$ be the set of all $n \in \N_{>0}$ for which $\map P n$ holds.
By $(1)$ we have that $1 \in M$.
By $(2)$ we have that if $k \in M$ then $k + 1 \in M$.
From the Axiomatization of $1$-Based Natural Numbers, Axiom $(\text F)$, it follows that $M = \N_{>0}$.
{{qed}}
Theorem: Principle of Mathematical Induction/One-Based

Let $\map P n$ be a propositional function depending on $n \in \N_{>0}$.
Suppose that:
:$(1): \quad \map P 1$ is true
:$(2): \quad \forall k \in \N_{>0}: k \ge 1 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \N_{>0}$.

Proof:
We have that Natural Numbers are Non-Negative Integers.
Then we have that Integers form Well-Ordered Integral Domain.
The result follows from Induction on Well-Ordered Integral Domain.
{{qed}}
Theorem: Principle of Mathematical Induction/One-Based

Let $\map P n$ be a propositional function depending on $n \in \N_{>0}$.
Suppose that:
:$(1): \quad \map P 1$ is true
:$(2): \quad \forall k \in \N_{>0}: k \ge 1 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \N_{>0}$.

Proof:
For each $n \in \N_{>0}$, let $\map {P'} n$ be defined as:
:$\map {P'} n := \map P 1 \land \dots \land \map P n$
It suffices to show that $\map {P'} n$ is true for all $n \in \N_{>0}$.
It is immediate from the assumption $\map P 1$ that $\map {P'} 1$ is true.
Now suppose that $\map {P'} n$ holds.
By $(2)$, this implies that $\map P {n + 1}$ holds as well.
Consequently, $\map {P'} n \land \map P {n + 1} = \map {P'} {n + 1}$ holds.
Thus by the Principle of Mathematical Induction:
:$\map {P'} n$ holds for all $n \in \N_{>0}$
as desired.
{{Qed}}