Proof of Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations

Proof of (i). The addition of $\mathbb{R}$ is an associative and commutative binary operation on $\mathbb{R}$ with neutral element $0$, by Addition on ℝ Is an Associative and Commutative Binary Operation (i), Addition on ℝ Is an Associative and Commutative Binary Operation (ii) and The Structure of ℝ as a Field and an Ordered Ring (vi). By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i), applied to $+$ and the map $a:\mathbb{N}\to\mathbb{R}$, there is a map $s:\mathbb{N}\to\mathbb{R}$ with $s(n)=\sum_{k=1}^{n}a_{k}$ for every $n\in\mathbb{N}$, the sum being the iterated operation of the restriction $a|_{[n]}$ as in Iterated Operations: Finite Sums and Finite Products (ii). The restriction $a|_{[n]}$ is a map $[n]\to\mathbb{R}$ by Domains and Restrictions of Maps (ii), and the sum $\sum_{k=1}^{n}a_{k}$ over the interval $\{1,\dots,n\}=[n]$ of Sums and Products over a Finite Set and over an Interval (iv) is, by Sums and Products over a Finite Set and over an Interval (iii), the sum over $[n]$ of the same restriction; the two readings agree by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (v), applied to $a|_{[n]}$. So $s$ is a sequence in $\mathbb{R}$ by Sequences (i), its $n$-th term is the $n$-th partial sum of $(a_{k})$, and $s$ is the sequence of partial sums of $(a_{k})$.

As $1\in\mathbb{N}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (ii), $[1]=\{1\}$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), so $s_{1}$ is the sum over $\{1\}$ of $a|_{\{1\}}$, which is $a|_{\{1\}}(1)=a_{1}$ by Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i) and Domains and Restrictions of Maps (iii).

Let $n\in\mathbb{N}$. Then $n+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi) and $1\le n+1$ by Arithmetic and Order of the Natural Numbers (x), and $\{1,\dots,n+1\}=[n+1]=\{k\in\mathbb{N}:k\le n+1\}$ is contained in $\mathbb{N}$, the domain of $a$, by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i). Hence Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii), with $m=1$, gives $\sum_{k=1}^{n+1}a_{k}=\Big(\sum_{k=1}^{n}a_{k}\Big)+a_{n+1}$, that is, $s_{n+1}=s_{n}+a_{n+1}$.

Proof of (ii). For $k\in\mathbb{N}$, $p,k\in\mathbb{N}_{0}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (i), and $p+k\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi), so $a(p+k)$ is defined and lies in $\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii). The expression $a(p+k)$ is built from the value of the addition of $\mathbb{N}_{0}$ at $(p,k)$ and the value of $a$ there, defined set symbols that are used properly for $k\in\mathbb{N}$. Indeed, let $k\in\mathbb{N}$; the addition $+$ of $\mathbb{N}_{0}$ is a map $\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$, as a binary operation on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv), and $a$ is a map $\mathbb{N}\to\mathbb{R}$, so by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), for all sets $w$ and $z$, $((p,k),w)\in{+}$ if and only if $w=p+k$, and, for $w\in\mathbb{N}$, $(w,z)\in a$ if and only if $z=a(w)$. The formulas $((p,k),w)\in{+}$ and $(w,z)\in a$ are predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii), and the two symbols are eliminated through them: $a(p+k)$ is introduced by the formula $\theta(z,k)$, $\exists w\,(((p,k),w)\in{+}\wedge(w,z)\in a)$, predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and for $k\in\mathbb{N}$ exactly one $z$ satisfies $\theta(z,k)$, namely $a(p+k)$, since the only $w$ with $((p,k),w)\in{+}$ is $p+k\in\mathbb{N}$. By Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathbb{R}$ for its $a$ and $b$, there is exactly one map $d:\mathbb{N}\to\mathbb{R}$ with $d(k)=a_{p+k}$ for every $k\in\mathbb{N}$; it is a sequence in $\mathbb{R}$ by Sequences (i).

Proof of (iii). Let $k\in\mathbb{N}$. Then $1\le k$ by Arithmetic and Order of the Natural Numbers (x), and $1,k\in\mathbb{N}_{0}$ by Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (i) and Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n (ii), so by The Difference of Two Natural Numbers with Zero (i), $k-1$ is the unique $j\in\mathbb{N}_{0}$ with $1+j=k$. The condition $j\in\mathbb{N}_{0}\wedge((1,j),k)\in{+}$, with $+$ the addition of $\mathbb{N}_{0}$, is predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iv), so $k-1$ is a defined set symbol with argument $k$, introduced by this condition and used properly where $k\in\mathbb{N}$, and it is eliminated as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii). As $k-1\in\mathbb{N}_{0}$, $q(k-1)$ is defined and lies in $\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), the value of $q$ being eliminated as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x), through the formula $(j,z)\in q$, predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii). By Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathbb{R}$ for its $a$ and $b$, there is exactly one map $r:\mathbb{N}\to\mathbb{R}$ with $r(k)=q(k-1)$ for every $k\in\mathbb{N}$, a sequence in $\mathbb{R}$ by Sequences (i).

Proof of (iv). By Absolute Value and Squaring as Maps on the Reals, and Entrywise Absolute Values and Squares of a Real Matrix (i) there is a map $\alpha:\mathbb{R}\to\mathbb{R}$ with $\alpha(x)=|x|$ for every $x\in\mathbb{R}$. By Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii), the composite $\alpha\circ a$ is a map $\mathbb{N}\to\mathbb{R}$ with $(\alpha\circ a)(k)=\alpha(a_{k})=|a_{k}|$ for every $k\in\mathbb{N}$, as $a_{k}\in\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii); it is a sequence in $\mathbb{R}$ by Sequences (i).

Proof of (v). Take $I=\mathbb{N}$ in Pointwise Operations on Real-Valued Maps (i). The sequences $a$ and $b$ are maps $\mathbb{N}\to\mathbb{R}$, hence elements of $\mathbb{R}^{\mathbb{N}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i). By Pointwise Operations on Real-Valued Maps (i), $a+b$, $ab$, $ca$ and $-b$ are elements of $\mathbb{R}^{\mathbb{N}}$ with $(a+b)(k)=a_{k}+b_{k}$, $(ab)(k)=a_{k}b_{k}$, $(ca)(k)=c\,a_{k}$ and $(-b)(k)=-b_{k}$ for $k\in\mathbb{N}$, and the difference $a-b=a+(-b)$ satisfies $(a-b)(k)=a_{k}+(-b_{k})=a_{k}-b_{k}$ by Negatives, Differences, Reciprocals and Quotients (i). By Pointwise Operations on Real-Valued Maps (ii) there is $h\in\mathbb{R}^{\mathbb{N}}$ with $h(k)=c$ for every $k\in\mathbb{N}$. Each of these elements of $\mathbb{R}^{\mathbb{N}}$ is a map $\mathbb{N}\to\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), hence a sequence in $\mathbb{R}$ by Sequences (i), with the stated $k$-th terms.