Laws of finite sums and products in $\mathbb{N}$, and $\iota\big(\sum_{k<n} a_k\big) = \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 = \big(\sum_{k<m} a_k + \sum_{j<d} a_{m+j}\big) + a_{m+d} = \sum_{k<m} a_k + \big(\sum_{j<d} a_{m+j} + a_{m+d}\big) = \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_kb_k) = \big(\prod_{k<n}(a_kb_k)\big)a_nb_n = \big(\prod_{k<n}a_k\big)\big(\prod_{k<n}b_k\big)a_nb_n = \big(\prod_{k<\sigma(n)}a_k\big)\big(\prod_{k<\sigma(n)}b_k\big)$ by associativity and commutativity. For the second assertion, note first that a product of two nonzero naturals is nonzero: if $xy = 0$ with $y \ne 0$, then $xy = 0 \cdot y$, so $x = 0$ by [L9]. Now induct: $\prod_{k<0}a_k = 1 \ne 0$ by [L9], and $\prod_{k<\sigma(n)}a_k = \big(\prod_{k<n}a_k\big)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) = \big(\sum_{k<n}a_k + \sum_{k<n}b_k\big) + (a_n+b_n) = \big(\sum_{k<n}a_k + a_n\big) + \big(\sum_{k<n}b_k + b_n\big) = \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 = \big(\sum_{k<j}a_k + a_j\big) + R$ for some $R \in \mathbb{N}$, and $a_j \le \big(\sum_{k<j}a_k + a_j\big) + 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 \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\big(\sum_{k<0}a_k\big) = \iota(0) = 0 = \sum^{\mathbb{R}}_{k<0}\iota(a_k)$. Assuming the identity at $n$, $\iota\big(\sum_{k<\sigma(n)}a_k\big) = \iota\big(\sum_{k<n}a_k + a_n\big) = \iota\big(\sum_{k<n}a_k\big) + \iota(a_n) = \sum^{\mathbb{R}}_{k<n}\iota(a_k) + \iota(a_n) = \sum^{\mathbb{R}}_{k<\sigma(n)}\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.