Proof of Finite Sums of Reals: Congruence, the Product Map (x,y) ↦ f(x)h(y), and the Sequence of Diagonal Sums

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), so sums over every finite set, empty or not, are defined by Sums and Products over a Finite Set and over an Interval (i) and Sums and Products over a Finite Set and over an Interval (ii).

Proof of (i). By Sums and Products over a Finite Set and over an Interval (iii), $\sum_{x\in A}f(x)$ and $\sum_{x\in A}f'(x)$ are the sums over $A$ of the restrictions $f|_{A}$ and $f'|_{A}$. These are maps $A\to\mathbb{R}$ with $f|_{A}(x)=f(x)$ and $f'|_{A}(x)=f'(x)$ for $x\in A$, by Domains and Restrictions of Maps (ii) and Domains and Restrictions of Maps (iii). As $f(x)=f'(x)$ for every $x\in A$, $f|_{A}=f'|_{A}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv), so the two sums are the sum over $A$ of one and the same map, and are equal.

Proof of (ii). For $x\in A$ and $y\in B$, $f(x)\in\mathbb{R}$ and $h(y)\in\mathbb{R}$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), so $f(x)\,h(y)\in\mathbb{R}$, the multiplication $\cdot$ being a binary operation on $\mathbb{R}$ by Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (i). The expression $f(x)\,h(y)$ is built from the values of $f$ and $h$ and the value of the multiplication of $\mathbb{R}$, defined set symbols that are used properly for $x\in A$ and $y\in B$ and are eliminated as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x) and Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), the latter applying because $\cdot$ is a binary operation on the set $\mathbb{R}$. By Maps and Relations Given by Formulas (ii), with $\mathbb{R}$, $A$ and $B$ for its $b$, $c$ and $d$, there is exactly one map $m:A\times B\to\mathbb{R}$ with $m((x,y))=f(x)\,h(y)$, written $m(x,y)$ as in Sets and Maps: Ordinary Notation (v), for all $x\in A$ and $y\in B$.

Proof of (iii). Let $m:\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ be the map of (ii) for $A=B=\mathbb{N}$, $f=a$ and $h=b$, so $m(i,j)=a_{i}b_{j}$.

The index sets. Let $n\in\mathbb{N}$. By Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), $[n]=\{k\in\mathbb{N}:k\le n\}\subseteq\mathbb{N}$, so $[n]\times[n]\subseteq\mathbb{N}\times\mathbb{N}\subseteq\mathbb{N}_{0}\times\mathbb{N}_{0}$; $[n]$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (vii), and $[n]\times[n]$ is finite by Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite (iii). Let $+:\mathbb{N}_{0}\times\mathbb{N}_{0}\to\mathbb{N}_{0}$ be the addition of $\mathbb{N}_{0}$, a binary operation on $\mathbb{N}_{0}$ by The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv). Under the guard $x\in[n]\times[n]$, the variable $x$ is a term of type $\mathbb{N}_{0}\times\mathbb{N}_{0}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (i), so $+(x)$ is a term of type $\mathbb{N}_{0}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), and $n+1\in\mathbb{N}_{0}$ is a term of type $\mathbb{N}_{0}$ by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (ii). By Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (vii), $T_{n}=\{x\in[n]\times[n]:+(x)=n+1\}$ is a set, whose elements are the pairs $(i,j)$ with $i,j\in[n]$ and $i+j=n+1$; that is, $T_{n}=\{(i,j)\in[n]\times[n]:i+j=n+1\}$. As a subset of $[n]\times[n]$, $T_{n}$ is finite by Adding an Element to, Subsets of, and Unions and Cartesian Products of Finite Sets Are Finite (ii), and it is contained in $\mathbb{N}\times\mathbb{N}$, the domain of $m$. So $\sum_{(i,j)\in T_{n}}m(i,j)$, the sum displayed in the statement, is defined by Sums and Products over a Finite Set and over an Interval (iii), as the sum over $T_{n}$ of the restriction $m|_{T_{n}}$, a map $T_{n}\to\mathbb{R}$ by Domains and Restrictions of Maps (ii), and lies in $\mathbb{R}$ by Iterated Operations and Operations over Finite Sets Take Values in the Underlying Set (ii).

