---

Step * of Lemma fun-ratio-test-everywhere

∀f:ℕ ⟶ ℝ ⟶ ℝ
  ((∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y])))
  ⇒ (∀m:ℕ+. ∃c:ℝ. ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|)))))
  ⇒ Σn.f[n;x]↓ absolutely for x ∈ (-∞, ∞))
BY
{ ((InstLemma  `fun-ratio-test` [⌜(-∞, ∞)⌝]⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast')) }

1
.....antecedent..... 
1. f : ℕ ⟶ ℝ ⟶ ℝ
2. ∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y]))
⊢ ∀n:ℕ. f[n;x] continuous for x ∈ (-∞, ∞)

2
1. f : ℕ ⟶ ℝ ⟶ ℝ
2. ∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y]))
3. (∀m:{m:ℕ+| icompact(i-approx((-∞, ∞);m))} 
      ∃c:ℝ
       ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| x ∈ i-approx((-∞, ∞);m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|)))))
⇒ Σn.f[n;x]↓ absolutely for x ∈ (-∞, ∞)
⊢ (∀m:ℕ+. ∃c:ℝ. ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|)))))
⇒ Σn.f[n;x]↓ absolutely for x ∈ (-∞, ∞)

3
.....wf..... 
1. f : ℕ ⟶ ℝ ⟶ ℝ
2. (∀n:ℕ. f[n;x] continuous for x ∈ (-∞, ∞))
⇒ (∀m:{m:ℕ+| icompact(i-approx((-∞, ∞);m))} 
      ∃c:ℝ
       ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| x ∈ i-approx((-∞, ∞);m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|)))))
⇒ Σn.f[n;x]↓ absolutely for x ∈ (-∞, ∞)
⊢ ∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y])) ∈ ℙ

---

Latex:

---

Latex:
\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
    ((\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[n;x]  =  f[n;y])))
    {}\mRightarrow{}  (\mforall{}m:\mBbbN{}\msupplus{}
                \mexists{}c:\mBbbR{}
                  ((r0  \mleq{}  c)
                  \mwedge{}  (c  <  r1)
                  \mwedge{}  (\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  |x|  \mleq{}  r(m)\}  .    (|f[n  +  1;x]|  \mleq{}  (c  *  |f[n;x]|)))))
    {}\mRightarrow{}  \mSigma{}n.f[n;x]\mdownarrow{}  absolutely  for  x  \mmember{}  (-\minfty{},  \minfty{}))


By

---

Latex:
((InstLemma    `fun-ratio-test`  [\mkleeneopen{}(-\minfty{},  \minfty{})\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index