ThmDex – An index of mathematical definitions, results, and conjectures.
Mean value theorem
Formulation 0
Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
(i) \begin{equation} a < b \end{equation}
(ii) $f : [a, b] \to \mathbb{R}$ is a D5231: Standard-continuous real function on $[a, b]$
(iii) $f$ is a D5614: Differentiable real function on $(a, b)$
Then \begin{equation} \exists \, x \in (a, b) : f'(x) = \frac{f(b) - f(a)}{b - a} \end{equation}
Proofs
Proof 0
Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
(i) \begin{equation} a < b \end{equation}
(ii) $f : [a, b] \to \mathbb{R}$ is a D5231: Standard-continuous real function on $[a, b]$
(iii) $f$ is a D5614: Differentiable real function on $(a, b)$
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$
Proof 1
Let $[a, b] \subseteq \mathbb{R}$ be a D544: Closed real interval such that
(i) \begin{equation} a < b \end{equation}
(ii) $f : [a, b] \to \mathbb{R}$ is a D5231: Standard-continuous real function on $[a, b]$
(iii) $f$ is a D5614: Differentiable real function on $(a, b)$
Consider a function $g : [a, b] \to \mathbb{R}$ defined by \begin{equation} g(x) : = f(x) - \frac{f(b) - f(a)}{b - a} (x - a) \end{equation} Now \begin{equation} g(a) = f(a) - \frac{f(b) - f(a)}{b - a} (a - a) = f(a) \end{equation} and \begin{equation} g(b) = f(b) - \frac{f(b) - f(a)}{b - a} (b - a) = f(b) - f(b) + f(a) = f(a) \end{equation} That is, $g(a) = g(b)$. Furthermore, $g$ is a sum of $f$ and a first-degree polynomial, whence results
(i) R2890: Basic real polynomial function is differentiable
(ii) R2891: Finite sum of differentiable functions is differentiable

guarantee that $g$ is differentiable on $(a, b)$. Result R1074: Rolle's theorem now guarantees that there exists $x \in (a, b)$ such that \begin{equation} 0 = g'(x) = f'(x) - \frac{f(b) - f(a)}{b - a} \end{equation} Adding $\frac{f(b) - f(a)}{b - a}$ to each side, we end up with \begin{equation} f'(x) = \frac{f(b) - f(a)}{b - a} \end{equation} This is exactly what was required to be shown. $\square$