The sequence. The sums are now described by one formula, uniformly in $n$. Let $X$, $F$, $Y$, $R$ and $P$ be parameters with the values $\mathbb{R}$, the addition of $\mathbb{R}$, $\mathbb{N}$, the order $\le$ of $\mathbb{N}_{0}$ and the addition $+$ of $\mathbb{N}_{0}$, let $o$ and $g$ be parameters with the values $1$ and $m$, let $\gamma(n)$ be the formula $n\in Y$, and let

$$\begin{aligned} \theta_{1}(z,n)&:\ \forall x\,\bigl(x\in z\Leftrightarrow(x\in Y\wedge(x,n)\in R)\bigr),\\ \theta_{2}(D,z)&:\ \forall x\,\bigl(x\in D\Leftrightarrow\exists u\,\exists v\,(u\in z\wedge v\in z\wedge x=(u,v))\bigr),\\ \theta_{3}(T,D,n)&:\ \forall x\,\bigl(x\in T\Leftrightarrow(x\in D\wedge\exists s\,((x,s)\in P\wedge((n,o),s)\in P))\bigr). \end{aligned}$$

They 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 (iii), Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), 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 of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). Let $n\in\mathbb{N}$. Each $\theta_{i}$ has the form $\forall x\,(x\in z\Leftrightarrow\psi)$ in its first variable, so by extensionality at most one set satisfies it for given values of the others. The set $[n]$ satisfies $\theta_{1}(z,n)$ by Intervals of Natural Numbers: Initial Segments, Adding One Element, Splitting and Shifting (i), $k\le n$ meaning $(k,n)\in{\le}$; the set $[n]\times[n]$ satisfies $\theta_{2}(D,[n])$ by The Cartesian Product of Two Classes (i); and $T_{n}$ satisfies $\theta_{3}(T,[n]\times[n],n)$, since for $x\in[n]\times[n]\subseteq\mathbb{N}_{0}\times\mathbb{N}_{0}$ and every set $s$, $(x,s)\in{+}$ if and only if $+(x)=s$ by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), and $((n,1),s)\in{+}$ if and only if $s=n+1$ by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), as $n,1\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). Let $\mathrm{fop}$ be the formula of Iterated Operations over Finite Sets Are Given by a Predicative Formula (i), with the parameters $X$, $F$, $Y$, $R$ and $P$ above (the addition of $\mathbb{R}$ is associative and commutative with neutral element $0$, as recorded at the start), and let $\theta(w,n)$ be

$$\exists z\,\exists D\,\exists T\,\bigl(\theta_{1}(z,n)\wedge\theta_{2}(D,z)\wedge\theta_{3}(T,D,n)\wedge\mathrm{fop}(w,T,g)\bigr),$$

bound variables renamed apart and $T$ and $g$ put for $C$ and $g$ of $\mathrm{fop}$ as in Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i); it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), no quantifier being applied to a class variable. The renaming puts $g$ for a set variable of $\mathrm{fop}$, and it keeps the meaning because the value $m$ of $g$ is a set: $\mathbb{N}\times\mathbb{N}$ is a set by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii), so the map $m:\mathbb{N}\times\mathbb{N}\to\mathbb{R}$ is an element of $\mathbb{R}^{\mathbb{N}\times\mathbb{N}}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), and hence a set by Classes, Membership, Sets and Proper Classes (i). For $n\in\mathbb{N}$, the only sets $z$, $D$ and $T$ satisfying the first three conjuncts are $[n]$, $[n]\times[n]$ and $T_{n}$, so $\theta(w,n)$ holds if and only if $\mathrm{fop}(w,T_{n},m)$, that is, by Iterated Operations over Finite Sets Are Given by a Predicative Formula (i), $T_{n}$ being finite and $m$ a map from $\mathbb{N}\times\mathbb{N}\supseteq T_{n}$ to $\mathbb{R}$, if and only if $w=\sum_{(i,j)\in T_{n}}m(i,j)$. So for every set $n$ satisfying $\gamma$ exactly one set $w$ satisfies $\theta(w,n)$; with $\gamma$ and $\theta$ as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii) ($k=1$), $t(n)=\sum_{(i,j)\in T_{n}}m(i,j)$ is a defined set symbol used properly for $n\in\mathbb{N}$, eliminated as there. By Maps and Relations Given by Formulas (i), with $\mathbb{N}$ and $\mathbb{R}$ for its $a$ and $b$, there is a map $c:\mathbb{N}\to\mathbb{R}$ with $c(n)=t(n)$ for every $n\in\mathbb{N}$; it is a sequence in $\mathbb{R}$ by Sequences (i), with the stated terms.