---

Step * 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
 r:{| (((r * r)  0)  0 < (r + 1) * (r + 1))}
BY
{ (With 0 (D 0) 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.  x  =  0
\mvdash{}  \mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  0)  \mwedge{}  0  <  (r  +  1)  *  (r  +  1))\}


By

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

---

Home Index