ThmDex – An index of mathematical definitions, results, and conjectures.
Rolle's 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)$
(iv) \begin{equation} f(a) = f(b) \end{equation}
Then \begin{equation} \exists \, x \in (a, b) : f'(x) = 0 \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)$
(iv) \begin{equation} f(a) = f(b) \end{equation}
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$