Variational characterisation of the nearest point

Suppose first that $p$ is nearest, and let $y\in C$; for every $t$ with $0<t\le 1$ the convexity hypothesis gives $p+t(y-p)\in C$, so $\mathrm{\parallel }x-p{\mathrm{\parallel }}^2\le \mathrm{\parallel }x-p-t(y-p){\mathrm{\parallel }}^2=\mathrm{\parallel }x-p{\mathrm{\parallel }}^2-2t\mathrm{Re}⟨x-p,y-p⟩+t^2\mathrm{\parallel }y-p{\mathrm{\parallel }}^2$, whence $2\mathrm{Re}⟨x-p,y-p⟩\le t\mathrm{\parallel }y-p{\mathrm{\parallel }}^2$, and if $\mathrm{Re}⟨x-p,y-p⟩$ were positive the choice $t<\min \{1,2\mathrm{Re}⟨x-p,y-p⟩\mathrm{/}(\mathrm{\parallel }y-p{\mathrm{\parallel }}^2+1)\}$ would make the right-hand side strictly smaller than the left, a contradiction; hence $\mathrm{Re}⟨x-p,y-p⟩\le 0$.

Conversely suppose $\mathrm{Re}⟨x-p,y-p⟩\le 0$ for every $y\in C$; then $\mathrm{\parallel }x-y{\mathrm{\parallel }}^2=\mathrm{\parallel }(x-p)+(p-y){\mathrm{\parallel }}^2=\mathrm{\parallel }x-p{\mathrm{\parallel }}^2+2\mathrm{Re}⟨x-p,p-y⟩+\mathrm{\parallel }p-y{\mathrm{\parallel }}^2\ge \mathrm{\parallel }x-p{\mathrm{\parallel }}^2$, because $\mathrm{Re}⟨x-p,p-y⟩=-\mathrm{Re}⟨x-p,y-p⟩\ge 0$.

Steps 1.1 and 1.2 prove both implications of the stated equivalence; the Countable Choice hypothesis is used only to invoke the existence theorem for nearest points (Projection onto a nonempty closed convex set) when the nearest point is not supplied, while the equivalence itself is choice-free for a given $p$.