Hilbert spaces are uniformly convex

By [F2], the induced function is a norm. The assumed completeness and [F3] therefore make $H$ a real or complex Banach space. This also covers the zero Hilbert space.

For arbitrary $x,y\in H$, expand with [F1]: $\mathrm{\parallel }x+y{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2+⟨x,y⟩+⟨y,x⟩+\mathrm{\parallel }y{\mathrm{\parallel }}^2,$ while $\mathrm{\parallel }x-y{\mathrm{\parallel }}^2=\mathrm{\parallel }x{\mathrm{\parallel }}^2-⟨x,y⟩-⟨y,x⟩+\mathrm{\parallel }y{\mathrm{\parallel }}^2\mathrm{.}$ Adding cancels the two cross terms, over both scalar fields, and gives $\mathrm{\parallel }x+y{\mathrm{\parallel }}^2+\mathrm{\parallel }x-y{\mathrm{\parallel }}^2=2\mathrm{\parallel }x{\mathrm{\parallel }}^2+2\mathrm{\parallel }y{\mathrm{\parallel }}^2\mathrm{.}$

Now let $x,y$ lie in the closed unit ball and suppose $\mathrm{\parallel }x-y\mathrm{\parallel }\ge \epsilon$. By [F2] and step 1.2, ${\parallel \frac{x+y}{2}\parallel }^2=\frac{\mathrm{\parallel }x{\mathrm{\parallel }}^2+\mathrm{\parallel }y{\mathrm{\parallel }}^2}{2}-\frac{\mathrm{\parallel }x-y{\mathrm{\parallel }}^2}{4}\le 1-\frac{{\epsilon }^2}{4}\mathrm{.}$ The radicand $r=1-{\epsilon }^2\mathrm{/}4$ belongs to $[0,1)$ because $0<\epsilon \le 2$. Let $s=\sqrt{r}\ge 0$ as in [F4]. If $s\ge 1$, then either $s=1$ or strict monotonicity of squaring gives $s^2>1$, whereas $s^2=r<1$; hence $s<1$. Since both $\mathrm{\parallel }(x+y)\mathrm{/}2\mathrm{\parallel }$ and $s$ are nonnegative, their squared inequality and strict monotonicity of squaring give $\parallel \frac{x+y}{2}\parallel \le s=1-\delta (\epsilon )\mathrm{.}$ Thus $\delta (\epsilon )=1-s>0$. At $\epsilon =2$, $r=s=0$ and $\delta (2)=1$.

Step 2.1 applies to every closed-unit-ball pair satisfying the separation hypothesis and supplies a positive number depending only on $\epsilon$. Therefore [F3] proves that $H$ is uniformly convex. No choice principle is used: the square root in the displayed formula is unique by [F4].