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$
