ThmDex – An index of mathematical definitions, results, and conjectures.
Proof P2154 on R1073: Mean value theorem
P2154
Consider a function $g : [a, b] \to \mathbb{R}$ given by $g(x) = x - a$. Now $g(b) = b - a$ and $g(a) = a - a = 0$. Since $g$ is a first-degree polynomial, results
(1) R2923: Basic real polynomial function is continuous
(2) R2890: Basic real polynomial function is differentiable

state that $g$ is continuous on $[a, b]$ and differentiable on $(a, b)$ with the derivative $g'$ equal to $1$ everywhere on $(a, b)$.

Result R2875: Cauchy's real mean value theorem now guarantees that there exists $x \in (a, b)$ such that \begin{equation} f'(x) (b - a) = f'(x) (g(b) - g(a)) = g'(x) (f(a) - f(b)) = f(a) - f(b) \end{equation} Dividing both sides by the nonzero quantity $b - a$, we obtain \begin{equation} f'(x) = \frac{f(a) - f(b)}{b - a} \end{equation} This completes the proof. $\square$