---

Step * 1 1 1 of Lemma tsqrt_wf


1. n : ℕ
2. v : ℕ
3. isqrt(2 * n) = v ∈ ℕ
4. 2 * n < (v * v) + v
5. v = 0 ∈ ℤ
⊢ 0 - 1 ∈ ℕ
BY
{ (HypSubst' (-1) (-2) THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  v  :  \mBbbN{}
3.  isqrt(2  *  n)  =  v
4.  2  *  n  <  (v  *  v)  +  v
5.  v  =  0
\mvdash{}  0  -  1  \mmember{}  \mBbbN{}


By

---

Latex:
(HypSubst'  (-1)  (-2)  THEN  Auto')

---

Home Index