Proof of Recursion for the Factorial of a Natural Number

Each result cited below is universally quantified over the data in its own statement; it is applied to the data named at the point of use. Throughout, the factors of the finite products that occur are the images in $\mathbb{R}$ of natural numbers under the canonical map, so that every such product is a real number.

Claim 1. $1!=1$.

By Factorial of a Natural Number, $1!=\prod_{i=1}^{1}i$, and the base clause of Finite Product Notation gives $\prod_{i=1}^{1}a_{i}=a_{1}$ for any family $(a_{i})$. Hence $1!$ is the image in $\mathbb{R}$ of the natural number $1$, which is $1$ by claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field.

Claim 2. $(n+1)!=(n+1)\cdot n!$ for every $n\in\mathbb{N}$.

Fix $n\in\mathbb{N}$. Addition of natural numbers is commutative by claim 4 of Arithmetic of Addition on the Natural Numbers, so $n+1=1+n$.

First, the recursive clause of Finite Product Notation applies to the index $n+1$. That clause is stated for natural numbers $N$ with $2\le N$, the numeral $2$ denoting $1+1$. By claim 4 of Properties of the Order on the Natural Numbers one has $1\le n$, and by claim 6 of that lemma $j\le t$ implies $m+j\le m+t$; taking $m=j=1$ and $t=n$ gives $2=1+1\le1+n=n+1$.

Second, the notation $N-1$ occurring in that clause, for a natural number $N$ with $1<N$, is to be read as the unique $j\in\mathbb{N}$ with $N=1+j$; such a $j$ exists and is unique by claim 7 of Properties of the Order on the Natural Numbers, and this is the only reading under which $N-1$ denotes a natural number, subtraction not being defined on $\mathbb{N}$. Here $1<n+1$, since claim 6 of Properties of the Order on the Natural Numbers gives $m<m+j$ for all $m,j\in\mathbb{N}$, so that $1<1+n=n+1$; and $n+1=1+n$, so uniqueness identifies the index as $(n+1)-1=n$.

The recursive clause therefore reads

Taking $a_{i}$ to be the image of $i$ in $\mathbb{R}$ and applying Factorial of a Natural Number to $n+1$ and to $n$ gives

the last factor being the image of $n+1$ in $\mathbb{R}$. Multiplication in $\mathbb{R}$ is commutative, $\mathbb{R}$ being a field, so $(n+1)!=(n+1)\cdot n!$, which is Claim 2 and completes the proof.