---

Step * 2 1 2 1 1 of Lemma sqrt-int-aa2


1. n : @i
2. r : @i
3. (r * r)  n@i
4. n < ((r + 1) * (r + 1))@i
5. ((n + 1) < ((r + 1) * (r + 1)))
6. ((r + 1) * (r + 1))  (n + 1)
 (n + 1) < (((r + 1) + 1) * ((r + 1) + 1))
BY
{ Auto' }



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


By

Auto'



Home Index