---

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


1. x : ℕ∞
2. x = ∞ ∈ ℕ∞
3. n : ℕ
4. ∀m:{n...}. ∞ m = 0∞ m
5. tt = n <z 0
⊢ False
BY
{ (MoveToConcl (-1) THEN AutoBoolCase ⌜n <z 0⌝⋅) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\minfty{}
2.  x  =  \minfty{}
3.  n  :  \mBbbN{}
4.  \mforall{}m:\{n...\}.  \minfty{}  m  =  0\minfty{}  m
5.  tt  =  n  <z  0
\mvdash{}  False


By

---

Latex:
(MoveToConcl  (-1)  THEN  AutoBoolCase  \mkleeneopen{}n  <z  0\mkleeneclose{}\mcdot{})

---

Home Index