Real function/Derivative zero/Constant/Fact/Proof

Proof

If ${}f$ is not constant, then there exists some ${}x<x'$ such that ${}f(x)\neq f(x')$. Then there exists, due to the mean value theorem, some ${}c$, ${}x<c<x'$, such that ${}f'(c)={\frac {f(x')-f(x)}{x'-x}}\neq 0$, which contradicts the assumption.

To fact