Prove property of floor function (one with square roots)

Question

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?

Answer 1

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.

Answer 2

In fact,we have $$[\sqrt{[\sqrt{x}]}]=[\sqrt{\sqrt{x}}]$$

Answer 3

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).