Laws of finite sums and products in $\mathbb{N}$, and $\iota \left({\sum }_{k<n}{a}_k\right)={\sum }_{k<n}\iota (a_k)$

Every clause is proved by induction on the upper index, using only the recursion clauses [L2], [L3] and the arithmetic [L4], [L8]; the inductions are written out one clause at a time.

The two notations agree: $\iota (n)=n\cdot 1_{\mathbb{R}}$ for every $n\ge 1$. At $n=1$, $\iota (1)=\iota (\sigma (0))=\iota (0)+1_{\mathbb{R}}=1_{\mathbb{R}}=1\cdot 1_{\mathbb{R}}$; and the successor clauses of the two recursions coincide, $\iota (\sigma (n))=\iota (n)+1_{\mathbb{R}}$ and $(n+1)\cdot 1_{\mathbb{R}}=n\cdot 1_{\mathbb{R}}+1_{\mathbb{R}}$. So the two agree at every $n\ge 1$ by induction, and [L7] may be read as a statement about $\iota$.

Clause 1 at $n=0$: both sides are the empty sum, $0=0+0$.

Clause 1, inductive hypothesis: assume ${\sum }_{k<n}(a_k+b_k)={\sum }_{k<n}{a}_k+{\sum }_{k<n}{b}_k$ for a fixed $n$ and all lists $a,b$.

Clause 2, by induction on $n$. At $n=0$ both sides are $0$, since $0\cdot c=0$. If ${\sum }_{k<n}c=n\cdot c$, then ${\sum }_{k<\sigma (n)}c={\sum }_{k<n}c+c=n\cdot c+c=\sigma (n)\cdot c$, the last equality being the successor law $\sigma (a)\cdot n=a\cdot n+n$ of [L4].

Clause 3, by induction on $d$, with $m$ fixed and $n=m+d$. At $d=0$ we have $n=m$ and the second sum is empty, so the claim reads ${\sum }_{k<m}{a}_k={\sum }_{k<m}{a}_k+0$. Assuming it at $d$, and using $m+\sigma (d)=\sigma (m+d)$, we get ${\sum }_{k<\sigma (n)}{a}_k={\sum }_{k<n}{a}_k+a_n=({\sum }_{k<m}{a}_k+{\sum }_{j<d}{a}_{m+j})+a_{m+d}={\sum }_{k<m}{a}_k+({\sum }_{j<d}{a}_{m+j}+a_{m+d})={\sum }_{k<m}{a}_k+{\sum }_{j<\sigma (d)}{a}_{m+j}$. The product form is the same argument with $+$ replaced by $\cdot$ and $0$ by $1$.

Clause 5, by induction on $n$. At $n=0$ both sides are $1=1\cdot 1$; and ${\prod }_{k<\sigma (n)}(a_k{b}_k)=({\prod }_{k<n}(a_k{b}_k))a_n{b}_n=\left({\prod }_{k<n}{a}_k\right)\left({\prod }_{k<n}{b}_k\right)a_n{b}_n=\left({\prod }_{k<\sigma (n)}{a}_k\right)\left({\prod }_{k<\sigma (n)}{b}_k\right)$ by associativity and commutativity. For the second assertion, note first that a product of two nonzero naturals is nonzero: if $xy=0$ with $y\mathrm{\ne }0$, then $xy=0\cdot y$, so $x=0$ by [L9]. Now induct: ${\prod }_{k<0}{a}_k=1\mathrm{\ne }0$ by [L9], and ${\prod }_{k<\sigma (n)}{a}_k=\left({\prod }_{k<n}{a}_k\right)a_n$ is a product of two nonzero naturals.

Clause 1, inductive step. Using [L2] twice and the associativity and commutativity of addition, ${\sum }_{k<\sigma (n)}(a_k+b_k)={\sum }_{k<n}(a_k+b_k)+(a_n+b_n)=({\sum }_{k<n}{a}_k+{\sum }_{k<n}{b}_k)+(a_n+b_n)=({\sum }_{k<n}{a}_k+a_n)+({\sum }_{k<n}{b}_k+b_n)={\sum }_{k<\sigma (n)}{a}_k+{\sum }_{k<\sigma (n)}{b}_k$, where the inductive hypothesis of step 1.4 was used at the second equality.

Clause 0. First $\iota (1)=1$, computed in step 1.2. For $m,n\ge 1$ the two identities are [L7], read through step 1.2. If $n=0$ then $\iota (m+0)=\iota (m)=\iota (m)+0=\iota (m)+\iota (0)$, and $\iota (m\cdot 0)=\iota (0)=0=\iota (m)\cdot 0=\iota (m)\iota (0)$ by [L8]; the case $m=0$ follows from these by the commutativity of addition and multiplication in $\mathbb{N}$ and in $\mathbb{R}$. So both identities hold for all $m,n\in \mathbb{N}$.

Clause 4. Monotonicity is an induction: at $n=0$ both sums are $0$; and if ${\sum }_{k<n}{a}_k\le {\sum }_{k<n}{b}_k$ and $a_n\le b_n$, then ${\sum }_{k<n}{a}_k+a_n\le {\sum }_{k<n}{b}_k+a_n\le {\sum }_{k<n}{b}_k+b_n$ by [L5], so ${\sum }_{k<\sigma (n)}{a}_k\le {\sum }_{k<\sigma (n)}{b}_k$ by transitivity. For the second assertion let $j<n$, so $1\le n-j$; splitting at $j$ and then splitting the tail at $1$, and using ${\sum }_{i<1}{a}_{j+i}=0+a_j=a_j$, gives ${\sum }_{k<n}{a}_k=({\sum }_{k<j}{a}_k+a_j)+R$ for some $R\in \mathbb{N}$, and $a_j\le ({\sum }_{k<j}{a}_k+a_j)+R$ because $a_j$ plus something equals it.

Clause 1 holds for every $n$, by step 1.3 and step 2.1 together with induction.

Clause 7. If $m<n$ put $d=n-m$, so $m+d=n$ and $d\mathrm{\ne }0$, hence $d\ge 1$ and $\iota (d)>0$ by [L7]; then $\iota (n)=\iota (m)+\iota (d)>\iota (m)$ by step 2.2. Conversely, if $\iota (m)<\iota (n)$ then $m=n$ and $n<m$ are both excluded, the first because the order of $\mathbb{R}$ is irreflexive and the second by what was just proved, so $m<n$ by trichotomy in $\mathbb{N}$. The statement about equality follows by trichotomy on both sides.

Clause 6, by induction on $n$. At $n=0$, $\iota \left({\sum }_{k<0}{a}_k\right)=\iota (0)=0={\sum }_{k<0}^{\mathbb{R}}\iota (a_k)$. Assuming the identity at $n$, $\iota \left({\sum }_{k<\sigma (n)}{a}_k\right)=\iota ({\sum }_{k<n}{a}_k+a_n)=\iota \left({\sum }_{k<n}{a}_k\right)+\iota (a_n)={\sum }_{k<n}^{\mathbb{R}}\iota (a_k)+\iota (a_n)={\sum }_{k<\sigma (n)}^{\mathbb{R}}\iota (a_k)$, the second equality by step 2.2. The product form is the same induction, starting from $\iota (1)=1$ and using multiplicativity.

Clause 0 is step 2.2, clause 1 is step 3.1, clause 2 is step 1.5, clause 3 is step 1.6, clause 4 is step 2.3, clause 5 is step 1.7, clause 6 is step 3.3 and clause 7 is step 3.2.