Proof of Properties of Finite Sums

All sums are the finite sums of that definition; we write $\sigma:[n]\to K$ for the map used there, so that $\sum_{k=1}^{j}a_{k}=\sigma(j)$ for every $j\in[n]$. Throughout we use the field axioms of $K$, the successor map $S$ of Natural Numbers, and the following facts about initial segments from claims 1 to 4 of Basic Properties of Initial Segments of the Natural Numbers: $1\in[n]$ and $n\in[n]$; $[1]=\{1\}$; $[S(n)]=[n]\cup\{S(n)\}$ with $S(n)\notin[n]$; and $[j]\subseteq[n]$ whenever $j\le n$. Claims 2 to 7 are proved by applying the principle of induction to the set of natural numbers $n$ for which the assertion in question holds for all admissible data on $[n]$.

Claim 1. Restriction. Let $j\in[n]$, let $a'$ be the restriction of $a$ to $[j]$, which is defined because $[j]\subseteq[n]$, and let $\sigma':[j]\to K$ be the map associated with $a'$ by Existence and Uniqueness of Iterates of a Binary Operation, so that $\sum_{k=1}^{i}a'_{k}=\sigma'(i)$ for every $i\in[j]$. Let $\rho$ be the restriction of $\sigma$ to $[j]$. Since $1\in[j]$ we have $\rho(1)=\sigma(1)=a_{1}=a'_{1}$. If $m\in\mathbb{N}$ satisfies $S(m)\in[j]$, then $S(m)\in[n]$, and $m\in[j]$ because $m<S(m)\le j$ by claims 5 and 1 of Properties of the Order on the Natural Numbers; hence

Thus $\rho$ satisfies the two conditions of Existence and Uniqueness of Iterates of a Binary Operation for the data $a'$, and by the uniqueness part of that lemma $\rho=\sigma'$. Therefore $\sum_{k=1}^{i}a'_{k}=\sigma(i)=\sum_{k=1}^{i}a_{k}$ for every $i\in[j]$.

Recursion. Directly from the definition, $\sum_{k=1}^{1}a_{k}=\sigma(1)=a_{1}$, and for $m\in\mathbb{N}$ with $S(m)\in[n]$,

In what follows we call these two identities the base clause and the recursion. By the restriction part of claim 1, when data are given on $[S(n)]$ a sum $\sum_{k=1}^{n}$ formed from them agrees with the corresponding sum formed from their restriction to $[n]$, so the inductive hypotheses below apply to it.

Claim 2. For $n=1$ we have $[1]=\{1\}$ and both sides equal $a_{1}+b_{1}$ by the base clause. Assume the identity for $n$ and let $a,b$ be defined on $[S(n)]$. By the recursion, the inductive hypothesis applied to the restrictions of $a$ and $b$ to $[n]$, and commutativity and associativity of addition,

which rearranges to

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

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

Claim 5. We first record two facts about real numbers, which form an ordered field. (i) If $0\le q$ then, adding $p$ to both sides, $p\le p+q$; if moreover $0\le p$, then $0\le p+q$ by transitivity. (ii) If $0\le p$, $0\le q$ and $p+q=0$, then $p\le p+q=0$ by (i) 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}$, since $\sum_{k=1}^{1}a_{k}=a_{1}$. Assume it for $n$ and let $0\le a_{k}$ for every $k\in[S(n)]$. The inductive hypothesis applied to the restriction of $a$ to $[n]$ gives $0\le\sum_{k=1}^{n}a_{k}$, and $0\le a_{S(n)}$, so (i) 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 every $k\in[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$ by the recursion, so $p=0$ and $q=0$ by (ii). Applying the inductive hypothesis to the restriction of $a$ to $[n]$ gives $a_{k}=0$ for every $k\in[n]$, and $a_{S(n)}=q=0$. Since $[S(n)]=[n]\cup\{S(n)\}$, all summands vanish.

Claim 6. For $n=1$ we have $[1]=\{1\}$, so $j=1$ and $a_{1}\le a_{1}=\sum_{k=1}^{1}a_{k}$ by reflexivity. Assume the assertion for $n$, let $0\le a_{k}$ for every $k\in[S(n)]$, and let $j\in[S(n)]=[n]\cup\{S(n)\}$. Put $T=\sum_{k=1}^{n}a_{k}$, so that $\sum_{k=1}^{S(n)}a_{k}=T+a_{S(n)}$ by the recursion, and $0\le T$ by claim 5.

If $j=S(n)$, then from $0\le T$ and fact (i) of claim 5, applied with the roles of $p$ and $q$ taken by $a_{S(n)}$ and $T$ together with commutativity of addition, we get $a_{S(n)}\le T+a_{S(n)}$.

If $j\in[n]$, the inductive hypothesis applied to the restriction of $a$ to $[n]$ gives $a_{j}\le T$, while $0\le a_{S(n)}$ and fact (i) give $T\le T+a_{S(n)}$; transitivity yields $a_{j}\le T+a_{S(n)}$.

In both cases $a_{j}\le\sum_{k=1}^{S(n)}a_{k}$, which completes the induction.

Claim 7. For $n=1$ we have $[1]=\{1\}$, so $i=1$ and $\sum_{k=1}^{1}a_{k}=a_{1}=a_{i}$ by the base clause. Assume the assertion for $n$, let $a$ be defined on $[S(n)]$, and let $i\in[S(n)]=[n]\cup\{S(n)\}$ satisfy $a_{k}=0$ for every $k\in[S(n)]$ with $k\ne i$.

If $i\in[n]$, then $S(n)\ne i$ because $S(n)\notin[n]$, so $a_{S(n)}=0$. The restriction of $a$ to $[n]$ satisfies the same hypothesis with the same distinguished index $i$, so the inductive hypothesis gives $\sum_{k=1}^{n}a_{k}=a_{i}$, and the recursion together with the additive identity gives $\sum_{k=1}^{S(n)}a_{k}=a_{i}+0=a_{i}$.

If $i=S(n)$, then $a_{k}=0$ for every $k\in[n]$. Applying the inductive hypothesis to the restriction of $a$ to $[n]$ with distinguished index $1$ gives $\sum_{k=1}^{n}a_{k}=a_{1}=0$, so the recursion gives $\sum_{k=1}^{S(n)}a_{k}=0+a_{S(n)}=a_{S(n)}=a_{i}$.