Proof of Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry

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, $+$, $\cdot$, $\le$ and $<$ are those of $\mathbb{N}_{0}$ as in 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, and the laws of arithmetic of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws (associativity, commutativity and distributivity of $+$ and $\cdot$, $m+0=0+m=m$ and $m\cdot1=m$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero and Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one) are used without further mention. The order $\le$ is a well-order, hence a total order, on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order; it is reflexive, antisymmetric and transitive by Partial and Total Orders on a Set and the Associated Strict Relation §partial, its strict relation is $<$ 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 $<$ is transitive by Uniqueness of Least and Greatest Elements, Properties of the Strict Order, and Trichotomy for Total Orders §strict-transitive.

Preliminary facts. Let $j,k,m,n\in\mathbb{N}_{0}$.

(P1) Either $k=0$ or $k=j+1$ for some $j\in\mathbb{N}_{0}$: by Omega Is the Least Inductive Class: It Is a Set, Induction from Zero, the Peano Properties, and Transitivity §cases, the successor of $j$ being $j+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one.

(P2) $1\neq0$, and $k\ge1$ if and only if $k\neq0$. Indeed $1\in\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §sets, so $1\neq0$. If $k\neq0$, then $k\in\mathbb{N}$, so $1\le k$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one. If $1\le k$ and $k=0$, then $1\le0$ and $0\le1$ 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$ by antisymmetry, which is false. In particular $j+1\neq0$, since $j+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §successors, the successor $S(j)$ of $j$ being $j+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §plus-one, and so $1\le j+1$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication §one.

(P3) $j<j+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; $j<n$ if and only if $j+1\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 §successor-below; and $j\le n$ if and only if $j+1\le n+1$, and $j<n$ if and only if $j+1<n+1$, by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §order and commutativity.

(P4) If $n<k$, then $k\neq0$: by (P3) $n+1\le k$, and $1\le n+1$ by (P2), so $1\le k$ by transitivity and $k\neq0$ by (P2).

(P5) For $m\le n$, $n-m$ is the unique $i\in\mathbb{N}_{0}$ with $m+i=n$, by The Difference of Two Natural Numbers with Zero §difference. Hence, checking in each case that the proposed value $i$ satisfies $m+i=n$: $n-0=n$, as $0+n=n$; $n-n=0$, as $n+0=n$; $(n+1)-(m+1)=n-m$, as $m+1\le n+1$ by (P3) and $(m+1)+(n-m)=(m+(n-m))+1=n+1$; $(n+1)-m=(n-m)+1$, as $m\le n\le n+1$ by (P3) and transitivity, and $m+((n-m)+1)=(m+(n-m))+1=n+1$; $n-m\le n$ by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §difference, as $(n-m)+m=m+(n-m)=n$; and therefore $n-(n-m)=m$, as $(n-m)+m=n$.

Clause recursion, existence. The values of row $n+1$ depend on all values of row $n$, so the recursion is run on whole rows, that is in the set of maps from $\mathbb{N}_{0}$ to $\mathbb{N}_{0}$. Let $X=\mathbb{N}_{0}^{\mathbb{N}_{0}}$, a set by Sets and Maps: Ordinary Notation §maps. By Maps Defined by Cases §cases, applied with $A=B=\mathbb{N}_{0}$, the property $k=0$, $t_{1}(k)=1$ and $t_{2}(k)=0$, there is exactly one map $e:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $e(0)=1$ and $e(k)=0$ for every $k\neq0$; so $e\in X$. For $r\in X$, by Maps Defined by Cases §cases, applied with $A=B=\mathbb{N}_{0}$, the parameter $r$, the property $k=0$, $t_{1}(k)=1$ and $t_{2}(k)=r(k-1)+r(k)$, which lies in $\mathbb{N}_{0}$ for $k\neq0$ because then $1\le k$ by (P2) and the difference $k-1$ is defined, there is exactly one map $z:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $z(0)=1$ and $z(k)=r(k-1)+r(k)$ for every $k\neq0$. Let $\theta(z,r)$ be the condition: $z$ is a map from $\mathbb{N}_{0}$ to $\mathbb{N}_{0}$, $z(0)=1$, and $z(k)=r(k-1)+r(k)$ for every $k\in\mathbb{N}_{0}$ with $k\neq0$. In it $k-1$ is used properly, since $k\neq0$ gives $1\le k$ by (P2). The condition quantifies over set variables only and is built from abbreviations introduced in earlier items, so it is a predicative expression in the sense of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols. We write $r^{+}$ for the unique set $z$ with $\theta(z,r)$: this is a defined set symbol with the set argument $r$, and it is used properly wherever $r\in X$ is in force, since for every $r\in X$ the application of Maps Defined by Cases §cases just made shows that exactly one set $z$ with $\theta(z,r)$ exists. In particular $r^{+}\in X$ for every $r\in X$. By Sets and Maps: Ordinary Notation §maps (via Maps and Relations Given by Formulas §binary) there is exactly one map $g:\mathbb{N}_{0}\times X\to X$ with $g(n,r)=r^{+}$ for all $n\in\mathbb{N}_{0}$ and $r\in X$. By The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §recursion, that is by The Recursion Theorem on Omega §recursion applied with the set $X$, the element $e$ and the map $g$, the successor of $n$ being $n+1$, there is exactly one map $F:\mathbb{N}_{0}\to X$ with $F(0)=e$ and $F(n+1)=g(n,F(n))=F(n)^{+}$ for every $n\in\mathbb{N}_{0}$.

