---

Step * 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. [%7] : ((r * r)  (x - 1))  x - 1 < (r + 1) * (r + 1)
 r:{| (((r * r)  x)  x < (r + 1) * (r + 1))}
BY
{ ((Evaluate r2 = r THENA Auto)
   THEN (Evaluate r3 = (r2 + 1) THENA Auto)
   THEN (Decide x < r3 * r3 THENA Auto)) }

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)
6. r2 : 
7. r2 = r
8. r3 : 
9. r3 = (r2 + 1)
10. x < r3 * r3
 r:{| (((r * r)  x)  x < (r + 1) * (r + 1))}

2
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))}

---

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


By

((Evaluate  \mkleeneopen{}r2  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}r3  =  (r2  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Decide  \mkleeneopen{}x  <  r3  *  r3\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index