Proof of Partial Sums of a Sequence in [0,∞]: First Term, Recursion and Two-Term Sums

By Sum of a Sequence in [0,∞] (i), $+$ is a binary operation on $[0,\infty]$ and, for $n\in\mathbb{N}$, $s_{n}=\sum_{k=1}^{n}a_{k}$ is the iterated operation of $+$ applied to the restriction $a|_{[n]}:[n]\to[0,\infty]$ of $(a_{k})$ (Iterated Operations: Finite Sums and Finite Products (ii)).

Proof of (i). By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), $[1]=\{1\}$ is a subset of $\mathbb{N}$, the domain of $(a_{k})$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix), the map $a|_{[1]}:[1]\to[0,\infty]$ has value $a_{1}$ at $1\in[1]$, and its restriction $(a|_{[1]})|_{[1]}$ is a function with domain $[1]\cap[1]=[1]$ and the same values as $a|_{[1]}$; so $(a|_{[1]})|_{[1]}=a|_{[1]}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i). Hence the iterated operation $\sum_{k=1}^{1}$ of the map $a|_{[1]}$, read as in Iterated Operations: Finite Sums and Finite Products (ii), is that of $a|_{[1]}$ itself, which is $s_{1}$. The first part of Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), applied to $+$ on $[0,\infty]$ and to the map $a|_{[1]}:[1]\to[0,\infty]$, therefore gives $s_{1}=a_{1}$.

Proof of (ii). Let $n\in\mathbb{N}$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), $[n]$ and $[n+1]$ are subsets of $\mathbb{N}$, the domain of $(a_{k})$, and $[n+1]=[n]\cup\{n+1\}$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (ii); so $[n]\subseteq[n+1]$ and $n+1\in[n+1]$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ix), the map $a|_{[n+1]}:[n+1]\to[0,\infty]$ has value $a_{n+1}$ at $n+1$; its restriction $(a|_{[n+1]})|_{[n]}$ is a function with domain $[n]\cap[n+1]=[n]$ and value $a_{k}$ at every $k\in[n]$, as is $a|_{[n]}$, so $(a|_{[n+1]})|_{[n]}=a|_{[n]}$ by Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (i); and likewise $(a|_{[n+1]})|_{[n+1]}=a|_{[n+1]}$. Hence the iterated operations $\sum_{k=1}^{n+1}$ and $\sum_{k=1}^{n}$ of the map $a|_{[n+1]}$, read as in Iterated Operations: Finite Sums and Finite Products (ii), are those of $a|_{[n+1]}$ and of $a|_{[n]}$, that is, $s_{n+1}$ and $s_{n}$. So the second part of Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), applied to $+$ on $[0,\infty]$ and to $a|_{[n+1]}$, gives $s_{n+1}=s_{n}+a_{n+1}$.

Proof of (iii). Since $2=1+1$ by Arithmetic and Order of the Natural Numbers (xiv), $1<2$ by Arithmetic and Order of the Natural Numbers (xi). Let $k\in\mathbb{N}$ with $2<k$. Then $k\neq2$ by Arithmetic and Order of the Natural Numbers (vii); and $1<k$ by Arithmetic and Order of the Natural Numbers (vi), so $k\neq1$ by Arithmetic and Order of the Natural Numbers (vii). Hence $a_{k}=0$. By Sums of Sequences in [0,∞]: Real Series, Linearity, Comparison, Rearrangement, Double Series and Monotone Convergence (vii) with $n=2$, $\sum_{k\in\mathbb{N}}a_{k}=s_{2}$. As $2=1+1$, (ii) with $n=1$ and (i) give $s_{2}=s_{1}+a_{2}=a_{1}+a_{2}$. Hence $\sum_{k\in\mathbb{N}}a_{k}=a_{1}+a_{2}$.