---

Step * 1 of Lemma sqrt-int-aa-fast


r:. (((r * r)  0)  (0 < ((r + 1) * (r + 1))))
BY
{ (InstConcl [0] THEN Auto) }



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


By

(InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index