Mean value theorem and the axiom of choice There's this theorem in Spivak's book of Calculus: 

Theorem 7
Suppose that $f$ is continuous at $a$, and that $f'(x)$ exists for all $x$ in some interval containing $a$, except perhaps for $x=a$. Suppose, moreover, that $\lim_{x \to a} f'(x)$ exists. Then $f'(a)$ also exists, and 
  $$f'(a) = \lim_{x \to a} f'(x)$$
Proof
By definition,
  $$f'(a) = \lim_{h \to 0} \frac{f(a+h)-f(a)}{h}$$
  For sufficiently small $h>0$ the function $f$ will be continuous on $[a,a+h]$ and differentiable on $(a,a+h)$ (a similar assertion holds for sufficiently small $h<0$). By the Mean Value Theorem there is a number $\alpha_h$ in $(a,a+h)$ such that
  $$\frac{f(a+h)-f(a)}{h} = f'(\alpha_h)$$
  Now $\alpha_h$ approaches $a$ as $h$ approaches $0$, because $\alpha_h$ is in $(a,a+h)$; since $\lim_{x \to a} f'(x)$ exists, it follows that
  $$f'(a) = \lim_{h \to 0} \frac{f(a+h)-f(a)}{h} = \lim_{h \to 0} f'(\alpha_h) = \lim_{x \to a} f'(x)$$
  (It is a good idea to supply a rigorous $\epsilon$-$\delta$ argument for this final step, which we have treated somewhat informally.) $\blacksquare$

Following the recommendation of supplying the details I had the question of $\alpha_h$ being a choice function. This is because for every $h$ there is the possibility of having a lot of points $c$ such that $f'(c)=\frac{f(a+h)-f(a)}{h}$. Then we choose one of them to have a function $\alpha_h$. I'm not sure though because I'm always struggling with the axiom of choice that I cannot distinguish if it's needed or not. Also maybe in this case what the author is saying is something different. Can you guys please help me?
 A: The Mean Value Theorem is a consequence of Rolle's Theorem, which says that if $f$ is continuous on $[a,b]$ and differentiable on $(a,b)$, and $f(a)=f(b)$, then there exists $c \in (a,b)$ such that $f'(c)=0$. This is proven by letting $c$ be a point where $f$ attains its global minimum or maximum on $(a,b)$; such a point must have $f'(c) = 0$.
To avoid having to make a choice here, you can specify $c$ uniquely as:
$$c = \sup\{x \in (a,b) | f \text{ attains its global minimum or maximum at } x\}$$
Then $f$ attains its global minimum or maximum at $c$, by continuity. (See [1] below for what to do if $c=b$.)
Armed with this version of Rolle's Theorem, you can use it to prove a similar non-choice version of the Mean Value Theorem. You can then use this theorem in your proof.

[1] It can happen that this supremum is equal to $b$, which we don't want. In this case:


*

*if $f(b)$ is a global minimum but not a global maximum, let $c = \sup\{x \in (a,b) | f \text{ attains its global maximum at } x\}$;

*if $f(b)$ is a global maximum but not a global minimum, let $c = \sup\{x \in (a,b) | f \text{ attains its global minimum at } x\}$;

*if $f(b)$ is both a global minimum and a global maximum, then $f$ is consant, so we can choose $c=\frac12(a+b)$.
A: Yes, this is an interesting technical point that is often overlooked. As written, Spivak is postulating the existence of the function that to each (positive, sufficiently small) $h$ assigns the value $\alpha_h$. On the face of it, this is an application of the axiom of choice, because the set of numbers $\tau$ between $a$ and $a+h$ such that $\displaystyle \frac{f(a+h)-f(a)}h=f'(\tau)$ does not need to be a singleton, or open, or closed, or any reasonably shaped set, so the problem of assigning to each such $h$ a specific such number $\tau$ requires infinitely many choices in what does not appear to be a straightforward definable manner.
One technical remark is that, using techniques of descriptive set theory, we can eliminate this use of choice since for $\eta>0$ small enough, the relation 
 $$\{(h,\tau):0<|h|<\eta\mbox{ and }\frac{f(a+h)-f(a)}h=f'(\tau)\}$$
is Borel, and therefore admits what we call a co-analytic uniformization, provably in Zermelo-Fraenkel set theory without the axiom of choice. (This means that we can actually prove, without choice, the existence of a function $a_h$ as in Spivak's argument.)
That said, both this statement and its proof are definitely beyond the level of Spivak's textbook. Fortunately, in order to formalize what he does, we can proceed in a more elementary manner: 
Let $L=\lim_{x\to a}f'(x)$, the limit whose existence is granted by assumption. For any $\epsilon>0$ there is a $\delta>0$ such that for any $\tau$, if $0\ne \tau$ and $|\tau|<\delta$, then $|f'(a+\tau)-L|<\epsilon$. It is enough to prove that 
 $$ \left|\frac{f(a+h)-f(a)}h - L\right|<\epsilon $$
for any $h$ with $0\ne h$ and $|h|<\delta$. Since $\epsilon$ is arbitrary, this indeed shows that $f'(a)$ exists and equals $L$. 
Now, given such an $h$, we know that there is a $\rho$ in the open interval with endpoints $a$ and $a+h$ such that $\displaystyle \frac{f(a+h)-f(a)}h=f'(\rho)$. There may in fact be many possible choices for $\rho$, but we do not need to choose any (that is, we do not need to assert the existence of the function $a_h$). Simply note that for any such $\rho$, we have $0<|\rho-a|<\delta$, and so indeed $$ \left|\frac{f(a+h)-f(a)}h - L\right|<\epsilon, $$ as needed.
A similar issue appears in (advanced) analysis, in the theory of the derivative, when studying Neugebauer's theorem that characterizes when a function is a derivative in terms of properties of a companion function playing the role of $a_h$ above. Without appealing to the descriptive set theoretic result mentioned above, Neugebauer's theorem appears to need more choice than the standard fragment usually assumed in analysis (dependent choices). I have not found any texts dealing with Neugebauer's theorem that address (or even appear aware of) this technicality.
A: I don't think $\alpha_h$ being a choice function has much to do with what the author is talking about. He is recommending the reader to try to prove that
$$
\lim_{h\to0}f'(\alpha_h) = \lim_{x\to a}f'(x)
$$
What the left side means is:
$$
\lim_{h\to0}f'(\alpha_h) = c \iff \forall\epsilon,\exists\delta>0\mid|h|<\delta \Rightarrow|f'(\alpha_h)-c|<\epsilon \tag{1}
$$
And the right side means:
$$
\lim_{x\to a}f'(x) = c \iff \forall\epsilon,\exists\delta>0\mid|x-a|<\delta \Rightarrow|f'(x)-c|<\epsilon \tag{2}
$$
You know that $(2)$ is true, so you have to prove that $(2)\Rightarrow (1)$.
First remember that $\alpha_h\in (a,a+h)$. So $0<\alpha_h-a<h$ and $|\alpha_h-a|<|h|$. Now just pick $x=\alpha_h$. You know that for any $\epsilon,h>0$, the following is true:
$$
\exists\delta>0\mid|\alpha_h-a|<\delta\Rightarrow|f'(\alpha_h)-c|<\epsilon \tag{3}
$$
You also know that $|h|<\delta\Rightarrow|\alpha_h-a|<\delta$. So it is also true that:
$$
\exists\delta>0\mid|h|<\delta\Rightarrow|\alpha_h-a|\Rightarrow|f'(\alpha_h)-c|<\epsilon \tag{4}
$$
Which shows that $(1)$ is true. Note that we arrived at the same limit $c$.
