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.
Best Answer
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.