Proof of One-Dimensional Derivatives, Partial Derivatives, and Smoothness on the Real Line

Claim 1. The defining condition of Interval in the Real Line holds for $\mathbb{R}$ because every real number lies in $\mathbb{R}$, so $\mathbb{R}$ is an interval. Let $x\in\mathbb{R}$. By claim 6 of Elementary Order Arithmetic in an Ordered Field we have $0<1$, hence $-1<0$ by claim 4 of that lemma; adding $x$ to each of these, by claim 1 of that lemma, gives $x-1<x$ and $x<x+1$. Since $x-1$ and $x+1$ lie in $\mathbb{R}$, the point $x$ is an interior point of $\mathbb{R}$ by Interior Point of an Interval.

Claim 2. By claim 1 of Polynomial Functions on the Real Line are Smooth, $\mathbb{R}^{1}$ is an open subset of $\mathbb{R}^{1}$, so Slice Function and the Partial Derivative applies with $n=1$, $U=\mathbb{R}^{1}$, $a=x$ and $i=1$. In that situation the point written $a[s]$ there is $s$ itself, so the slice function of $f$ at $x$ in the first variable is the restriction $f|_{I}$ of $f$ to the interval

where $\rho\in\mathbb{R}$ with $0<\rho$ is an admissible radius as in claim 1 of that lemma, and $x$ is an interior point of $I$. Claim 2 of that lemma states that $\partial_{1}f(x)$ exists if and only if $f|_{I}$ is differentiable at $x$, and that the two values then agree.

It therefore suffices to show that $f$ is differentiable at $x$ with derivative $L$ if and only if $f|_{I}$ is differentiable at $x$ with derivative $L$.

Suppose first that $f$ is differentiable at $x$ with derivative $L$, and let $\varepsilon\in\mathbb{R}$ with $0<\varepsilon$. Take $\delta$ as in Derivative at an Interior Point for $f$ and $\varepsilon$. If $h\in\mathbb{R}$ satisfies $0<|h|<\delta$ and $x+h\in I$, then in particular $x+h\in\mathbb{R}$, so the required bound on the difference quotient holds. Hence $f|_{I}$ is differentiable at $x$ with derivative $L$.

Conversely, suppose that $f|_{I}$ is differentiable at $x$ with derivative $L$, and let $\varepsilon\in\mathbb{R}$ with $0<\varepsilon$. Take $\delta$ as in Derivative at an Interior Point for $f|_{I}$ and $\varepsilon$, and let $\delta'$ be the smaller of $\delta$ and $\rho$, which exists by claim 9 of Elementary Order Arithmetic in an Ordered Field and satisfies $0<\delta'$. If $h\in\mathbb{R}$ satisfies $0<|h|<\delta'$, then $|h|<\rho$, so $x-\rho<x+h<x+\rho$ by claim 6 of Properties of the Absolute Value in an Ordered Field and claim 1 of Elementary Order Arithmetic in an Ordered Field, whence $x+h\in I$; and $|h|<\delta$, so the required bound on the difference quotient holds. Hence $f$ is differentiable at $x$ with derivative $L$.

Claim 3. We first record that every $f\in D$ is continuous at every point of $\mathbb{R}^{1}$ in the Euclidean sense. Indeed, $f$ is differentiable at every point of $\mathbb{R}$, and $\mathbb{R}$ is an interval all of whose points are interior by claim 1, so Differentiability at an Interior Point Implies Continuity There shows that $f$ is continuous at every point of $\mathbb{R}$ as a map into the real line with the metric of The Absolute Value Metric on the Real Line; by claim 1 of Euclidean Continuity Agrees with Metric Continuity for Real-Valued Functions this is the same as continuity in the Euclidean sense at every point of $\mathbb{R}^{1}$.

Next, every $f\in D$ is of class $C^{1}$ on $\mathbb{R}^{1}$. Indeed, $f$ is continuous at every point of $\mathbb{R}^{1}$ by the previous paragraph; by claim 2 the partial derivative of $f$ with respect to the first variable exists at every point of $\mathbb{R}^{1}$ and the function $\partial_{1}f$ is the function $x\mapsto f'(x)$, which belongs to $D$ and is therefore also continuous at every point of $\mathbb{R}^{1}$. Since $\mathbb{R}^{1}$ is open in $\mathbb{R}^{1}$, clauses 1 and 3 of C^k Maps on a Euclidean Open Set give that $f$ is of class $C^{1}$ on $\mathbb{R}^{1}$.

Now let $E$ be the set of those natural numbers $k$ such that every $f\in D$ is of class $C^{k}$ on $\mathbb{R}^{1}$. By the previous paragraph, $1\in E$. Let $k\in E$ and let $f\in D$. Then $f$ is of class $C^{1}$ on $\mathbb{R}^{1}$, and $\partial_{1}f$ is the function $x\mapsto f'(x)$, which belongs to $D$ and hence is of class $C^{k}$ on $\mathbb{R}^{1}$ because $k\in E$. Since $k+1=S(k)$ for the successor map $S$ of Natural Numbers, by claim 1 of Arithmetic of Addition on the Natural Numbers, clause 2 of C^k Maps on a Euclidean Open Set gives that $f$ is of class $C^{S(k)}$ on $\mathbb{R}^{1}$. Hence $S(k)\in E$.

By Principle of Induction for the Natural Numbers, $E=\mathbb{N}$, so every $f\in D$ is of class $C^{k}$ on $\mathbb{R}^{1}$ for every natural number $k$, that is, smooth on $\mathbb{R}^{1}$ by Smooth Map on a Euclidean Open Set.