Proof of Kit for def:derivative-real-interval

Routine facts about real numbers are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (vi)). Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated, 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_{3}$ are distinct also when $N<4$. The parameters $\mathbb{R}$, $+$, $\cdot$, $0$, $1$, $\le$ and $<$ are variables other than $x_{0},x_{1},\dots$ and other than the bound variables below, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); $\mathbb{R}$ and its elements $0$ and $1$ are sets. Pair memberships such as $(t,a)\in f$ are the formulas of 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 for set variables $p$ and $p'$, $p\le p'$ and $p<p'$ stand for the pair memberships $(p,p')\in{\le}$ and $(p,p')\in{<}$. The letters $\varepsilon,\delta,t,a,b,c,e,n,q,r,s,y,z$ denote further set variables, distinct from one another, from $x_{0},x_{1},\dots$ and from the parameters.

Arithmetic formulas. By Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (i) and Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (ii), with its number of variables equal to $3$ and $i=0$, $j=1$ and $k=2$, and by Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (iii), with its number of variables equal to $2$, $i=0$ and $k=1$, there are predicative formulas, with parameters among $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$, expressing "$x_{0},x_{1}\in\mathbb{R}$ and $x_{2}=x_{0}-x_{1}$", "$x_{0},x_{1}\in\mathbb{R}$, $x_{1}\neq0$ and $x_{2}=x_{0}/x_{1}$" and "$x_{0}\in\mathbb{R}$ and $x_{1}=|x_{0}|$". For set variables $p$, $p'$ and $p''$ write $D(p,p',p'')$, $Q(p,p',p'')$ and $V(p,p'')$ for these formulas with $p$, $p'$ and $p''$ put for $x_{0}$, $x_{1}$ and $x_{2}$, respectively $p$ and $p''$ for $x_{0}$ and $x_{1}$. 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 (i) they are predicative, and for sets $p$, $p'$ and $p''$: $D(p,p',p'')$ holds if and only if $p,p'\in\mathbb{R}$ and $p''=p-p'$; $Q(p,p',p'')$ holds if and only if $p,p'\in\mathbb{R}$, $p'\neq0$ and $p''=p/p'$; and $V(p,p'')$ holds if and only if $p\in\mathbb{R}$ and $p''=|p|$.

The formulas. Write $I$ and $f$ for $x_{0}$ and $x_{1}$. Let

$$\theta=\forall a\,(a\in I\Rightarrow a\in\mathbb{R})\wedge\forall a\,\forall b\,\forall c\,\bigl((a\in I\wedge c\in I\wedge b\in\mathbb{R}\wedge a\le b\wedge b\le c)\Rightarrow b\in I\bigr)\wedge\exists a\,\exists b\,(a\in I\wedge b\in I\wedge\neg\,a=b),$$

and let $\mu_{f}$ and $\mu_{g}$ be the formula $\mu(F,A,B)$ of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii) with $x_{1}$, $x_{0}$ and $\mathbb{R}$, respectively $x_{2}$, $x_{0}$ and $\mathbb{R}$, as its $F$, $A$ and $B$, its auxiliary set variables chosen pairwise distinct and distinct from $x_{0},x_{1},\dots$, from the letters above and from the parameters. For distinct set variables $v$ and $w$ among $x_{2}$, $x_{3}$, $y$ and $z$ let

$$\beta(v,t,\delta)=t\in I\wedge\exists e\,\exists n\,\bigl(D(t,v,e)\wedge V(e,n)\wedge0<n\wedge n<\delta\bigr),$$ $$\lambda(v,w,t,\varepsilon)=\exists a\,\exists b\,\exists c\,\exists e\,\exists q\,\exists r\,\exists s\,\bigl((t,a)\in f\wedge(v,b)\in f\wedge D(a,b,c)\wedge D(t,v,e)\wedge Q(c,e,q)\wedge D(q,w,r)\wedge V(r,s)\wedge s<\varepsilon\bigr),$$ $$\kappa(v,w)=\forall\varepsilon\,\Bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists\delta\,\bigl(\delta\in\mathbb{R}\wedge0<\delta\wedge\forall t\,(\beta(v,t,\delta)\Rightarrow\lambda(v,w,t,\varepsilon))\bigr)\Bigr),$$

