Step
*
2
1
2
of Lemma
sqrt-int-aa2
1. n : 
@i
2. r : 
@i
3. ((r * r) 
 n) 
 (n < ((r + 1) * (r + 1)))@i
4. 
((n + 1) < ((r + 1) * (r + 1)))
 
r:
. (((r * r) 
 (n + 1)) 
 ((n + 1) < ((r + 1) * (r + 1))))
BY
{ (Assert ((r + 1) * (r + 1)) 
 (n + 1) BY
         MaAuto) }
1
1. n : 
@i
2. r : 
@i
3. ((r * r) 
 n) 
 (n < ((r + 1) * (r + 1)))@i
4. 
((n + 1) < ((r + 1) * (r + 1)))
5. ((r + 1) * (r + 1)) 
 (n + 1)
 
r:
. (((r * r) 
 (n + 1)) 
 ((n + 1) < ((r + 1) * (r + 1))))
1.  n  :  \mBbbN{}@i
2.  r  :  \mBbbN{}@i
3.  ((r  *  r)  \mleq{}  n)  \mwedge{}  (n  <  ((r  +  1)  *  (r  +  1)))@i
4.  \mneg{}((n  +  1)  <  ((r  +  1)  *  (r  +  1)))
\mvdash{}  \mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  (n  +  1))  \mwedge{}  ((n  +  1)  <  ((r  +  1)  *  (r  +  1))))
By
(Assert  ((r  +  1)  *  (r  +  1))  \mleq{}  (n  +  1)  BY
              MaAuto)
Home
Index