---

Step * 1 1 of Lemma not-diverges-converges


1. x : ℕ ⟶ ℝ
2. x[n]↓ as n→∞@i
3. e : ℝ@i
4. r0 < e@i
5. ∀k:ℕ. ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ |x[m] - x[n]|))@i
6. ∀k:ℕ+. (∃N:{ℕ| (∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k)))))})
7. k : ℕ+
8. (r1/r(k)) < e
9. N : ℕ
10. ∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k))))
11. m : ℕ
12. n : ℕ
13. N ≤ m
14. N ≤ n
15. e ≤ |x[m] - x[n]|
16. |x[m] - x[n]| ≤ (r1/r(k))
⊢ False
BY
{ (RelRST THEN All Thin THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}@i
3.  e  :  \mBbbR{}@i
4.  r0  <  e@i
5.  \mforall{}k:\mBbbN{}.  \mexists{}m,n:\mBbbN{}.  ((k  \mleq{}  m)  \mwedge{}  (k  \mleq{}  n)  \mwedge{}  (e  \mleq{}  |x[m]  -  x[n]|))@i
6.  \mforall{}k:\mBbbN{}\msupplus{}.  (\mexists{}N:\{\mBbbN{}|  (\mforall{}n,m:\mBbbN{}.    ((N  \mleq{}  n)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (|x[n]  -  x[m]|  \mleq{}  (r1/r(k)))))\})
7.  k  :  \mBbbN{}\msupplus{}
8.  (r1/r(k))  <  e
9.  N  :  \mBbbN{}
10.  \mforall{}n,m:\mBbbN{}.    ((N  \mleq{}  n)  {}\mRightarrow{}  (N  \mleq{}  m)  {}\mRightarrow{}  (|x[n]  -  x[m]|  \mleq{}  (r1/r(k))))
11.  m  :  \mBbbN{}
12.  n  :  \mBbbN{}
13.  N  \mleq{}  m
14.  N  \mleq{}  n
15.  e  \mleq{}  |x[m]  -  x[n]|
16.  |x[m]  -  x[n]|  \mleq{}  (r1/r(k))
\mvdash{}  False


By

---

Latex:
(RelRST  THEN  All  Thin  THEN  Auto)\mcdot{}

---

Home Index