Prove that $(\sup\{y\in\Bbb R^{\ge0}:y^2\le x\})^2=x$ This question is a simple one from foundations of analysis, regarding the definition of the square root function. We begin by defining
$$\sqrt x:=\sup\{y\in\Bbb R^{\ge0}:y^2\le x\}:=\sup S(x)$$
for $x\ge0$, and now we wish to show that it satisfies its defining property, namely $\sqrt x^2=x$. By dividing into cases $x\le1$ (where $1$ is an upper bound for $S(x)$) and $x\ge1$ (where $x$ is an upper bound for $S(x)$), we know $S(x)$ is upper bounded and hence the function is well-defined for all $x\ge0$.
It follows from the intermediate value theorem applied to $f(y)=y^2$ on $[0,\max(1,x)]$ that $\sqrt x^2=x$, if we can prove that $f(y)$ is continuous, but suffice it to say that I would like to prove the IVT later in generality, when I will have the definition $|x|=\sqrt{xx^*}$ (which is used in the definition of continuity), so I hit a circularity problem. Thus I need a "bootstrap" version of the IVT for this particular case, i.e. I can't just invoke this theorem.
What is the cleanest way to get to the goal here? Assume I don't have any theorems to work from except basic algebra.

Let $A=\sup S(x)=\sqrt x$. (We wish to show $A^2=x$.) By the AM-GM inequality, $\frac12(A+\frac xA)\ge\sqrt x$. Here's the algebraic proof of this claim:
$$0\le\Big(A-\frac xA\Big)^2=A^2-2x+\frac{x^2}{A^2}\implies 4x\le A^2+2x+\frac{x^2}{A^2}=\Big(A+\frac xA\!\Big)^2,$$
and we get the desired inequality by applying a square root and dividing by 2. Of course we don't have square root yet, so we can just keep it in this form. The point is that if $A^2>x$, then $A>\frac xA$, so $A>\frac12(A+\frac xA)$. But for each $y\in S(x)$, $y^2\le x\le\frac14(A+\frac xA)^2$, so $y\le\frac12(A+\frac xA)$. (Note that $a<b$ iff $a^2<b^2$ for $a,b\in\Bbb R^{\ge0}$.) Thus $\frac12(A+\frac x A)$ is an upper bound of $S(x)$ less than $A$, a contradiction. Therefore $A^2\le x$.
If $x=0$, then $S(0)=\{0\}$ so $\sup S(0)=0$ and thus $A^2=x$. If $x>0$ then $0<\min(x,1)^2<x$ so $\sup S(x)=A>0$. Thus $2A>A$ so if $A^2\le\frac x4$ then $2A\in S(x)$, a contradiction. Thus $A^2>\frac x4$.
For the final case, if $0<\frac x4\le A^2<x$ then $\frac 32A>0$, $x-A^2>0$, and $A^2-\frac x4\ge0$, so
$$0\le\frac{x-A^2}{[\frac 32\!A]^2}\Big(A^2-\frac x4\!\Big)=x-\frac{x^2A^{-2}+4x+4A^2}9=x-\Big(\!\frac{xA^{-1}+2A}3\!\Big)^2:=x-B^2,$$
so $B^2\le x$. Also $$B=\frac x{3A}+\frac{2A}3=A+\frac{x-A^2}{3A},$$ so $B>A$. Thus $B\in S(x)$ is greater than $A=\sup S(x)$, a contradiction. Thus $A^2=x$.
