---

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


1. x : ℕ∞
2. ¬ni-eventually-equal(x;0∞)
⊢ x = ∞ ∈ ℕ∞
BY
{ (D 1 THEN EqTypeCD THEN Auto THEN Ext THEN Auto THEN RenameVar `i' (-1)) }

1
1. x : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(x (n + 1))) ⇒ (↑(x n)))
3. ¬ni-eventually-equal(x;0∞)
4. i : ℕ
⊢ x i = ∞ i

---

Latex:

---

Latex:

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


By

---

Latex:
(D  1  THEN  EqTypeCD  THEN  Auto  THEN  Ext  THEN  Auto  THEN  RenameVar  `i'  (-1))

---

Home Index