and let $\chi(v)=\theta\wedge\mu_{f}\wedge v\in I$. Writing $S$ and $g$ for $x_{2}$ where they occur, let

$$\varphi_{1}=\chi(x_{2}),\qquad\varphi_{2}=\chi(x_{2})\wedge x_{3}\in\mathbb{R}\wedge\kappa(x_{2},x_{3}),\qquad\varphi_{3}=\chi(x_{2})\wedge\exists z\,\bigl(z\in\mathbb{R}\wedge\kappa(x_{2},z)\bigr),$$ $$\varphi_{4}=\theta\wedge\mu_{f}\wedge\forall y\,(y\in S\Rightarrow y\in I)\wedge\forall y\,\bigl(y\in S\Rightarrow\exists z\,(z\in\mathbb{R}\wedge\kappa(y,z))\bigr),$$ $$\varphi_{5}=\theta\wedge\mu_{f}\wedge\mu_{g}\wedge\forall y\,\bigl(y\in I\Rightarrow\exists z\,((y,z)\in g\wedge\kappa(y,z))\bigr).$$

The formulas $\mu_{f}$, $\mu_{g}$ (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii)), the pair memberships (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 $D$, $Q$ and $V$ are predicative, so they contain no quantifier over a class variable, and every other quantifier above is over a set variable. So no quantifier of $\varphi_{1},\dots,\varphi_{5}$ is applied to a class variable, and they are predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i). The free variables of $\kappa(v,w)$ are among $x_{0}$, $x_{1}$, $v$, $w$ and the parameters; so those of $\varphi_{2}$ are among $x_{0},\dots,x_{3}$ and the parameters, and those of $\varphi_{1}$, $\varphi_{3}$, $\varphi_{4}$ and $\varphi_{5}$ among $x_{0}$, $x_{1}$, $x_{2}$ and the parameters.

What $\theta$ says. Let a set $I$ be assigned to $x_{0}$. The first conjunct of $\theta$ says that $I\subseteq\mathbb{R}$ (Subclasses and Subsets (i)). When it holds, the elements $a$ and $c$ of $I$ in the second conjunct are real numbers, so the second conjunct says that $b\in I$ for all $a,b,c\in\mathbb{R}$ with $a,c\in I$ and $a\le b\le c$, that is, by Intervals of the Real Line (i), that $I$ is an interval; and the third says that $I$ contains two distinct points. So $\theta$ holds if and only if $I$ is an interval containing two distinct points.

What $\kappa$ says. Let sets $I$, $f$, $x$ and $L$ be assigned to $x_{0}$, $x_{1}$, $v$ and $w$, where $I$ is an interval containing two distinct points, $f$ is a map $f:I\to\mathbb{R}$, $x\in I$ and $L\in\mathbb{R}$. Let $\delta,\varepsilon\in\mathbb{R}$ and let $t$ be a set.

First, $\beta(v,t,\delta)$ holds if and only if $t\in I$ and $0<|t-x|<\delta$: for $t\in I$, $t$ and $x$ are real numbers, so $D(t,v,e)$ holds exactly for $e=t-x$, and then $V(e,n)$ exactly for $n=|t-x|$.

Second, let $t\in I$ with $0<|t-x|$. Then $t-x\neq0$, as $|0|=0$. By Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), $(t,a)\in f$ holds exactly for $a=f(t)$ and $(x,b)\in f$ exactly for $b=f(x)$, and these are real numbers. So, by the meanings of $D$, $Q$ and $V$, the conjuncts of $\lambda(v,w,t,\varepsilon)$ before $s<\varepsilon$ hold exactly for $a=f(t)$, $b=f(x)$, $c=f(t)-f(x)$, $e=t-x$, $q=c/e$, $r=q-L$ and $s=|r|$, and $\lambda(v,w,t,\varepsilon)$ holds if and only if

$$\Bigl|\frac{f(t)-f(x)}{t-x}-L\Bigr|<\varepsilon .$$

Hence $\kappa(v,w)$ holds if and only if for every real $\varepsilon>0$ there is a real $\delta>0$ such that every $t\in I$ with $0<|t-x|<\delta$ satisfies this inequality, that is, by Derivative of a Real Function on an Interval (i), if and only if $L$ is a derivative of $f$ at $x$.

