---

Step * 2 1 2 1 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. (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)
BY
{ (ElimVar `r3' THEN ElimVar `r2' THEN Auto') }

---

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.  (r  *  r)  \mleq{}  (x  -  1)
6.  x  -  1  <  (r  +  1)  *  (r  +  1)
7.  r2  :  \mBbbZ{}
8.  r2  =  r
9.  r3  :  \mBbbZ{}
10.  r3  =  (r2  +  1)
11.  \mneg{}x  <  r3  *  r3
12.  (r3  *  r3)  \mleq{}  x
\mvdash{}  x  <  (r3  +  1)  *  (r3  +  1)


By

(ElimVar  `r3'  THEN  ElimVar  `r2'  THEN  Auto')\mcdot{}

---

Home Index