Laws of finite sums and finite products

Base case $n=0$: every claim holds at $n=0$, since both sides of claim 1 are $0=0+0$, both sides of claim 2 are $0=\lambda \cdot 0$ and $0=0\lambda$, claim 4 reads $0\le 0$ with no term to bound and the hypothesis ${\sum }_{k<0}{a}_k=0$ giving nothing to prove, claim 5 reads $0=c_0-c_0$, and claim 6 reads $1=1\cdot 1$ with $1>0$.

Inductive hypothesis: fix $n\in \mathbb{N}$ and assume claims 1, 2, 4, 5 and 6 hold for this $n$ and for all sequences $a,b,c$ and all $\lambda$.

Splitting, claim 3: fix $m$ and prove for every natural $d$ the identities ${\sum }_{k<m+d}{a}_k={\sum }_{k<m}{a}_k+{\sum }_{j<d}{a}_{m+j}$ and ${\prod }_{k<m+d}{a}_k=({\prod }_{k<m}{a}_k)({\prod }_{j<d}{a}_{m+j})$. For $d=0$, [L7] gives $m+0=m$ and [L1, L2] give addition of $0$ and multiplication by $1$. If the two identities hold for $d$, then $m+(d+1)=(m+d)+1$ by [L7]; recursion and associativity give ${\sum }_{k<m+(d+1)}{a}_k={\sum }_{k<m+d}{a}_k+a_{m+d}={\sum }_{k<m}{a}_k+({\sum }_{j<d}{a}_{m+j}+a_{m+d})={\sum }_{k<m}{a}_k+{\sum }_{j<d+1}{a}_{m+j}$. Likewise, ${\prod }_{k<m+(d+1)}{a}_k=({\prod }_{k<m+d}{a}_k)a_{m+d}=({\prod }_{k<m}{a}_k)(({\prod }_{j<d}{a}_{m+j})a_{m+d})=({\prod }_{k<m}{a}_k)({\prod }_{j<d+1}{a}_{m+j})$. Thus [L3] proves both identities for every $d$. Given the stated $m\le n$, choose the unique $d$ with $m+d=n$ by [L7]; substituting $n=m+d$ and using the lower-index notation in [L1] proves claim 3, including $m=n$ and $m=n=0$.

Additivity at $n+1$: ${\sum }_{k<n+1}(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<n+1}{a}_k+{\sum }_{k<n+1}{b}_k$, using the recursion clause, the hypothesis, and commutativity with associativity of addition.

Scaling at $n+1$: ${\sum }_{k<n+1}\lambda a_k={\sum }_{k<n}\lambda a_k+\lambda a_n=\lambda {\sum }_{k<n}{a}_k+\lambda a_n=\lambda ({\sum }_{k<n}{a}_k+a_n)=\lambda {\sum }_{k<n+1}{a}_k$ by the recursion clause, the hypothesis and distributivity; taking $a_k=1$ for all $k$ gives ${\sum }_{k<n+1}\lambda ={\sum }_{k<n}\lambda +\lambda =n\lambda +\lambda =(n+1)\lambda$.

Monotonicity at $n+1$: assume $a_k\le b_k$ for all $k<n+1$; then $a_k\le b_k$ for all $k<n$, so the hypothesis gives ${\sum }_{k<n}{a}_k\le {\sum }_{k<n}{b}_k$, and adding the inequality $a_n\le b_n$ gives ${\sum }_{k<n+1}{a}_k={\sum }_{k<n}{a}_k+a_n\le {\sum }_{k<n}{b}_k+b_n={\sum }_{k<n+1}{b}_k$.

Telescoping at $n+1$: ${\sum }_{k<n+1}(c_{k+1}-c_k)={\sum }_{k<n}(c_{k+1}-c_k)+(c_{n+1}-c_n)=(c_n-c_0)+(c_{n+1}-c_n)=c_{n+1}-c_0$, by the recursion clause, the hypothesis and the field identities.

Products at $n+1$: ${\prod }_{k<n+1}(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<n+1}{a}_k\right)\left({\prod }_{k<n+1}{b}_k\right)$ by the recursion clause, the hypothesis, and commutativity with associativity of multiplication; and if every $a_k\ge 0$ for $k<n+1$ then ${\prod }_{k<n+1}{a}_k=\left({\prod }_{k<n}{a}_k\right)a_n$ is a product of two nonnegatives, hence nonnegative, with the same argument giving positivity from positivity since ${\prod }_{k<0}{a}_k=1>0$.

Consequences of monotonicity, completing claim 4: monotonicity itself holds at every $n$, by the induction principle applied to the base case of step 1.1 and the successor step 2.3, so it is available for an arbitrary $n$ in what follows; if $a_k\ge 0$ for all $k<n$ then comparing with the zero sequence gives ${\sum }_{k<n}{a}_k\ge {\sum }_{k<n}0=0$; for $j<n$ splitting at $j$ and then at $j+1$ writes ${\sum }_{k<n}{a}_k={\sum }_{k<j}{a}_k+a_j+{\sum }_{k=j+1}^{n-1}{a}_k$ with the first and third summands $\ge 0$, so $a_j\le {\sum }_{k<n}{a}_k$; and if moreover ${\sum }_{k<n}{a}_k=0$ then $0\le a_j\le 0$ for every $j<n$, so $a_j=0$.

By the induction principle claims 1, 2, 4, 5 and 6 hold for every $n\in \mathbb{N}$, and claim 3 was proved in step 1.3 with its consequences in step 3.1, so all six laws hold.