---

Step * 2 1 2 of Lemma int_sqrt_sq_exists_anne


1. x : @i
2. x1:x. (r:{| (((r * r)  x1)  x1 < (r + 1) * (r + 1))})@i
3. (x = 0)
4. r : 
5. [%7] : ((r * r)  (x - 1))  x - 1 < (r + 1) * (r + 1)
6. r2 : 
7. r2 = r
8. r3 : 
9. r3 = (r2 + 1)
10. x < r3 * r3
 r:{| (((r * r)  x)  x < (r + 1) * (r + 1))}
BY
{ (With r3 (D 0) THEN Auto') }

1
1. x : @i
2. x1:x. (r:{| (((r * r)  x1)  x1 < (r + 1) * (r + 1))})@i
3. (x = 0)
4. r : 
5. (r * r)  (x - 1)
6. x - 1 < (r + 1) * (r + 1)
7. r2 : 
8. r2 = r
9. r3 : 
10. r3 = (r2 + 1)
11. x < r3 * r3
12. (r3 * r3)  x
 x < (r3 + 1) * (r3 + 1)

---

Latex:



1.  x  :  \mBbbN{}@i
2.  \mforall{}x1:\mBbbN{}x.  (\mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  x1)  \mwedge{}  x1  <  (r  +  1)  *  (r  +  1))\})@i
3.  \mneg{}(x  =  0)
4.  r  :  \mBbbN{}
5.  [\%7]  :  ((r  *  r)  \mleq{}  (x  -  1))  \mwedge{}  x  -  1  <  (r  +  1)  *  (r  +  1)
6.  r2  :  \mBbbZ{}
7.  r2  =  r
8.  r3  :  \mBbbZ{}
9.  r3  =  (r2  +  1)
10.  \mneg{}x  <  r3  *  r3
\mvdash{}  \mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))\}


By

(With  \mkleeneopen{}r3\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto')

---

Home Index