---

Step * of Lemma tsqrt_wf

No Annotations
∀[n:ℕ]. (tsqrt(n) ∈ ℕ)
BY
{ ((D 0 THENA Auto) THEN Unfold `tsqrt` 0 THEN (GenConclAtAddr [2;1] THENA Auto)) }

1
1. n : ℕ
2. v : ℕ
3. isqrt(2 * n) = v ∈ ℕ
⊢ eval r = v in
  if (r * r) + r ≤z 2 * n then r else r - 1 fi  ∈ ℕ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}].  (tsqrt(n)  \mmember{}  \mBbbN{})


By

---

Latex:
((D  0  THENA  Auto)  THEN  Unfold  `tsqrt`  0  THEN  (GenConclAtAddr  [2;1]  THENA  Auto))

---

Home Index