Since $F(n)\in X$, $F(n)(k)\in\mathbb{N}_{0}$ for all $n,k\in\mathbb{N}_{0}$, so by Sets and Maps: Ordinary Notation §maps there is a map $C:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $C(n,k)=F(n)(k)$. It satisfies the three conditions. First, $C(0,0)=e(0)=1$, and for $n=m+1$ with $m\in\mathbb{N}_{0}$, $C(m+1,0)=F(m)^{+}(0)=1$; by (P1), $C(n,0)=1$ for every $n$. Second, for $k\ge1$ we have $k\neq0$ by (P2), so $C(0,k)=e(k)=0$. Third, $k+1\neq0$ by (P2) and $(k+1)-1=k$ by (P5), as $1+k=k+1$; hence

$$C(n+1,k+1)=F(n)^{+}(k+1)=F(n)(k)+F(n)(k+1)=C(n,k)+C(n,k+1).$$

Clause recursion, uniqueness. Let $C':\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ also satisfy the three conditions, and let $K=\{n\in\mathbb{N}_{0}:C'(n,k)=C(n,k)\text{ for every }k\in\mathbb{N}_{0}\}$. We have $0\in K$: $C'(0,0)=1=C(0,0)$, and for $k\neq0$, $k\ge1$ by (P2) and $C'(0,k)=0=C(0,k)$. Let $n\in K$ and $k\in\mathbb{N}_{0}$. If $k=0$, then $C'(n+1,0)=1=C(n+1,0)$. Otherwise $k=j+1$ by (P1), and $C'(n+1,j+1)=C'(n,j)+C'(n,j+1)=C(n,j)+C(n,j+1)=C(n+1,j+1)$. So $n+1\in K$, and $K=\mathbb{N}_{0}$ by induction (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §induction). Every element of $\mathbb{N}_{0}\times\mathbb{N}_{0}$ is a pair $(n,k)$ with $n,k\in\mathbb{N}_{0}$ by The Cartesian Product of Two Classes §product, and conversely every such pair is an element of $\mathbb{N}_{0}\times\mathbb{N}_{0}$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, so $C'$ and $C$ have the same domain and the same values, and $C'=C$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction §equality. This proves the clause recursion; from now on $C$ is this unique map.

Clause above. Let $K=\{n\in\mathbb{N}_{0}:C(n,k)=0\text{ for every }k\in\mathbb{N}_{0}\text{ with }k>n\}$. If $k>0$, then $k\neq0$ by (P4), so $k\ge1$ by (P2) and $C(0,k)=0$; thus $0\in K$. Let $n\in K$ and $k>n+1$. Then $k\neq0$ by (P4), so $k=j+1$ for some $j$ by (P1), and $n<j$ by (P3). As $j<j+1$ by (P3), also $n<j+1$ by transitivity of $<$. Since $n\in K$, $C(n,j)=0$ and $C(n,j+1)=0$, so $C(n+1,k)=C(n,j)+C(n,j+1)=0+0=0$. Hence $n+1\in K$, and $K=\mathbb{N}_{0}$ by induction.

