ThmDex – An index of mathematical definitions, results, and conjectures.
Proof P3195 on R1074: Rolle's theorem
P3195
If $f$ is a constant function, then $f'(x) = 0$ for every $x \in (a, b)$ trivially. Suppose therefore that $f$ is not a constant function.

Result R1070: Extreme value theorem for basic real calculus shows that $f$ attains a maximum value $M = f(x)$ at some $x \in [a, b]$ and a minimum value $m = f(y)$ at some $y \in [a, b]$. If $x \in \{ a, b \}$, then $f$ attains a (weakly) smaller value than $M$ at all points $t \in (a, b)$ and hence $y \in (a, b)$ since $f$ is not constant. Similarly, if $y \in \{ a, b \}$, then $f$ attains a (weakly) greater value than $m$ at all points $t \in (a, b)$ and hence $x \in (a, b)$ since $f$ is not constant. Hence, both $x$ and $y$ can not be in the set $\{ a, b \}$. Without loss of generality, we may assume that $x \in (a, b)$.

Result R1075: Basic real interior extremum theorem now states that $f'(x) = 0$. $\square$