Proof of Uniqueness of the Derivative at an Interior Point

Order arithmetic is taken from Elementary Order Arithmetic in an Ordered Field (claim 2 mixed transitivity, claim 5 product of positive elements, claim 7 inverse of a positive element, claim 8 halving, claim 9 the least of two elements) and from Elementary Arithmetic in an Ordered Field (claim 3 translation), and claims 2 and 5 of Properties of the Absolute Value in an Ordered Field are used as symmetry and the triangle inequality for the absolute value.

Suppose $L\ne L'$. Then $L-L'\ne0$, so $0<|L-L'|$ by claim 1 of Properties of the Absolute Value in an Ordered Field together with claim 3 of Additive Cancellation and Elementary Additive Identities in a Field, which gives $L-L'=0$ only when $L=L'$. Put $\varepsilon=\tfrac12\,|L-L'|$, which satisfies $0<\varepsilon$ by halving, and note that $\varepsilon+\varepsilon=|L-L'|$.

Let $\delta_1$ and $\delta_2$ be as in the hypothesis for $L$ and for $L'$ with this $\varepsilon$, and let $\delta$ be the minimum of $\delta_1$ and $\delta_2$; by claims 1 and 2 of Elementary Properties of the Minimum of Two Elements, $\delta\le\delta_1$, $\delta\le\delta_2$, and $\delta$ equals $\delta_1$ or $\delta_2$, so $0<\delta$.

An admissible increment exists. Since $x_0$ is an interior point of $I$, there are $u,v\in I$ with $u<x_0<v$. Let $h$ be the minimum of $\tfrac12\,\delta$ and $v-x_0$; both are positive, the second because translating $x_0<v$ by $-x_0$ gives $0<v-x_0$, so $0<h$, and $h\le\tfrac12\,\delta<\delta$ by halving and mixed transitivity. From $h\le v-x_0$ and translation we get $x_0+h\le v$, and from $0<h$ we get $x_0<x_0+h$; since $x_0,v\in I$, order-convexity of $I$ gives $x_0+h\in I$. Finally $|h|=h$ because $0\le h$, so $0<|h|<\delta$.

Contradiction. Write $Q$ for the difference quotient $\bigl(f(x_0+h)-f(x_0)\bigr)/h$. Since $\delta\le\delta_1$ and $\delta\le\delta_2$, this $h$ is admissible for both hypotheses, so $|Q-L|<\varepsilon$ and $|Q-L'|<\varepsilon$. Using $L-L'=(L-Q)+(Q-L')$, the triangle inequality and symmetry,

Adding the two strict inequalities gives $|Q-L|+|Q-L'|<\varepsilon+\varepsilon=|L-L'|$, so mixed transitivity yields $|L-L'|<|L-L'|$, which is impossible.

Hence $L=L'$, and the value $f'(x_0)$ named in Derivative at an Interior Point is uniquely determined.