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.
 A: Since you have the l.u.b. axiom, you can use that, for any two bounded sets $A,B$ of nonnegative reals, we have 
$$(\sup A) \cdot (\sup B)=\sup( \{a\cdot b:a \in A,b \in B\}).$$
Applying this to $A=B=S(x)$ we want to find the sup of the set of products $a\cdot b$ where $a^2\le x$ and $b^2 \le x.$ First note any such product is at most $x$: without loss assume $a \le b$, then we have $ab \le b^2 \le x.$ This much shows $\sqrt{x}\cdot \sqrt{x} \le x$ for your definition of $\sqrt{x}$ as a sup.
Second, since we may use any (independent) choices of $a,b \in S(x)$ we may in particular take them both equal, and obtain the products $t\cdot t=t^2$ which, given the definition of $S(x)$, have supremum $x$, which shows that $\sqrt{x}\cdot \sqrt{x} \ge x$.
A: Let $f(x):=\sqrt{x}:=\sup(y| y^2\leq x)$. 
As pointed in the comments existence of supremum implies the Archimedean property: If there is $x$ such that for every $n\in\mathbb{N}$, $x>n$ then there is a supremum $y$ of $\mathbb{N}$. But then there is $n\in\mathbb{N}$ such that $n>y-1$, from where $\mathbb{N}\ni n+1>y$. Which is a contradiction. Therefore we have:
Archimedean property:
For every $x$ there is $n\in\mathbb{N}$ such that $n>x$.
The Archimedean property is very comfortable to use because from there we can apply the proof about limits etc. that we are used to in Calculus. 
Since supremum is minimal bound: 
For every $n\in\mathbb{N}$ there is $y_n$ such that $y_n^2\leq x$ and $y_n>f(x)-\frac{1}{n}$. We can take $n$ such that $f(x)-\frac{1}{n}>0$ (Archimedean property). Square both sides of $y_n>f(x)-\frac{1}{n}$ to get $$x\geq y_n^2>(f(x)-\frac{1}{n})^2$$. We have that $f(x)^2$ is an upper bound of all $(f(x)-\frac{1}{n})^2$. 
We prove now that is the minimal bound. For every $e>0$ take $n$ such that $n>\frac{2f(x)}{e}$ (Archimedean property). Then $e\geq \frac{2f(x)}{n}>\frac{2f(x)}{n}-\frac{1}{n^2}$, from where $f(x)^2-e<f(x)^2-\frac{2f(x)}{n}+\frac{1}{n^2}=(f(x)-\frac{1}{n})^2$. Hence $f(x)^2$ is the minimal bound of the $(f(x)-\frac{1}{n})^2$.
From the above displayed inequality $x$ is an upper bound of the $(f(x)-\frac{1}{n})^2$ and therefore it is larger than its supremum, i.e. we get that $x\geq f(x)^2$.
Now we need to get the other inequality.
Since supremum is a bound: 
For every $n>0$ we have $(f(x)+\frac{1}{n})^2> x$, otherwise $f(x)$ is not an upper bound of $(y|y^2<x)$. Now we need to show that $-f(x)^2$ is the supremum of $-(f(x)-\frac{1}{n})^2$. This will imply that $-f(x)^2\leq-x$, i.e. $f(x)^2\geq x$. I put the minus sign to use that we have supremum of bounded sets, but of course it happens likewise for infimum. Now we proceed as before. Let $e>0$ and take $n$ such that $n>\frac{1}{e}$ then $n^2>\frac{1}{e}$ or $e>\frac{1}{n^2}>-\frac{2f(x)}{n}+\frac{1}{n^2}$. Hence $-f(x)^2-e<-f(x)^2+\frac{2f(x)}{n}-\frac{1}{n^2}=-(f(x)-\frac{1}{n})^2$. Thus, $-f(x)^2$ is the minimal bound of the $-(f(x)-\frac{1}{n})^2$, and therefore the supremum. QED.
A: 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$.
