---

Step * 2 1 2 1 of Lemma sqrt-int-aa-fast


1. i : @i
2. r : @i
3. (r * r)  (i  4)@i
4. (i  4) < ((r + 1) * (r + 1))@i
5. (i < (((2 * r) + 1) * ((2 * r) + 1)))
 i < ((((2 * r) + 1) + 1) * (((2 * r) + 1) + 1))
BY
{ Fiat }



1.  i  :  \mBbbN{}@i
2.  r  :  \mBbbN{}@i
3.  (r  *  r)  \mleq{}  (i  \mdiv{}  4)@i
4.  (i  \mdiv{}  4)  <  ((r  +  1)  *  (r  +  1))@i
5.  \mneg{}(i  <  (((2  *  r)  +  1)  *  ((2  *  r)  +  1)))
\mvdash{}  i  <  ((((2  *  r)  +  1)  +  1)  *  (((2  *  r)  +  1)  +  1))


By

Fiat



Home Index