Clause diagonal. $C(0,0)=1$. If $C(n,n)=1$, then, as $n<n+1$ by (P3), the clause above gives $C(n,n+1)=0$, so $C(n+1,n+1)=C(n,n)+C(n,n+1)=1+0=1$. By induction, $C(n,n)=1$ for every $n$.

Clause one. $C(0,1)=0$, as $1\ge1$ by reflexivity. If $C(n,1)=n$, then, as $1=0+1$, $C(n+1,1)=C(n,0)+C(n,1)=1+n=n+1$. By induction, $C(n,1)=n$ for every $n$.

Clause factorial. By The Factorial: Recursion, Positivity and Bounds by Powers §recursion, $0!=1$ and $(m+1)!=(m+1)\cdot m!$ for every $m\in\mathbb{N}_{0}$. Let $K=\{n\in\mathbb{N}_{0}:k!\,(n-k)!\,C(n,k)=n!\text{ for every }k\in\mathbb{N}_{0}\text{ with }k\le n\}$.

$0\in K$: if $k\le0$, then $k=0$ by antisymmetry, as $0\le k$ 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; and $0!\,(0-0)!\,C(0,0)=1\cdot0!\cdot1=1=0!$, using $0-0=0$ from (P5).

Let $n\in K$ and $k\le n+1$. If $k=0$, then by (P5) and the clause recursion, $0!\,((n+1)-0)!\,C(n+1,0)=1\cdot(n+1)!\cdot1=(n+1)!$. If $k=n+1$, then by (P5) and the clause diagonal, $(n+1)!\,((n+1)-(n+1))!\,C(n+1,n+1)=(n+1)!\cdot0!\cdot1=(n+1)!$. Otherwise $k\neq0$, so $k=j+1$ for some $j$ by (P1); then $j\le n$ by (P3), and $j\neq n$ as $k\neq n+1$, so $j<n$ 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 $j+1\le n$ by (P3). As $n\in K$, applied to $j\le n$ and to $j+1\le n$,

$$j!\,(n-j)!\,C(n,j)=n!\qquad\text{and}\qquad(j+1)!\,(n-(j+1))!\,C(n,j+1)=n!.$$

Let $m=n-(j+1)$, so that $(j+1)+m=n$ by (P5). Then $j+(m+1)=(j+1)+m=n$, so $n-j=m+1$ by (P5), and $(n+1)-(j+1)=n-j=m+1$ by (P5). Using $(j+1)!=(j+1)\cdot j!$ and $(m+1)!=(m+1)\cdot m!$,

$$\begin{aligned} k!\,((n+1)-k)!\,C(n+1,k)&=(j+1)!\,(m+1)!\,\big(C(n,j)+C(n,j+1)\big)\\ &=(j+1)\cdot\big(j!\,(m+1)!\,C(n,j)\big)+(m+1)\cdot\big((j+1)!\,m!\,C(n,j+1)\big)\\ &=(j+1)\cdot\big(j!\,(n-j)!\,C(n,j)\big)+(m+1)\cdot\big((j+1)!\,(n-(j+1))!\,C(n,j+1)\big)\\ &=(j+1)\cdot n!+(m+1)\cdot n!=\big((j+1)+(m+1)\big)\cdot n!=(n+1)\cdot n!=(n+1)!, \end{aligned}$$

since $(j+1)+(m+1)=((j+1)+m)+1=n+1$. Hence $n+1\in K$, and $K=\mathbb{N}_{0}$ by induction.

Clause symmetry. Let $k\le n$. By (P5), $n-k\le n$ and $n-(n-k)=k$. The clause factorial, applied to $k$ and to $n-k$, gives

$$k!\,(n-k)!\,C(n,k)=n!=(n-k)!\,k!\,C(n,n-k)=k!\,(n-k)!\,C(n,n-k).$$

By The Factorial: Recursion, Positivity and Bounds by Powers §positive, $1\le k!$ and $1\le(n-k)!$, so $k!\neq0$ and $(n-k)!\neq0$ by (P2), and $k!\,(n-k)!\neq0$ by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §no-zero-divisors. Hence $C(n,k)=C(n,n-k)$ by Arithmetic of Multiplication on Omega: Recursion Rules, Distributivity, Associativity, Commutativity, No Zero Divisors, Cancellation and Compatibility with the Order §cancellation.