Proof of The Square and the Fourth Power of a Sum

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.

The ring laws of Commutative Rings §ring (associativity and commutativity of $+$ and $\cdot$, $z\cdot1=z$) are used without further mention, as are the laws of arithmetic of $\mathbb{N}_{0}$ of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §laws. The numerals $2,3,4,5,6$ are as in The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §digits, so that $2=1+1$, $3=2+1$, $4=3+1$, $5=4+1$ and $6=5+1$; standing next to elements of $R$ they denote their images in $R$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals.

Clause square. This is the first identity of Rules of Arithmetic in a Commutative Ring: Zero, Signs and Squares, and No Zero Divisors in a Field §squares, applied with $x=s$ and $y=t$.

Clause fourth. By The Binomial Theorem in a Commutative Ring §binomial, applied with $x=s$, $y=t$ and $n=4$, and by The Binomial Coefficient §binomial, which identifies $\binom{4}{k}$ with $C(4,k)$ for the map $C$ of Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry §recursion, unique by that clause,

$$(s+t)^{4}=\sum_{k=0}^{4}a_{k},\qquad a_{k}=C(4,k)\,s^{k}t^{4-k}\quad(k\in\{0,\dots,4\}).$$

Arithmetic in $\mathbb{N}_{0}$. From the digit relations: $2+2=2+(1+1)=(2+1)+1=3+1=4$, $3+2=3+(1+1)=4+1=5$ and $3+3=3+(2+1)=(3+2)+1=5+1=6$. By The Difference of Two Natural Numbers with Zero §difference, $4-k$ is the unique $i$ with $k+i=4$; as $0+4=4$, $1+3=3+1=4$, $2+2=4$, $3+1=4$ and $4+0=4$, we get $4-0=4$, $4-1=3$, $4-2=2$, $4-3=1$ and $4-4=0$. Likewise $3-1=2$, as $1+2=2+1=3$.

Expanding the sum. The operation $+$ of $R$ has the neutral element $0$, and $0\le1\le2\le3\le4$ (each step $j\le j+1$ because $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, 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, and $j<j+1$ gives $j\le 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 §strict; 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). By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §interval-recursion, applied with $m=0$ and successively with upper limits $4=3+1$, $3=2+1$, $2=1+1$ and $1=0+1$, the last by Arithmetic of Addition on Omega: Recursion Rules, Associativity, Commutativity, Cancellation and Compatibility with the Order §zero,

$$\sum_{k=0}^{4}a_{k}=\Big(\Big(\Big(\sum_{k=0}^{0}a_{k}+a_{1}\Big)+a_{2}\Big)+a_{3}\Big)+a_{4}.$$

The interval $\{0,\dots,0\}$ is $\{0\}$, since $0\le k\le0$ forces $k=0$ by antisymmetry of the total order of The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion §order; so $\sum_{k=0}^{0}a_{k}=a_{0}$ by Sums and Products over a Finite Set and over an Interval §intervals and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals §singleton.

The coefficients. By Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry §recursion, $C(4,0)=1$. By Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry §diagonal, $C(4,4)=1$. By Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry §one, $C(4,1)=4$ and $C(3,1)=3$. By Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry §symmetry, applied with $n=4$, $k=1\le4$, and with $n=3$, $k=1\le3$, and the differences above, $C(4,3)=C(4,4-1)=C(4,1)=4$ and $C(3,2)=C(3,3-1)=C(3,1)=3$. By Binomial Coefficients: Existence and Uniqueness by Pascal's Recursion, Vanishing above the Diagonal, Diagonal and First Values, the Factorial Formula and Symmetry §recursion, applied with $n=3$ and $k=1$, $C(4,2)=C(3+1,1+1)=C(3,1)+C(3,2)=3+3=6$.

The terms. Reading these coefficients in $R$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §numerals, with $1_{R}=1$ 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 §constants, and using $s^{0}=t^{0}=1$ by Commutative Rings, Fields and Ordered Fields: Standard Notation §rings and $s^{1}=s$, $t^{1}=t$ by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality §product, together with the differences $4-k$ above:

$$a_{0}=1\cdot s^{0}t^{4}=t^{4},\quad a_{1}=4\,s^{1}t^{3}=4st^{3},\quad a_{2}=6\,s^{2}t^{2},\quad a_{3}=4\,s^{3}t^{1}=4s^{3}t,\quad a_{4}=1\cdot s^{4}t^{0}=s^{4}.$$

Hence

$$(s+t)^{4}=t^{4}+4st^{3}+6s^{2}t^{2}+4s^{3}t+s^{4}=s^{4}+4s^{3}t+6s^{2}t^{2}+4st^{3}+t^{4},$$

the last step by associativity and commutativity of $+$.