---

Step * 2 1 1 1 2 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 : ℕ+
6. m : ℕ+
7. ¬((f n) ≤ (f m))
⊢ |x[f n] - x[f m]| ≤ ((r1/r(n)) + (r1/r(m)))
BY
{ ((Assert |x[f n] - x[f m]| ≤ (r1/r(m)) BY (BHyp 4 THEN Auto)) THEN (RWO "-1" 0 THENA Auto)) }

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 : ℕ+
6. m : ℕ+
7. ¬((f n) ≤ (f m))
8. |x[f n] - x[f m]| ≤ (r1/r(m))
⊢ (r1/r(m)) ≤ ((r1/r(n)) + (r1/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.  n  :  \mBbbN{}\msupplus{}
6.  m  :  \mBbbN{}\msupplus{}
7.  \mneg{}((f  n)  \mleq{}  (f  m))
\mvdash{}  |x[f  n]  -  x[f  m]|  \mleq{}  ((r1/r(n))  +  (r1/r(m)))


By

---

Latex:
((Assert  |x[f  n]  -  x[f  m]|  \mleq{}  (r1/r(m))  BY  (BHyp  4  THEN  Auto))  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index