---

Step * of Lemma isqrt_wf

∀[x:ℕ]. (isqrt(x) ∈ ℕ)
BY
{ TACTIC:(D 0 THENA Auto) }

1
1. x : ℕ
⊢ isqrt(x) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}].  (isqrt(x)  \mmember{}  \mBbbN{})


By

---

Latex:
TACTIC:(D  0  THENA  Auto)

---

Home Index