---

Step * 1 1 of Lemma isqrt_wf


1. x : ℕ
2. v : ∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))]@i
3. (TERMOF{integer-sqrt-ext:o, 1:l} x) = v ∈ (∃r:ℕ [(((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))])
⊢ v ∈ ℕ
BY
{ TACTIC:Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:Auto

---

Home Index