---

Step * of Lemma series-diverges-rmul

∀[x:ℕ ⟶ ℝ]. (Σn.x[n]↑ ⇒ (∀c:ℝ. (c ≠ r0 ⇒ Σn.c * x[n]↑)))
BY
{ (Auto THEN D 2 THEN D 0 With ⌜|c| * e⌝  THEN Auto) }

1
1. [x] : ℕ ⟶ ℝ
2. e : ℝ
3. r0 < e
4. ∀k:ℕ. ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ |Σ{x[i] | 0≤i≤m} - Σ{x[i] | 0≤i≤n}|))
5. c : ℝ
6. c ≠ r0
⊢ r0 < (|c| * e)

2
1. [x] : ℕ ⟶ ℝ
2. e : ℝ
3. r0 < e
4. ∀k:ℕ. ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ (e ≤ |Σ{x[i] | 0≤i≤m} - Σ{x[i] | 0≤i≤n}|))
5. c : ℝ
6. c ≠ r0
7. r0 < (|c| * e)
8. k : ℕ
⊢ ∃m,n:ℕ. ((k ≤ m) ∧ (k ≤ n) ∧ ((|c| * e) ≤ |Σ{c * x[i] | 0≤i≤m} - Σ{c * x[i] | 0≤i≤n}|))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}].  (\mSigma{}n.x[n]\muparrow{}  {}\mRightarrow{}  (\mforall{}c:\mBbbR{}.  (c  \mneq{}  r0  {}\mRightarrow{}  \mSigma{}n.c  *  x[n]\muparrow{})))


By

---

Latex:
(Auto  THEN  D  2  THEN  D  0  With  \mkleeneopen{}|c|  *  e\mkleeneclose{}    THEN  Auto)

---

Home Index