---

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


1. n:. ((n.r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))) n)
2. n : @i
 r:. (((r * r)  n)  (n < ((r + 1) * (r + 1))))
BY
{ (InstHyp [n] (-2) THEN Auto) }



1.  \mforall{}n:\mBbbN{}.  ((\mlambda{}n.\mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  n)  \mwedge{}  (n  <  ((r  +  1)  *  (r  +  1)))))  n)
2.  n  :  \mBbbN{}@i
\mvdash{}  \mexists{}r:\mBbbN{}.  (((r  *  r)  \mleq{}  n)  \mwedge{}  (n  <  ((r  +  1)  *  (r  +  1))))


By

(InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)



Home Index