Proof of Rolle's Theorem and the Mean Value Theorem on a Closed Interval

Order arithmetic is taken from Elementary Order Arithmetic in an Ordered Field (claim 1 strict compatibility with addition, claim 2 mixed transitivity, claim 6 $0<1$, claim 7 inverse of a positive element, claim 10 strict compatibility with multiplication by a positive element) and from Elementary Arithmetic in an Ordered Field (claim 3 translation), and the field axioms of the field $\mathbb{R}$ are used for rearrangement.

Midpoints. If $s<t$ then $m=\tfrac12\,(s+t)$ satisfies $s<m<t$: strict compatibility with addition gives $s+s<s+t$ and $s+t<t+t$, and multiplying by the positive element $\tfrac12$ together with $\tfrac12\,(s+s)=s$ and $\tfrac12\,(t+t)=t$ gives the two strict inequalities. In particular $(a,b)$ is nonempty.

Restriction to the open interval. Let $c\in(a,b)$ and let $g$ be the restriction of $f$ to $(a,b)$. By the midpoint remark applied to $a<c$ and to $c<b$ there are $u,v\in(a,b)$ with $u<c<v$, so $c$ is an interior point of the interval $(a,b)$. Moreover $g$ is differentiable at $c$ with $g'(c)=f'(c)$: taking $L=f'(c)$ and, for a given $\varepsilon$, the same $\delta$ as for $f$, every $h$ with $0<|h|<\delta$ and $c+h\in(a,b)$ also satisfies $c+h\in[a,b]$, and $g$ agrees with $f$ at $c$ and at $c+h$, so the required estimate holds; the value is $f'(c)$ by Uniqueness of the Derivative at an Interior Point.

Claim 1. By Extreme Value Theorem on a Closed Interval there are $x_{\max},x_{\min}\in[a,b]$ with $f(x_{\min})\le f(x)\le f(x_{\max})$ for every $x\in[a,b]$.

Suppose first that $x_{\max}\in(a,b)$. Then $g$ has a local maximum at $x_{\max}$ relative to $(a,b)$: the choice $\delta=1$ is positive, and every $y\in(a,b)$ satisfies $g(y)=f(y)\le f(x_{\max})=g(x_{\max})$. Hence $g'(x_{\max})=0$ by Vanishing of the Derivative at an Interior Local Extremum, and $f'(x_{\max})=0$ by the restriction remark; take $c=x_{\max}$. If instead $x_{\min}\in(a,b)$, the same argument with a local minimum gives $f'(x_{\min})=0$.

Otherwise neither point lies in $(a,b)$. A point $x\in[a,b]$ with $x\ne a$ and $x\ne b$ satisfies $a<x<b$ and hence lies in $(a,b)$, so $x_{\max}$ and $x_{\min}$ each equal $a$ or $b$. Since $f(a)=f(b)$ this gives $f(x_{\max})=f(x_{\min})$, so every $x\in[a,b]$ satisfies $f(x_{\min})\le f(x)\le f(x_{\min})$ and therefore $f(x)=f(x_{\min})$ by antisymmetry of $\le$. Let $c=\tfrac12\,(a+b)$, which lies in $(a,b)$ by the midpoint remark. Then $g$ is constant, so it has a local maximum at $c$ relative to $(a,b)$, and Vanishing of the Derivative at an Interior Local Extremum with the restriction remark gives $f'(c)=0$.

Claim 2. Translating $a<b$ by $-a$ gives $0<b-a$, so $b-a\ne0$ and its inverse exists. Put

Let $\iota:[a,b]\to\mathbb{R}$ be given by $\iota(x)=x$; it is continuous on $[a,b]$, since for a given $\varepsilon$ the choice $\delta=\varepsilon$ satisfies $d_{\mathbb{R}}(\iota(x),\iota(x_0))=d_{\mathbb{R}}(x_0,x)<\varepsilon$ whenever $d_{\mathbb{R}}(x_0,x)<\delta$, using the symmetry axiom of Metric Space. Let $\phi:[a,b]\to\mathbb{R}$ be given by $\phi(x)=f(x)+(-\alpha)\,x$. By claims 4, 2 and 5 of Continuity of Sums and Products of Real-Valued Functions on a Metric Space, applied to the scalar multiple $(-\alpha)\iota$ and then to the sum, $\phi$ is continuous on $[a,b]$.

Let $c\in(a,b)$. The function $(-\alpha)\iota$ is differentiable at $c$ with derivative $-\alpha$: for every $h\ne0$ distributivity gives

so the condition of Derivative at an Interior Point holds with $L=-\alpha$ and $\delta=1$, the absolute value of $0$ being $0$ by Absolute Value in an Ordered Field. Claim 2 of Sum and Product Rules for One-Dimensional Derivatives and Continuity now shows that $\phi$ is differentiable at $c$ with

Finally

so $\phi(a)=\phi(b)$ by claim 3 of Additive Cancellation and Elementary Additive Identities in a Field. Claim 1, applied to $\phi$, therefore provides $c\in(a,b)$ with $\phi'(c)=0$, that is $f'(c)+(-\alpha)=0$, whence $f'(c)=\alpha$ by claim 1 of Additive Cancellation and Elementary Additive Identities in a Field and claim 5 of that lemma. Multiplying by $b-a$ gives $f'(c)\,(b-a)=\alpha\,(b-a)=f(b)-f(a)$.