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 at $x_0 \in (a, b)$
|
| (iv) |
One of the following statements is true
| (a) |
\begin{equation}
\exists \, r > 0 :
\forall \, x \in (x_0 - r, x_0 + r) :
f(x_0) \geq f(x)
\end{equation}
|
| (b) |
\begin{equation}
\exists \, r > 0 :
\forall \, x \in (x_0 - r, x_0 + r) :
f(x_0) \leq f(x)
\end{equation}
|
|
Without loss of generality, we may assume that $x_0$ is a local maximum for $f$.
Since $f$ is differentiable at $x_0$, then the limits
\begin{equation}
\lim_{x \nearrow x_0} \frac{f(x) - f(x_0)}{x - x_0}, \quad
\lim_{x \to x_0} \frac{f(x) - f(x_0)}{x - x_0}, \quad
\lim_{x \searrow x_0} \frac{f(x) - f(x_0)}{x - x_0}
\end{equation}
all exist and we have
\begin{equation}
\lim_{x \nearrow x_0} \frac{f(x) - f(x_0)}{x - x_0}
= \lim_{x \to x_0} \frac{f(x) - f(x_0)}{x - x_0}
= \lim_{x \searrow x_0} \frac{f(x) - f(x_0)}{x - x_0}
\end{equation}
Since $x_0$ is a local maximum for $f$, then for every $x \in (x_0 - r, x_0)$ we have
\begin{equation}
\frac{f(x) - f(x_0)}{x - x_0}
\geq 0
\end{equation}
By isotonicity of limits, we then we have
\begin{equation}
\lim_{x \to x_0} \frac{f(x) - f(x_0)}{x - x_0}
= \lim_{x \nearrow x_0} \frac{f(x) - f(x_0)}{x - x_0}
\geq 0
\end{equation}
Reasoning symmetrically, we deduce also that
\begin{equation}
\lim_{x \to x_0} \frac{f(x) - f(x_0)}{x - x_0}
= \lim_{x \searrow x_0} \frac{f(x) - f(x_0)}{x - x_0}
\leq 0
\end{equation}
Applying
R1043: Equality from two inequalities for real numbers, we can then conclude
\begin{equation}
f'(x_0)
= \lim_{x \to x_0} \frac{f(x) - f(x_0)}{x - x_0}
= 0
\end{equation}
$\square$
