Prove that given a nonnegative integer n, there is a unique nonnegative integer m such that m^2≤n<(m+1)^2
I started like this:
There are two cases to consider: either n is a perfect square or it is not.
Assume n is a perfect square. For the existence part of the proof, let m=√n, where √n is a positive root of n. Then (√n)^2=n, so (√n)^2≤n. Assume for reductio that n≥(√n+1)^2. Factor the right hand side of the inequality and get n≥n+2√n+1. Therefore -1≥2√n, and -1/2≥√n. But √n is a positive root, so we have a contradiction.
So there exists an m such that m^2≤n<(m+1)^2.
Now I prove that m is unique. I do this by showing that m cannot be greater or less than √n. To show it is not greater, assume without loss of generality that there is a nonnegative integer m' such that m'=m+1. Therefore, m'=√n+1. Then, for reductio, assume (√n+1)^2≤n<(√n+1+1)^2. The left side of the inequality, (√n+1)^2≤n, contradicts the right hand side of (i): n<(√n+1)^2.
Now assume that there is a nonnegative integer m' such that m'=m-1. So, m'=√n-1. Now assume (√n-1)^2≤n<(√n-1+1)^2. The right side becomes n<(√n)^2 or n<n, which is a contradiction. Thus, m is unique.
How do I show this for the case where n is not a perfect square? I know that if n is not a perfect square, then m^2≠n, so I have to prove m^2<n<(m+1)^2. I don't know where to go from here though.
It might interest you to know that by coincidence I found this theorem used in a real application just now. GMP is a free library for arbitrary precision arithmetic (bignums) for C. I was looking through the source code file /gmp-5.0.1/mpf/sqrt.c and therein is an argument for why desired precision is achieved through the specified truncation using this theorem in the proof.
"Further limbs below the 2*prec or 2*prec-1 used don't affect the result and are simply truncated. This can be seen by considering an integer x, with s=floor(sqrt(x)). s is the unique integer satisfying s^2 <= x < (s+1)^2. Notice that adding a fraction part to x (ie. some further bits) doesn't change the inequality, s remains the unique solution. Working suitable factors of 2 into this argument lets it apply to an intended precision at any position for any x, not just the integer binary point."
Edit: This appears to be the algorithm implemented
Info: (gmp) Square Root Algorithm