The standing hypotheses, and derivatives and differentiability at a point. Let sets $I$, $f$, $x$ and $L$ be assigned to $x_{0},\dots,x_{3}$. By the meaning of $\theta$ and 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 (vii), $\chi(x_{2})$ holds if and only if $I$ is an interval containing two distinct points, $f$ is a map $f:I\to\mathbb{R}$ and $x\in I$. So $\varphi_{1}$ is a predicative formula in $x_{0},x_{1},x_{2}$, in the sense of Renaming and Substituting Variables in Predicative Formulas, expressing the condition of (i) with $I=x_{0}$, $f=x_{1}$ and $u=x_{2}$. If $\chi(x_{2})$ fails, then $\varphi_{2}$ and $\varphi_{3}$ fail, and so do the conditions of (ii) and (iii). If $\chi(x_{2})$ holds, then, by the meaning of $\kappa$, $x_{3}\in\mathbb{R}\wedge\kappa(x_{2},x_{3})$ holds exactly when $L\in\mathbb{R}$ and $L$ is a derivative of $f$ at $x$; and $\exists z\,(z\in\mathbb{R}\wedge\kappa(x_{2},z))$ holds exactly when some real number is a derivative of $f$ at $x$, that is, as a derivative is a real number (Derivative of a Real Function on an Interval (i)), when $f$ is differentiable at $x$ (Derivative of a Real Function on an Interval (ii)). So $\varphi_{2}$ is a predicative formula in $x_{0},\dots,x_{3}$ expressing the condition of (ii) with $I=x_{0}$, $f=x_{1}$, $x=x_{2}$ and $L=x_{3}$, and $\varphi_{3}$ one in $x_{0},x_{1},x_{2}$ expressing the condition of (iii) with $I=x_{0}$, $f=x_{1}$ and $x=x_{2}$.

Differentiability on a subset. Let sets $I$, $f$ and $S$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. The first three conjuncts of $\varphi_{4}$ hold exactly when $I$ is an interval containing two distinct points, $f:I\to\mathbb{R}$ and $S\subseteq I$ (Subclasses and Subsets (i)); if one of them fails, $\varphi_{4}$ fails and so does the condition of (iv). If they hold, then for every $y\in S$ we have $y\in I$, so by the previous paragraph, with $y$ in place of $x$, $\exists z\,(z\in\mathbb{R}\wedge\kappa(y,z))$ holds exactly when $f$ is differentiable at $y$. So the last conjunct says that $f$ is differentiable at every point of $S$, that is, differentiable on $S$ (Derivative of a Real Function on an Interval (iii)). Hence $\varphi_{4}$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing the condition of (iv) with $I=x_{0}$, $f=x_{1}$ and $S=x_{2}$.

The derivative map. Let sets $I$, $f$ and $g$ be assigned to $x_{0}$, $x_{1}$ and $x_{2}$. If one of $\theta$, $\mu_{f}$ and $\mu_{g}$ fails, then $\varphi_{5}$ fails, and so does the condition of (vi), which requires $I$ to be an interval containing two distinct points and $f$ and $g$ to be maps from $I$ to $\mathbb{R}$. Let them hold. For $y\in I$, $(y,z)\in g$ holds exactly for $z=g(y)$, a real number (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii)), so by the meaning of $\kappa$ the last conjunct of $\varphi_{5}$ says that $g(y)$ is a derivative of $f$ at $y$ for every $y\in I$. If it holds, then $f$ is differentiable at every point of $I$, that is, differentiable (Derivative of a Real Function on an Interval (iii)), and $g(y)=f'(y)$ for every $y\in I$, since $g(y)$ and $f'(y)$ are both derivatives of $f$ at $y$ (Derivative of a Real Function on an Interval (ii)). Conversely, if $f$ is differentiable and $g(y)=f'(y)$ for every $y\in I$, then each $g(y)$ is a derivative of $f$ at $y$ (Derivative of a Real Function on an Interval (ii)). Finally, for differentiable $f$ the derivative $f'$ is a map $f':I\to\mathbb{R}$ with value $f'(u)$ at every $u\in I$ (Derivative of a Real Function on an Interval (iv)), and a map $g:I\to\mathbb{R}$ with $g(u)=f'(u)$ for every $u\in I$ is equal to $f'$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)); so $g=f'$ if and only if $g$ is a map $g:I\to\mathbb{R}$ with $g(u)=f'(u)$ for every $u\in I$. Hence $\varphi_{5}$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing the condition of (vi) with $I=x_{0}$, $f=x_{1}$ and $g=x_{2}$.

