Proof of Kit for def:series-nbg

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), and the given $x_{0},\dots,x_{n-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{6}$ are distinct also when $n<7$. The parameters are those of the statement, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); in formulas, $\alpha$ denotes the addition of $\mathbb{R}$, $\beta$ the addition of $\mathbb{N}_{0}$, and $e$ the element $1$ of $\mathbb{N}$. Facts about natural numbers and maps carried by Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity are used without comment, as are the facts that $\mathbb{R}$ and the element $1$ of $\mathbb{N}$ are sets and so are the elements of every class (The Real Numbers (i), Classes, Membership, Sets and Proper Classes (i)), and that the one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)).

Sequences in $\mathbb{R}$. Kit for def:sequence-nbg (i), for two variables and the positions $0$ and $1$, gives a predicative formula in $x_{0},x_{1}$ expressing that $x_{0}$ is a sequence in $x_{1}$. By Renaming and Substituting Variables in Predicative Formulas (iii), with $\tau_{0}=x_{0}$ and $\tau_{1}=\mathbb{R}$, it yields a predicative formula $\eta(x_{0})$ in $x_{0}$ that holds exactly when $x_{0}$ is a sequence in $\mathbb{R}$, that is, a map $\mathbb{N}\to\mathbb{R}$ (Sequences (i)). By Renaming and Substituting Variables in Predicative Formulas (i), $\eta(x_{m})$ is, for every $m$, a predicative formula that holds exactly when $x_{m}$ is a sequence in $\mathbb{R}$.

Two reading rules. (a) For a map $g:\mathbb{N}\to\mathbb{R}$ and all sets $w$ and $u$: $(w,u)\in g$ if and only if $w\in\mathbb{N}$ and $u=g(w)$, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (x); and then $u\in\mathbb{R}$. (b) For $r\in\mathbb{N}$ and every set $q$: $((r,1),q)\in\beta$ if and only if $q=r+1$; and for $u,b\in\mathbb{R}$ and every set $v$: $((u,b),v)\in\alpha$ if and only if $v=u+b$. Both are Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), for the binary operation $+$ on $\mathbb{N}_{0}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv)), with $\mathbb{N}\subseteq\mathbb{N}_{0}$, and for the binary operation $+$ on $\mathbb{R}$ (The Real Numbers (iii)).

The recursion formula. 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) 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 (iv), each formula $(t_{1},t_{2})\in t_{3}$ and $((t_{1},t_{2}),t_{3})\in t_{4}$ written here and in $\lambda$ below is predicative and, when sets are assigned to the variables inside the pairs, holds if and only if the corresponding membership of ordered pairs holds. Let

$$\pi(x_{0},x_{1})=\eta(x_{0})\wedge\eta(x_{1})\wedge\exists x_{2}\,\bigl((e,x_{2})\in x_{0}\wedge(e,x_{2})\in x_{1}\bigr)\wedge\forall x_{2}\,\forall x_{3}\,\forall x_{4}\,\forall x_{5}\,\forall x_{6}\,\bigl(\chi\Rightarrow(x_{3},x_{6})\in x_{1}\bigr),$$ $$\chi=(x_{2},x_{4})\in x_{1}\wedge((x_{2},e),x_{3})\in\beta\wedge(x_{3},x_{5})\in x_{0}\wedge((x_{4},x_{5}),x_{6})\in\alpha.$$

Its parts are predicative and the rest adds only connectives and quantifiers over set variables; so $\pi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), and its free variables are $x_{0}$, $x_{1}$ and parameters.

Assign sets $a$ and $s$ to $x_{0}$ and $x_{1}$, and let them be sequences in $\mathbb{R}$. By (a), the third conjunct of $\pi$ holds if and only if $s(1)=a(1)$. Read conjunct by conjunct with (a) and (b), $\chi$ says that $x_{2}\in\mathbb{N}$, $x_{4}=s(x_{2})$, $x_{3}=x_{2}+1$, $x_{5}=a(x_{3})$ and $x_{6}=x_{4}+x_{5}$; so, by (a) once more, the last conjunct of $\pi$ reads

$$s(r+1)=s(r)+a(r+1)\qquad\text{for every }r\in\mathbb{N}.$$

Hence, under every assignment of sets to $x_{0}$ and $x_{1}$, $\pi(x_{0},x_{1})$ holds if and only if $x_{0}$ and $x_{1}$ are sequences in $\mathbb{R}$ with $x_{1}(1)=x_{0}(1)$ and $x_{1}(r+1)=x_{1}(r)+x_{0}(r+1)$ for every $r\in\mathbb{N}$.

