---

Step * 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)))))})
⊢ False
BY
{ ((InstLemma `small-reciprocal-real` [⌜e⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜k⌝] (-3)⋅ THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌜N⌝] 5⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert |x[m] - x[n]| ≤ (r1/r(k)) BY
               Auto)) }

1
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

---

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)))))\})
\mvdash{}  False


By

---

Latex:
((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}k\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}N\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  |x[m]  -  x[n]|  \mleq{}  (r1/r(k))  BY
                          Auto))

---

Home Index