Is the fundamental theorem of calculus independent of ZF? By the fundamental theorem of calculus I mean the following.
Theorem: Let $B$ be a Banach space and $f : [a, b] \to B$ be a continuously differentiable function (this means that we can write $f(x + h) = f(x) + h f'(x) + o(|h|)$ for some continuous function $f' : [a, b] \to B$). Then
$$\int_a^b f'(t) \, dt = f(b) - f(a).$$
(This integral can be defined in any reasonable way, e.g. one can use the Bochner integral or a Riemann sum.)
This theorem can be proven from Hahn-Banach, which allows you to reduce to the case $B = \mathbb{R}$. However, Hahn-Banach is independent of ZF.
Recently I tried to prove this theorem without Hahn-Banach and found that I couldn't do it. The standard proof in the case $B = \mathbb{R}$ relies on the mean value theorem, which is not applicable here. I can only prove it (I think) under stronger hypotheses, e.g. $f'$ continuously differentiable or Lipschitz.
So I am curious whether this theorem is even true in the absence of Hahn-Banach. It is likely that I am just missing some nice argument involving uniform continuity, but if I'm not, that would be good to know.
 A: Claim: Let $g:[a,b]\to B$ be differentiable, with $g'(t)=0$ for all $t\in[a,b]$.  Then $g(t)$ is a constant.
Proof: Fix $\epsilon>0$. For each $t\in[a,b]$, we can find $\delta_t>0$ such that $0<|h|<\delta_t\Rightarrow\|g(t+h)-g(t)\|<\epsilon|h|$.  The open intervals $(t-\delta_t,t+\delta_t)$ cover $[a,b]$, so there is a finite subcover $\{(t_i-\delta_{t_i},t_i+\delta_{t_i}):1\leq i\leq N\}$.  We may choose our labeling so that $t_1<t_2<\ldots<t_N$.  Now, we should be able to find points $x_0,\ldots,x_N$ with $x_0=a<t_1<x_1<t_2<\ldots<t_N<x_N=b$, satisfying $|x_i-t_i|<\delta_i$ and $|x_{i-1}-t_i|<\delta_i$ for $1\leq i\leq N$.  Now,
\begin{eqnarray*}
\|g(b)-g(a)\|&=&\left\|\sum_{i=1}^N(g(x_i)-g(t_{i}))-(g(t_i)-g(x_{i-1}))\right\|\\
&<&\sum_{i=1}^N \epsilon (x_i-t_i)+\epsilon(t_i-x_{i-1})\\
&=&\epsilon(b-a)
\end{eqnarray*}
Since $\epsilon$ is arbitrary, we have $g(b)=g(a)$.  This argument works on any subinterval, so $g(t)$ is constant.
We can apply the above with $g(x):=\int_a^xf'(t)\,dt-(f(x)-f(a))$.  I believe it can be checked directly that $g'(x)=0$ for all $x$, and that $g(a)=0$, so that $g(x)$ must be identically 0.
A: I believe that one of the standard proofs works.


*

*Let $F(x) := \intop_a^x f^\prime (t) dt$. Then $F$ is differentiable and its derivative is $f^\prime$ due to a standard estimate that has nothing to do with AC.

*$(F-f)^\prime = 0$, hence it is constant. This boils down to the one-dimensional case: just consider $g := \Vert F-f-F(a)+f(a) \Vert$. It is a real-valued function with zero derivative, and $g(a)=0$, so we can use the usual "one-dimensional" mean value theorem.
A: It seems that all suggestions above work under the assumption that $f$ is continuous and piece wise continuously differentiable in order to be able to use standard uniform continuity type arguments. Here is how it could be done under the assumption above:
It is enough to assume that $f'$ is also continuous, The strong measurability of $f'$ is straight forward and so is the integrability of $\|f'\|$. This in turn implies that $f'$ is integrable.
The sequence
$$f'_n(t)=\sum^{(2^n-1)\wedge b}_{k=(-2^n)\vee a}f'\big(\frac{k}{2^n}\big)\mathbb{1}_{\big(\frac{k}{2^n},\frac{k+1}{2^n}\big]}(t)$$
For instance can be use to approximate $f'$ over $[a,b]$ uniformly.
The slightly tricky part is to show $f(b)-f(a)=\int^b_a f'$. For this,
We observe that 
$$\frac{1}{h}\Big\|\int^{t+h}_{t}\big(f'(s)-f'(t)\big)\,ds\Big\|\leq \sup_{x,y\in[t,t+h]}\|f'(x)-f'(y)\|$$
Which can be made small for sufficiently small $h$ by the uniform continuity of $f'$ over $[a,b]$. Similar argument can be used for $[t-h,t]$. ALl this shows that $F:t\mapsto\int^t_af'(s)\,ds$ is differentiable and that  $F'(t)=f'(t)$. The conclusion then follows from the mean value theorem for Banach spaces:
$$\|F(b)-(f(b)-f(a))-F(a)\|\leq \sup_{a\leq x\leq b}\|F'(x)-f'(x)\||b-a|=0$$
More general situations, for instance, when all one assumes is that $f$ is absolutely continuous over $[a,b]$ and then get as consequence that 


*

*$f$ is differentiable almost everywhere,

*that $f'$ is integrable (a la Bochner),

*and that $f(b)-f(a)=\int^a_b f(t)\,dt$ 


would require additional assumptions on the Banach space $B$. For instance, that its dual $B^*$ is separable. The use of Hanh-Banach's theorem then would seem to be inevitable.
