Proof of Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing

Proof of (i). Let $m,n\in\mathbb{N}_{0}$ with $m\le n$ in $\mathbb{N}_{0}$, and let $j=n-m\in\mathbb{N}_{0}$ be the difference of The Difference of Two Natural Numbers with Zero (i), so that $m+j=n$. The images $m_{\mathbb{R}}$, $n_{\mathbb{R}}$ and $j_{\mathbb{R}}$ lie in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (v), $\mathbb{R}$ being an ordered field by The Real Numbers Form an Ordered Field in Which Every Nonempty Set Bounded Above Has a Supremum (i). By The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (ii), $n_{\mathbb{R}}=m_{\mathbb{R}}+j_{\mathbb{R}}$, and $0\le j_{\mathbb{R}}$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vi). As $m_{\mathbb{R}}\le m_{\mathbb{R}}$ by Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (viii), the order-compatibility of addition in the ordered ring $\mathbb{R}$, Rules of Order in an Ordered Ring: Differences, Sums, Negatives, Products and Squares (ii), gives $m_{\mathbb{R}}+0\le m_{\mathbb{R}}+j_{\mathbb{R}}$, where $m_{\mathbb{R}}+0=m_{\mathbb{R}}$ by Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (v). Hence $m_{\mathbb{R}}\le n_{\mathbb{R}}$, that is, $m\le n$ in $\mathbb{R}$.

Proof of (ii). Let $n\in\mathbb{N}$. Then $1\le n$ in $\mathbb{N}_{0}$ by Arithmetic and Order of the Natural Numbers (x), so $1_{\mathbb{R}}\le n_{\mathbb{R}}$ by (i), and $1_{\mathbb{R}}$ is the unit $1$ of $\mathbb{R}$ by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (i). So $1\le n$ in $\mathbb{R}$.

Proof of (iii). Let $k\in\mathbb{N}_{0}$. Then $k+1\in\mathbb{N}_{0}$, the addition being a binary operation on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv) and $1\in\mathbb{N}_{0}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (ii), and $k!$ and $(k+1)!$ lie in $\mathbb{N}_{0}$, as the values at $k$ and $k+1$ of the map $\mathbb{N}_{0}\to\mathbb{N}_{0}$, $n\mapsto n!$, of The Factorial as a Map on the Natural Numbers with Zero (i), by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). By The Factorial: Recursion, Positivity and Bounds by Powers (ii), $1\le k!\le(k+1)!$ in $\mathbb{N}_{0}$, so by (i) and The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (i), $1\le k!$ and $k!\le(k+1)!$ in $\mathbb{R}$. As $1\in\mathbb{N}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (ii), $0<1_{\mathbb{R}}$ by Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vi), that is, $0<1$ in $\mathbb{R}$ by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (i); so Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (i) gives $0<k!$ in $\mathbb{R}$, so $k!\neq0$ in $\mathbb{R}$, as $0<0$ fails by Irreflexivity of the Strict Order and Subtracting Zero in ℝ (i). By The Factorial: Recursion, Positivity and Bounds by Powers (i), $(k+1)!=(k+1)\cdot k!$ in $\mathbb{N}_{0}$, and taking images in $\mathbb{R}$, The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (iii) gives $\big((k+1)!\big)_{\mathbb{R}}=(k+1)_{\mathbb{R}}\cdot(k!)_{\mathbb{R}}$, that is, $(k+1)!=(k+1)\cdot k!$ in $\mathbb{R}$.