---

Step * 1 of Lemma isqrt_wf


1. x : ℕ
⊢ isqrt(x) ∈ ℕ
BY
{ (Unfold `isqrt` 0 THEN ((GenConclAtAddr [2]) THENA Auto)) }

1
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 ∈ ℕ

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}
\mvdash{}  isqrt(x)  \mmember{}  \mBbbN{}


By

---

Latex:
(Unfold  `isqrt`  0  THEN  ((GenConclAtAddr  [2])  THENA  Auto))

---

Home Index