---

Step * 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)
 r:{| (((r * r)  x)  x < (r + 1) * (r + 1))}
BY
{ ((InstHyp [x - 1] 2 THENA Auto) THEN D (-1)) }

1
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)
 r:{| (((r * r)  x)  x < (r + 1) * (r + 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)
\mvdash{}  \mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))\}


By

((InstHyp  [\mkleeneopen{}x  -  1\mkleeneclose{}]  2\mcdot{}  THENA  Auto)  THEN  D  (-1))

---

Home Index