---

Step * 2 of Lemma not-ni-eventually-equal-inf


1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
⊢ ¬ni-eventually-equal(x;0∞)
BY
{ ((HypSubst' (-1) 0 THENA Auto) THEN (D 0 THENA Auto) THEN D -1 THEN (InstHyp [⌜n⌝] (-1)⋅ THENA Auto)) }

1
1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
3. n : ℕ
4. ∀m:{n...}. ∞ m = 0∞ m
5. ∞ n = 0∞ n
⊢ False

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\minfty{}
2.  x  =  \minfty{}
\mvdash{}  \mneg{}ni-eventually-equal(x;0\minfty{})


By

---

Latex:
((HypSubst'  (-1)  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index