<s>[INST] Existence of $2^{1/2}$ I'm trying to prove, that the square root of 2 exists in $\mathbb{R}$.
I'm looking at the set $A:=\{y\in\mathbb{R}: y\geq 0, y^2\geq 2\}$. I have already proven that the greatest lower bound $b$ of $A$ exists. However, now I don't know how to proceed. I know that I should consider the cases $b^2 > 2$ and $b^2 < 2$, and bring them to a contradiction, so only the possibility $b^2=2$ is left. I have been given the tip to use the quantities $a:=\frac{1}{2}(1 - \frac{2}{b^2}),\; a^\prime := \frac{1}{2}(1-\frac{b^2}{2}),\; b(1-a),\; \frac{b}{1-a^\prime}$.
I believe I should get to the contradiction that $b$ can't be the greatest lower bound in both cases, but I don't see how to get there.
Any ideas?
 [/INST] Suppose that the infimum is $b$ and there is no real number $c$ such that $c^2=2$.  Then if $b^2> 2$, then we have $0<a<1$ and moreover: 
$$
b(1-a)< b\\
b^2(1-a)^2=b^2\left(\frac 12+\frac 1{b^2}\right)^2\geq b^2\left(\frac {\sqrt 2}{b}\right)^2=2
$$
where the last inequality comes from simple AM-GM inequality. But this is a contradiction because $b(1-a)< b$ which means that we found $b(1-a)$ less than the infimum $b$ but still bigger than or equal to 2.
On the other  hand, if $b^2<2$ then we also have $0<a'<1$, hence $b/(1-a')> b$ and because $b$ is infimum then $\frac{b^2}{(1-a')^2}> 2$ (if $\frac{b^2}{(1-a')^2}=2$ then we found $c$ such that $c^2=2$). But: 
$$
\frac{b^2}{(1-a')^2}=\frac{b^2}{\left(\frac 12+\frac {b^2}4\right)^2} \leq \frac{b^2}{\left(\frac { 2 b}{\sqrt 8}\right)^2}=2
$$
which is again a contradition. 
Therefore $b^2=2$. 
</s>