---

Step * of Lemma not-diverges-converges

∀[x:ℕ ⟶ ℝ]. (¬(x[n]↓ as n→∞ ∧ n.x[n]↑))
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN (FLemma `converges-iff-cauchy` [-2] THENA Auto)
   THEN Unfold `cauchy` -1
   THEN D -2
   THEN 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)))))})
⊢ False

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  (\mneg{}(x[n]\mdownarrow{}  as  n\mrightarrow{}\minfty{}  \mwedge{}  n.x[n]\muparrow{}))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  (FLemma  `converges-iff-cauchy`  [-2]  THENA  Auto)
  THEN  Unfold  `cauchy`  -1
  THEN  D  -2
  THEN  Auto)

---

Home Index