Proof of The Factorial: Recursion, Positivity and Bounds by Powers

Each result cited below is universally quantified over the data in its own statement, and is applied to the data named where it is cited.

Throughout, all computations take place in $\mathbb{N}_{0}$ with its addition, multiplication and order of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §operations and The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order. By Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §associative, Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §commutative and Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §one, with $1=S(0)$ by The Set of Natural Numbers and the Number One §one, the multiplication of $\mathbb{N}_{0}$ is associative and commutative with neutral element $1$, so Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals applies to it with $X=\mathbb{N}_{0}$ and $e=1$. By The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §well-order and Well-Orders on a Set §well-order, the order of $\mathbb{N}_{0}$ is a total order, in particular reflexive, antisymmetric and transitive. For $n\in\mathbb{N}_{0}$, $S(n)=n+1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §successor, so induction from zero, The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction, applies with the step from $n$ to $n+1$. We use three auxiliary facts.

(A) Intervals. $\{1,\dots,0\}=\emptyset$, and $1\le n+1$ for every $n\in\mathbb{N}_{0}$. Indeed, by Intervals of Natural Numbers §interval, an element $k$ of $\{1,\dots,0\}$ would satisfy $1\le k\le0$, hence $1\le0$; but $0<S(0)=1$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §successor, so $0\le1$ and $0\neq1$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §strict, and $1\le0$ would give $0=1$ by antisymmetry. Further, $0\le n$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §zero-least, so $1+0\le1+n$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §order, that is $1\le n+1$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero and Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §commutative.

(B) Monotonicity of products. Let $x,y,z\in\mathbb{N}_{0}$ with $x\le y$. By Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §difference there is $d\in\mathbb{N}_{0}$ with $y=x+d$, so $zy=zx+zd$ by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §distributive, and $zx\le zy$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §difference; by commutativity also $xz\le yz$. Likewise $x\le x+d$ for all $x,d\in\mathbb{N}_{0}$, by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §difference.

(C) Powers. Let $x\in\mathbb{N}_{0}$, with powers for the multiplication of $\mathbb{N}_{0}$ as in Powers with Exponents in the Natural Numbers with Zero §power and Powers with Exponents in the Natural Numbers with Zero §zero, and let $c$ be the map $k\mapsto x$ on $\mathbb{N}_{0}$. For every $n\in\mathbb{N}_{0}$, $x^{n}=\prod_{k=1}^{n}c_{k}$, the product over the interval $\{1,\dots,n\}$ of Sums and Products over a Finite Set and over an Interval §intervals: for $1\le n$, $x^{n}$ is the finite product of Iterated Operations: Finite Sums and Finite Products §iterated and Iterated Operations: Finite Sums and Finite Products §sums, which agrees with the interval product by Sums and Products over a Finite Set and over an Interval §intervals; for $n=0$, the interval is empty by (A), so the interval product is $1$ by Sums and Products over a Finite Set and over an Interval §empty, and $x^{0}=1$. Since $1\le n+1$ by (A), Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §interval-recursion with $m=1$ gives $x^{n+1}=x^{n}\cdot x$. In particular $x^{1}=1\cdot x=x$. Consequently, if $x\le y$ in $\mathbb{N}_{0}$, then $x^{k}\le y^{k}$ for every $k\in\mathbb{N}_{0}$, by induction on $k$: $x^{0}=1=y^{0}$, and if $x^{k}\le y^{k}$, then $x^{k+1}=x^{k}x\le y^{k}x\le y^{k}y=y^{k+1}$ by (B) and transitivity.

Recursion. By The Factorial of a Natural Number with Zero §factorial, $n!$ is the product over the interval $\{1,\dots,n\}$ of the map $k\mapsto k$ on $\mathbb{N}_{0}$. For $n=0$ this interval is empty by (A), so $0!=1$ by Sums and Products over a Finite Set and over an Interval §empty. Since $1\le n+1$ by (A), Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §interval-recursion with $m=1$ gives

$$(n+1)!=\prod_{k=1}^{n+1}k=\Big(\prod_{k=1}^{n}k\Big)\cdot(n+1)=n!\cdot(n+1)=(n+1)\cdot n!,$$

the last step by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §commutative.

Positive. By the recursion clause and Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §successor, $(n+1)!=S(n)\cdot n!=n\cdot n!+n!$, which equals $n!+n\cdot n!$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §commutative; hence $n!\le(n+1)!$ by (B), for every $n\in\mathbb{N}_{0}$. Now $1\le n!$ for every $n\in\mathbb{N}_{0}$ by induction: $0!=1$, so $1\le0!$ by reflexivity; and if $1\le n!$, then $1\le n!\le(n+1)!$ gives $1\le(n+1)!$ by transitivity.

Lower. By induction on $n$. For $n=0$: $2^{0}=1$ by (C), and $1!=(0+1)\cdot0!=1\cdot1=1$ by the recursion clause, so $2^{0}\le1!$. Suppose $2^{n}\le(n+1)!$. Since $0\le n$ by The Order on Omega Is a Well-Order with Membership as Its Strict Order, and Nothing Lies between n and Its Successor §zero-least, $2=2+0\le2+n=n+2$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero, Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §order and Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §commutative. Moreover $(n+1)+1=n+(1+1)=n+2$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §associative and Arithmetic and Order of the Natural Numbers §digits. By (C), (B), the recursion clause applied to $n+1$, and transitivity,

$$2^{n+1}=2^{n}\cdot2\le(n+1)!\cdot2\le(n+1)!\cdot(n+2)=(n+2)\cdot(n+1)!=((n+1)+1)!.$$

Upper. By induction on $n$. For $n=0$: $1!=(0+1)\cdot0!=1\cdot1=1=1^{1}$ by the recursion clause and (C). Suppose $(n+1)!\le(n+1)^{n+1}$. As $n+2=(n+1)+1$, shown in the proof of the clause lower by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §associative and Arithmetic and Order of the Natural Numbers §digits, (B) gives $n+1\le n+2$, hence $(n+1)^{n+1}\le(n+2)^{n+1}$ by (C). By the recursion clause applied to $n+1$, (B), commutativity, (C) and transitivity,

$$((n+1)+1)!=(n+2)\cdot(n+1)!\le(n+2)\cdot(n+1)^{n+1}\le(n+2)\cdot(n+2)^{n+1}=(n+2)^{n+1}\cdot(n+2)=(n+2)^{n+2},$$

which is the claim for $n+1$, since $n+2=(n+1)+1$.