---

Step * 2 1 1 2 1 1 of Lemma converges-iff-cauchy


1. x : ℕ ⟶ ℝ
2. ∀k:ℕ+. (∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k)))))])
3. f : k:ℕ+ ⟶ ℕ
4. ∀k:ℕ+. ∀n,m:ℕ.  (((f k) ≤ n) ⇒ ((f k) ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k))))
5. ∀n,m:ℕ+.  (|x[f n] - x[f m]| ≤ ((r1/r(n)) + (r1/r(m))))
6. ∀x:ℝ. ∀n:ℕ+.  (|x - (x within 1/n)| ≤ (r1/r(n)))
7. n : ℕ+
8. ∀n@0,m:ℕ.  (((f n) ≤ n@0) ⇒ ((f n) ≤ m) ⇒ (|x[n@0] - x[m]| ≤ (r1/r(n))))
9. m : ℕ+
10. ∀m@0:ℕ. (((f n) ≤ m) ⇒ ((f n) ≤ m@0) ⇒ (|x[m] - x[m@0]| ≤ (r1/r(n))))
11. |x[f n] - (x[f n] within 1/n)| ≤ (r1/r(n))
12. |x[f m] - (x[f m] within 1/m)| ≤ (r1/r(m))
13. |x[f n] - x[f m]| ≤ ((r1/r(n)) + (r1/r(m)))
⊢ |(x[f n] within 1/n) - (x[f m] within 1/m)| ≤ ((r(2)/r(n)) + (r(2)/r(m)))
BY
{ UseTriangleInequality [⌜x[f n]⌝;⌜x[f m]⌝]⋅ }

1
1. x : ℕ ⟶ ℝ
2. ∀k:ℕ+. (∃N:ℕ [(∀n,m:ℕ.  ((N ≤ n) ⇒ (N ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k)))))])
3. f : k:ℕ+ ⟶ ℕ
4. ∀k:ℕ+. ∀n,m:ℕ.  (((f k) ≤ n) ⇒ ((f k) ≤ m) ⇒ (|x[n] - x[m]| ≤ (r1/r(k))))
5. ∀n,m:ℕ+.  (|x[f n] - x[f m]| ≤ ((r1/r(n)) + (r1/r(m))))
6. ∀x:ℝ. ∀n:ℕ+.  (|x - (x within 1/n)| ≤ (r1/r(n)))
7. n : ℕ+
8. ∀n@0,m:ℕ.  (((f n) ≤ n@0) ⇒ ((f n) ≤ m) ⇒ (|x[n@0] - x[m]| ≤ (r1/r(n))))
9. m : ℕ+
10. ∀m@0:ℕ. (((f n) ≤ m) ⇒ ((f n) ≤ m@0) ⇒ (|x[m] - x[m@0]| ≤ (r1/r(n))))
11. |(x[f n] within 1/n) - x[f n]| ≤ (r1/r(n))
12. |x[f m] - (x[f m] within 1/m)| ≤ (r1/r(m))
13. |x[f n] - x[f m]| ≤ ((r1/r(n)) + (r1/r(m)))
⊢ ((r1/r(n)) + ((r1/r(n)) + (r1/r(m))) + (r1/r(m))) ≤ ((r(2)/r(n)) + (r(2)/r(m)))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  \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)))))])
3.  f  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}n,m:\mBbbN{}.    (((f  k)  \mleq{}  n)  {}\mRightarrow{}  ((f  k)  \mleq{}  m)  {}\mRightarrow{}  (|x[n]  -  x[m]|  \mleq{}  (r1/r(k))))
5.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|x[f  n]  -  x[f  m]|  \mleq{}  ((r1/r(n))  +  (r1/r(m))))
6.  \mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}\msupplus{}.    (|x  -  (x  within  1/n)|  \mleq{}  (r1/r(n)))
7.  n  :  \mBbbN{}\msupplus{}
8.  \mforall{}n@0,m:\mBbbN{}.    (((f  n)  \mleq{}  n@0)  {}\mRightarrow{}  ((f  n)  \mleq{}  m)  {}\mRightarrow{}  (|x[n@0]  -  x[m]|  \mleq{}  (r1/r(n))))
9.  m  :  \mBbbN{}\msupplus{}
10.  \mforall{}m@0:\mBbbN{}.  (((f  n)  \mleq{}  m)  {}\mRightarrow{}  ((f  n)  \mleq{}  m@0)  {}\mRightarrow{}  (|x[m]  -  x[m@0]|  \mleq{}  (r1/r(n))))
11.  |x[f  n]  -  (x[f  n]  within  1/n)|  \mleq{}  (r1/r(n))
12.  |x[f  m]  -  (x[f  m]  within  1/m)|  \mleq{}  (r1/r(m))
13.  |x[f  n]  -  x[f  m]|  \mleq{}  ((r1/r(n))  +  (r1/r(m)))
\mvdash{}  |(x[f  n]  within  1/n)  -  (x[f  m]  within  1/m)|  \mleq{}  ((r(2)/r(n))  +  (r(2)/r(m)))


By

---

Latex:
UseTriangleInequality  [\mkleeneopen{}x[f  n]\mkleeneclose{};\mkleeneopen{}x[f  m]\mkleeneclose{}]\mcdot{}

---

Home Index