Prove property of floor function (one with square roots) I want to prove that:
$$\lfloor\sqrt{x}\rfloor=\lfloor\sqrt{\lfloor x\rfloor}\rfloor$$
It's true that (by definition of floor operation):
$$\lfloor\sqrt{x}\rfloor\leq\sqrt{x}<\lfloor\sqrt{x}\rfloor+1$$
$$\lfloor\sqrt{\lfloor x\rfloor}\rfloor\leq\sqrt{\lfloor x\rfloor}<\lfloor\sqrt{\lfloor x\rfloor}\rfloor+1$$
But I don't know what comes next. Tried multiple conversions of those inequalities, but I did not see anything. Can you help? 
 A: Using the implicit condition $x\ge 0$, we have for $n\in\mathbb N_0$
$$\lfloor\sqrt x\rfloor <n\iff \sqrt x<n\iff x<n^2$$
and 
$$\left\lfloor \sqrt{\lfloor x\rfloor}\right\rfloor <n\iff \sqrt{\lfloor x\rfloor}<n\iff\lfloor x\rfloor <n^2\iff x<n^2.$$
Since both $\lfloor\sqrt x\rfloor$ and $\left\lfloor \sqrt{\lfloor x\rfloor}\right\rfloor$ are in $\mathbb N_0$, this suffices to show equality.
A: Using
$$
\tag{0} n = m \;\equiv\; \langle \forall k :: k \le n \equiv k \le m \rangle
$$
for integer $\;n,m,k\;$, this is proved by the following calculation: for all $\;k\;$, we have
\begin{align}
& k \le \left\lfloor \sqrt{\left\lfloor x \right\rfloor} \right\rfloor \\
\equiv & \qquad \text{"by $(1)$ below, since $\;k\;$ is integer"} \\
& k \le \sqrt{\left\lfloor x \right\rfloor} \\
\equiv & \qquad \text{"square both sides, using RHS $\;\ge 0\;$"} \\
& k < 0 \;\lor\; k^2 \le \left\lfloor x \right\rfloor \\
\equiv & \qquad \text{"by $(1)$ below, since $\;k^2\;$ is integer"} \\
& k < 0 \;\lor\; k^2 \le x \\
\equiv & \qquad \text{"in second part: square root of both sides, using RHS $\;\ge 0\;$"} \\
& k \le \sqrt{x} \\
\equiv & \qquad \text{"by (1) below, since $\;k\;$ is integer"} \\
& k \le \left\lfloor \sqrt{x} \right\rfloor \\
\end{align}
Here I used
$$
\tag{1} k \le \left\lfloor x \right\rfloor \;\equiv\; k \le x
$$
where $\;k\;$ is integer and $\;x\;$ is real.

After I finished typing the above, I noticed that this is just like Hagen von Eitzen's answer, except that he uses the equivalent
$$
\tag{0'} n = m \;\equiv\; \langle \forall k :: n < k \equiv m < k \rangle
$$
and
$$
\tag{1'} \left\lfloor x \right\rfloor < k \;\equiv\; x < k
$$
and he lets $\;n,m,k\;$ range over the natural numbers.  And my proof is in the calculational format which I've learned like a lot (for background information, see the second part of EWD1300).
A: In fact,we have
$$[\sqrt{[\sqrt{x}]}]=[\sqrt{\sqrt{x}}]$$
A: Let $x=i+f$ where $i\in \Bbb{Z},f\in[0,1)$ . 
$\therefore\sqrt x=\sqrt{i+f}$
Now $\exists g\in[0,1)$ such that $0<g<f$ and $f=2\sqrt ig+g^2$
Also $\exists h\in[0,1)$ such that $h>f$ and $f=-2\sqrt ih+h^2$
So $$\sqrt x=\sqrt i+g=\sqrt i-h$$
However $[\sqrt i]\leq [\sqrt i+g]\le [\sqrt i]+1$ and $[\sqrt i]-1\leq [\sqrt i-h]\le [\sqrt i]$
$$\therefore [\sqrt i+g]=[\sqrt i-h]=[\sqrt i]\\\implies [\sqrt x]=\left[\sqrt[2][x]\right]$$
