Spectra of elements of a Banach algebra and the role played by the Hahn-Banach Theorem.

I do not believe that the Hahn-Banach theorem is necessary. At some point I had planned on writing up a blog post verifying this but I lost the motivation...

The idea is that you can prove Liouville's theorem in the Banach space setting directly without using Hahn-Banach to reduce to the case of $\mathbb{C}$ (I asked whether this was possible in this math.SE question). Most of the steps in the proof are exactly the same; the only one that isn't, as far as I can tell, is the fundamental theorem of calculus, which is usually proven using the mean value theorem but which can instead be proven following the answers to this math.SE question.

I think Hahn-Banach can be eliminated from the usual proof, but being a non-expert in set theory, I cannot guarantee that the proof is completely independent of the axiom of choice.

Here is a sketch of a basic calculus proof. A function $U\to B$ from a region $U\subset C$ to a Banach space $B$ is called analytic if every point has a neighborhood where it is represented by a convergent Taylor series. You can prove a weak form of Cauchy theorem which says that if a function is analytic in $| z | < R \leq \infty$ then its Taylor series has radius of convergence at least $R$. It seems that this does not use the axiom of choice. Then you prove that Cauchy inequalities hold (there is a simple algebraic proof of this, see my answer to Liouville's theorem with your bare hands), and derive the Liouville theorem for Banach-space-valued functions.

Then again it is an elementary fact that if $a-\lambda_0 1$ has has a bounded inverse then the resolvent is an analytic function (in the sense I defined above) in a neighborhood of $\lambda_0$. Then you show that if the resolvent exists everywhere then it tends to $0$ as $\lambda\to\infty$. Then it seems to me that you obtain a proof without Hahn-Banach by applying the Liouville theorem to the resolvent.

Sorry if I missed something...

EDIT. The weak form of Cauchy's theorem that I mentioned uses only elementary manipulation with absolutely convergent series, no integral is involved, see Liouville's theorem with your bare hands.

There is a proof without using even complex analysis, and at first glance without using AC. We replace Cauchy integral formula by clever finite sums. Namely, we define the spectral radius as $r(a):=\lim \|a^n\|^{1/n}$ (the limit exists by Fekete lemma), by scaling it suffices to consider two cases: $r(a)=0$ and $r(a)=1$. In the first case $a$ is not invertible, since if $ab=1$, then $a^nb^n=1$ and $\|a^n\|\cdot \|b\|^n\geqslant 1$, thus $r(a)\geqslant 1/\|b\|$. If $r=1$, we prove that there exist $\lambda$ on the unit circle such that $a-\lambda$ is not invertible. Assume the contrary, then by continuity of the inverse and compactness of the circle we get $\|(a-\lambda)^{-1}\|\leqslant M$ for all $\lambda$ on the unit circle and certain $M>0$. Now we use the rational functions identity $$n^2 a^{n-1}=(1-a^n)^2\sum_{w:w^n=1}w(a-w)^{-2}$$ and take the spectral radius of both right and left hand sides. By using the easy equalities and inequalities $r(u^n)=(r(u))^n$, $r(uv)\leqslant r(u)\cdot \|v\|$, $r(1+u)\leqslant 1+r(u)$ for commuting $u,v$ we see that $r(n^2a^{n-1})=n^2$ while $r(RHS)=O(n)$. A contradiction.

I read this proof in the paper of E. Gorin, who says that it is a simplification of the proof in [Rickart C. E. General Theory of Banach Algebras. Princeton NJ, D. van Nostrand (1960).]