---

Step * 3 of Lemma ni-eventually-equal-equiv


1. ∀a:ℕ∞. ∃n:ℕ. ∀m:{n...}. a m = a m
2. ∀a,b:ℕ∞.  ((∃n:ℕ. ∀m:{n...}. a m = b m) ⇒ (∃n:ℕ. ∀m:{n...}. b m = a m))
3. a : ℕ∞
4. b : ℕ∞
5. c : ℕ∞
6. ∃n:ℕ. ∀m:{n...}. a m = b m
7. ∃n:ℕ. ∀m:{n...}. b m = c m
⊢ ∃n:ℕ. ∀m:{n...}. a m = c m
BY
{ (ExRepD THEN With ⌜imax(n;n1)⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  \mforall{}a:\mBbbN{}\minfty{}.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  a  m
2.  \mforall{}a,b:\mBbbN{}\minfty{}.    ((\mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  b  m)  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  b  m  =  a  m))
3.  a  :  \mBbbN{}\minfty{}
4.  b  :  \mBbbN{}\minfty{}
5.  c  :  \mBbbN{}\minfty{}
6.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  b  m
7.  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  b  m  =  c  m
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}m:\{n...\}.  a  m  =  c  m


By

---

Latex:
(ExRepD  THEN  With  \mkleeneopen{}imax(n;n1)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index