---

Step * of Lemma int_sqrt_sq_exists_anne

x:. (r:{| (((r * r)  x)  x < (r + 1) * (r + 1))})
BY
{ ((GeneralInductionOnNat THENA Auto) THEN CaseNat 0 `x') }

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

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

---

Latex:


\mforall{}x:\mBbbN{}.  (\mexists{}r:\{\mBbbN{}|  (((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))\})


By

((GeneralInductionOnNat  THENA  Auto)  THEN  CaseNat  0  `x')

---

Home Index