Partial sums and the recursion. Let $a$ and $s$ be sequences in $\mathbb{R}$. Then $a$ is a sequence in $\mathbb{R}$ also in the earlier sense, with the same terms (The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i)), so Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (i) gives its sequence of partial sums in the earlier sense, a sequence $p$ in $\mathbb{R}$ with $p(1)=a(1)$ and $p(r+1)=p(r)+a(r+1)$ for every $r\in\mathbb{N}$. By The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i) and The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (v), $p$ is a sequence in $\mathbb{R}$ and the sequence of partial sums of $a$ in the sense of Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (i); so $s$ is the sequence of partial sums of $a$ if and only if $s(m)=p(m)$ for every $m\in\mathbb{N}$, as a map is determined by its values. If so, $s(1)=p(1)=a(1)$ and $s(r+1)=p(r+1)=p(r)+a(r+1)=s(r)+a(r+1)$ for $r\in\mathbb{N}$. Conversely, let $s(1)=a(1)$ and $s(r+1)=s(r)+a(r+1)$ for every $r\in\mathbb{N}$. Apply Composite Maps into Classes, Images of Singletons, and Agreement of Maps by Induction (iii) with $\mathbb{N}$ as its classes $A$, $B$ and $T$, $\mathbb{R}$ as its $X$ and $Y$, and $s$ and $p$ as its maps $S$ and $M$. As $0\notin\mathbb{N}$, its first hypothesis holds vacuously. For its second, let $k\in\mathbb{N}_{0}$ with $s(k)=p(k)$ if $k\in\mathbb{N}$: if $k=0$, then $k+1=1$ and $s(1)=a(1)=p(1)$; otherwise $k\in\mathbb{N}$ and $s(k+1)=s(k)+a(k+1)=p(k)+a(k+1)=p(k+1)$. So $s(m)=p(m)$ for every $m\in\mathbb{N}$. Hence $\pi(x_{0},x_{1})$ holds if and only if $x_{0}$ and $x_{1}$ are sequences in $\mathbb{R}$ and $x_{1}$ is the sequence of partial sums of $x_{0}$; so $\pi$ is a predicative formula in $x_{0},x_{1}$ in the sense of Renaming and Substituting Variables in Predicative Formulas. In particular, for a sequence $a$ in $\mathbb{R}$, the sets $s$ for which $\pi(a,s)$ holds are exactly the one set $p$ above.

Partial sums at any positions. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=2$, $\sigma(0)=i$ and $\sigma(1)=j$, the formula $\pi(x_{i},x_{j})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds exactly when $x_{i}$ and $x_{j}$ are sequences in $\mathbb{R}$ and $x_{j}$ is the sequence of partial sums of $x_{i}$. This proves (i).

Absolute values. Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (iii), for two variables with its $i=0$ and $k=1$, gives a predicative formula in $x_{0},x_{1}$ expressing "$x_{0}\in\mathbb{R}$ and $x_{1}=|x_{0}|$", whose parameters are among those of the statement; by Renaming and Substituting Variables in Predicative Formulas (i) with $\sigma(0)=2$ and $\sigma(1)=3$, it yields a predicative formula $\theta(x_{2},x_{3})$ that holds exactly when $x_{2}\in\mathbb{R}$ and $x_{3}=|x_{2}|$. Let

$$\lambda(x_{0},x_{1})=\eta(x_{0})\wedge\eta(x_{1})\wedge\forall x_{2}\,\forall x_{3}\,\forall x_{4}\,\bigl(((x_{4},x_{2})\in x_{0}\wedge(x_{4},x_{3})\in x_{1})\Rightarrow\theta(x_{2},x_{3})\bigr),$$

predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). Assign sequences $a$ and $b$ in $\mathbb{R}$ to $x_{0}$ and $x_{1}$. If the last conjunct holds and $k\in\mathbb{N}$, take $a(k)$, $b(k)$ and $k$ for $x_{2}$, $x_{3}$ and $x_{4}$: the hypotheses hold by (a), so $b(k)=|a(k)|$. Conversely, if $b(k)=|a(k)|$ for every $k\in\mathbb{N}$ and sets $u$, $v$ and $w$ assigned to $x_{2}$, $x_{3}$ and $x_{4}$ satisfy the hypotheses, then $w\in\mathbb{N}$, $u=a(w)\in\mathbb{R}$ and $v=b(w)=|u|$ by (a), so $\theta(u,v)$ holds. Hence $\lambda(x_{0},x_{1})$ holds if and only if $x_{0}$ and $x_{1}$ are sequences in $\mathbb{R}$ and $x_{1}(k)=|x_{0}(k)|$ for every $k\in\mathbb{N}$. By Renaming and Substituting Variables in Predicative Formulas (i) for two variables, with $\sigma(0)=i$ and $\sigma(1)=j$, $\lambda(x_{i},x_{j})$ expresses the condition of (ii), which is proved. For a sequence $a$ in $\mathbb{R}$, there is a sequence in $\mathbb{R}$ with $k$-th term $|a(k)|$ for every $k\in\mathbb{N}$ (Sequences of Real Numbers Built from Given Ones: Partial Sums, Index Shifts, Predecessor Reindexing, Absolute Values and Termwise Operations (iv), transferred between the earlier and the new sense of sequences by The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i)), and it is the only set $b$ for which $\lambda(a,b)$ holds, as a map is determined by its values.

Convergent series. Kit for def:convergent-sequence-nbg (ii), for two variables and the position $1$, gives a predicative formula $\gamma(x_{1})$ that holds exactly when $x_{1}$ is a convergent sequence in $\mathbb{R}$. Let

$$\kappa(x_{0})=\exists x_{1}\,\bigl(\pi(x_{0},x_{1})\wedge\gamma(x_{1})\bigr),$$

predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i), with $x_{0}$ as its only free variable other than parameters. For a set $a$, $\kappa(a)$ holds if and only if there is a set $s$ such that $a$ and $s$ are sequences in $\mathbb{R}$, $s$ is the sequence of partial sums of $a$, and $s$ is convergent. By the last sentence of the paragraph on partial sums and the recursion, this says that $a$ is a sequence in $\mathbb{R}$ whose sequence of partial sums is convergent, that is, by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii), a sequence in $\mathbb{R}$ whose series converges. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, $\kappa(x_{i})$ expresses the condition of (iii), which is proved.

Divergent series. Let $\delta(x_{0})=\eta(x_{0})\wedge\neg\kappa(x_{0})$, predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). For a set $a$, it holds if and only if $a$ is a sequence in $\mathbb{R}$ and it is not the case that $a$ is a sequence in $\mathbb{R}$ whose series converges, that is, if and only if $a$ is a sequence in $\mathbb{R}$ whose series does not converge, which by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii) means that its series diverges. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, $\delta(x_{i})$ expresses the condition of (iv), which is proved.

Absolutely convergent series. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=1$, $\kappa(x_{1})$ holds exactly when $x_{1}$ is a sequence in $\mathbb{R}$ whose series converges. Let

$$\varepsilon(x_{0})=\exists x_{1}\,\bigl(\lambda(x_{0},x_{1})\wedge\kappa(x_{1})\bigr),$$

predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). For a set $a$, $\varepsilon(a)$ holds if and only if there is a set $b$ such that $a$ and $b$ are sequences in $\mathbb{R}$, $b(k)=|a(k)|$ for every $k\in\mathbb{N}$, and the series of $b$ converges. By the last sentence of the paragraph on absolute values, this says that $a$ is a sequence in $\mathbb{R}$ and the series $\sum_{k=1}^{\infty}|a(k)|$ converges, that is, by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (iii), that $a$ is a sequence in $\mathbb{R}$ whose series converges absolutely. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, $\varepsilon(x_{i})$ expresses the condition of (v), which is proved.

The classes. The Class Comprehension Theorem for Predicative Formulas (i), applied to the predicative formulas $\kappa(x_{0})$, $\delta(x_{0})$ and $\varepsilon(x_{0})$ in $x_{0}$ (the case $n=1$, $i=0$ above), each with $x_{0}$ as its single variable and the parameters of the statement as its parameters, gives classes whose set elements are exactly the sequences in $\mathbb{R}$ whose series converges, diverges, respectively converges absolutely, and since every element of a class and every sequence in $\mathbb{R}$ is a set (a sequence in $\mathbb{R}$, a map $\mathbb{N}\to\mathbb{R}$, lies in the class $\mathbb{R}^{\mathbb{N}}$ of functions from $\mathbb{N}$ to $\mathbb{R}$, The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)), these classes serve as the $C$ of (vi), the $D$ of (vii) and the $A$ of (viii).