Proof of Properties of Finite Sums

All sums are the finite sums of that definition, whose two clauses we call the base clause and the recursion. Each claim is proved by applying the principle of induction to the set of natural numbers $n$ for which the assertion holds for all admissible data, with $S$ the successor map of Natural Numbers. We use the field axioms of $K$ throughout.

Claim 1. For $n=1$ both sides equal $a_{1}+b_{1}$ by the base clause. Assume the identity for $n$, and let $a_{k},b_{k}$ be given for $1\le k\le S(n)$. By the recursion, the inductive hypothesis, and commutativity and associativity of addition,

which rearranges to $\bigl(\sum_{k=1}^{n}a_{k}+a_{S(n)}\bigr)+\bigl(\sum_{k=1}^{n}b_{k}+b_{S(n)}\bigr)=\sum_{k=1}^{S(n)}a_{k}+\sum_{k=1}^{S(n)}b_{k}$.

Claim 2. For $n=1$ both sides equal $\lambda a_{1}$. Assume the identity for $n$. By the recursion, the inductive hypothesis and the distributive law,

Claim 3. For $n=1$ both sides equal $\overline{a_{1}}$. Assume the identity for $n$. Since conjugation preserves sums by claim 1 of Properties of Complex Conjugation and Modulus,

Claim 4. We first record two facts about real numbers, which form an ordered field. If $0\le p$ and $0\le q$, then adding $p$ to $0\le q$ gives $p\le p+q$, so $0\le p+q$ by transitivity. If moreover $p+q=0$, then $p\le p+q=0$ and $0\le p$, so $p=0$ by antisymmetry, and symmetrically $q=0$.

First assertion. For $n=1$ it is the hypothesis $0\le a_{1}$. Assume it for $n$ and let $0\le a_{k}$ for $1\le k\le S(n)$. By the inductive hypothesis $0\le\sum_{k=1}^{n}a_{k}$, and $0\le a_{S(n)}$, so the first recorded fact gives $0\le\sum_{k=1}^{n}a_{k}+a_{S(n)}=\sum_{k=1}^{S(n)}a_{k}$.

Second assertion. For $n=1$ the hypothesis reads $a_{1}=0$. Assume it for $n$ and suppose $0\le a_{k}$ for $1\le k\le S(n)$ with $\sum_{k=1}^{S(n)}a_{k}=0$. Writing $p=\sum_{k=1}^{n}a_{k}$ and $q=a_{S(n)}$, we have $0\le p$ by the first assertion, $0\le q$, and $p+q=0$, so $p=0$ and $q=0$ by the second recorded fact. Applying the inductive hypothesis to $a_{1},\dots,a_{n}$ gives $a_{k}=0$ for $1\le k\le n$, and $a_{S(n)}=q=0$.