Step
*
1
of Lemma
sqrt-int-aa2
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