Step * 1 1 of Lemma isqrt_wf


1. : ℕ
2. : ∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))]
3. (TERMOF{integer-sqrt-ext:o, 1:l} x) v ∈ (∃r:ℕ [(((r r) ≤ x) ∧ x < (r 1) (r 1))])
⊢ v ∈ ℕ
BY
xxxAutoxxx }


Latex:


Latex:

1.  x  :  \mBbbN{}
2.  v  :  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  x)  \mwedge{}  x  <  (r  +  1)  *  (r  +  1))]
3.  (TERMOF\{integer-sqrt-ext:o,  1:l\}  x)  =  v
\mvdash{}  v  \mmember{}  \mBbbN{}


By


Latex:
xxxAutoxxx




Home Index