---

Step * 2 2 1 of Lemma Kummer-criterion

.....assertion..... 
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
⇒ (∃c:{c:ℝ| r0 < c} 
     ∃N:ℕ
      ((∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n])))
      ∧ (∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1]))))))
⇒ Σn.x[n]↓
4. N : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. (((a[n] * x[n]/x[n + 1]) - a[n + 1]) ≤ r0)
7. Σn.(r1/a[N + n])↑
8. ∀n:{N...}. ((a[N] * x[N]) ≤ (a[n] * x[n]))
⊢ Σn.x[N + n]↑
BY
{ (InstLemma `comparison-test-for-divergence` [⌜λ2n.x[N + n]⌝;⌜λ2n.(a[N] * x[N]) * (r1/a[N + n])⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
⇒ (∃c:{c:ℝ| r0 < c} 
     ∃N:ℕ
      ((∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n])))
      ∧ (∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1]))))))
⇒ Σn.x[n]↓
4. N : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. (((a[n] * x[n]/x[n + 1]) - a[n + 1]) ≤ r0)
7. Σn.(r1/a[N + n])↑
8. ∀n:{N...}. ((a[N] * x[N]) ≤ (a[n] * x[n]))
⊢ Σn.(a[N] * x[N]) * (r1/a[N + n])↑

2
.....antecedent..... 
1. a : ℕ ⟶ ℝ
2. x : ℕ ⟶ ℝ
3. lim n→∞.a[n] * x[n] = r0
⇒ (∃c:{c:ℝ| r0 < c} 
     ∃N:ℕ
      ((∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n])))
      ∧ (∀n:{N...}. ((r0 < a[n]) ∧ (c ≤ ((a[n] * x[n]/x[n + 1]) - a[n + 1]))))))
⇒ Σn.x[n]↓
4. N : ℕ
5. ∀n:{N...}. ((r0 < a[n]) ∧ (r0 < x[n]))
6. ∀n:{N...}. (((a[n] * x[n]/x[n + 1]) - a[n + 1]) ≤ r0)
7. Σn.(r1/a[N + n])↑
8. ∀n:{N...}. ((a[N] * x[N]) ≤ (a[n] * x[n]))
⊢ ∃N@0:ℕ. ∀n:{N@0...}. ((r0 ≤ ((a[N] * x[N]) * (r1/a[N + n]))) ∧ (((a[N] * x[N]) * (r1/a[N + n])) ≤ x[N + n]))

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  lim  n\mrightarrow{}\minfty{}.a[n]  *  x[n]  =  r0
{}\mRightarrow{}  (\mexists{}c:\{c:\mBbbR{}|  r0  <  c\} 
          \mexists{}N:\mBbbN{}
            ((\mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n])))
            \mwedge{}  (\mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (c  \mleq{}  ((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1]))))))
{}\mRightarrow{}  \mSigma{}n.x[n]\mdownarrow{}
4.  N  :  \mBbbN{}
5.  \mforall{}n:\{N...\}.  ((r0  <  a[n])  \mwedge{}  (r0  <  x[n]))
6.  \mforall{}n:\{N...\}.  (((a[n]  *  x[n]/x[n  +  1])  -  a[n  +  1])  \mleq{}  r0)
7.  \mSigma{}n.(r1/a[N  +  n])\muparrow{}
8.  \mforall{}n:\{N...\}.  ((a[N]  *  x[N])  \mleq{}  (a[n]  *  x[n]))
\mvdash{}  \mSigma{}n.x[N  +  n]\muparrow{}


By

---

Latex:
(InstLemma  `comparison-test-for-divergence`  [\mkleeneopen{}\mlambda{}\msubtwo{}n.x[N  +  n]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}n.(a[N]  *  x[N])  *  (r1/a[N  +  n])\mkleeneclose{}]\mcdot{}
  THEN  Auto
  )

---

Home Index