Renaming to arbitrary positions. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$ and $\sigma(0)=i$, $\sigma(1)=j$ and $\sigma(2)=k$, the formula $\varphi_{1}(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{N-1}$, exactly when the condition of (i) holds for $I=x_{i}$, $f=x_{j}$ and $u=x_{k}$. This proves (i). In the same way $\varphi_{3}(x_{i},x_{j},x_{k})$, $\varphi_{4}(x_{i},x_{j},x_{k})$ and $\varphi_{5}(x_{i},x_{j},x_{k})$ prove (iii), (iv) and (vi), and, with the number of variables equal to $4$ and moreover $\sigma(3)=l$, $\varphi_{2}(x_{i},x_{j},x_{k},x_{l})$ proves (ii). Finally, with the number of variables equal to $3$ and $\sigma(0)=i$, $\sigma(1)=j$ and $\sigma(2)=i$, the formula $\varphi_{4}(x_{i},x_{j},x_{i})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing the condition of (iv) with $S=I$. As $I\subseteq I$ always, and differentiability on $I$ is differentiability (Derivative of a Real Function on an Interval (iii)), this is the condition of (v), which is therefore predicative.

The class of maps differentiable at a point. Let $I$ be an interval containing two distinct points and let $x\in I$. Then $I$ is a set, being a subclass of the set $\mathbb{R}$ (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)), and $x$ is a set, being an element of a class (Classes, Membership, Sets and Proper Classes (i)). Apply The Class Comprehension Theorem for Predicative Formulas (i) to $\varphi_{3}$ with its abbreviations eliminated, with $x_{1}$ as its single variable and $x_{0}$, $x_{2}$, $\mathbb{R}$, $+$, $\cdot$, $0$, $1$, $\le$ and $<$ as its parameters, $x_{0}$ and $x_{2}$ being assigned $I$ and $x$. It gives a class $C$ whose elements are exactly the sets $f$ for which $\varphi_{3}$ holds with $f$ assigned to $x_{1}$ (the one-entry tuple $\langle f\rangle$ is $f$ by The Ordered Pair of Two Sets and Nested Tuples (ii)), that is, as the hypotheses on $I$ and $x$ hold, the sets $f$ that are maps $f:I\to\mathbb{R}$ differentiable at $x$. Every element of $C$ is a set (Classes, Membership, Sets and Proper Classes (i)), and every map $f:I\to\mathbb{R}$ is a set, as it lies in the class $\mathbb{R}^{I}$ of functions from $I$ to $\mathbb{R}$ by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), $I$ and $\mathbb{R}$ being sets. So for every class $f$, $f\in C$ if and only if $f$ is a map $f:I\to\mathbb{R}$ differentiable at $x$. This proves (vii).

The class of maps differentiable on a subset. Let $I$ be an interval containing two distinct points and let $S\subseteq I$; $I$ is a set as before, and $S$ is a set, being a subclass of the set $I$ (Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i)). The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi_{4}$ with its abbreviations eliminated, with $x_{1}$ as its single variable and $x_{0}$ and $x_{2}$ (assigned $I$ and $S$), $\mathbb{R}$, $+$, $\cdot$, $0$, $1$, $\le$ and $<$ as its parameters, gives a class $C$ whose elements are exactly the maps $f:I\to\mathbb{R}$ that are differentiable on $S$, which proves (viii) (bookkeeping as in the previous paragraph).

The class of differentiable maps. Let $I$ be an interval containing two distinct points. As $I\subseteq I$, (viii) with $S=I$ gives a class $C$ such that, for every class $f$, $f\in C$ if and only if $f:I\to\mathbb{R}$ is differentiable on $I$, that is, differentiable (Derivative of a Real Function on an Interval (iii)). This proves (ix).