Step * of Lemma isqrtn_wf

x:ℕ(isqrtn(x) ∈ {r:ℕ((r r) ≤ x) ∧ x < (r 1) (r 1)} )
BY
xxxProveWfLemmaxxx }


Latex:


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


By


Latex:
xxxProveWfLemmaxxx




Home Index