---

Step * of Lemma fun-ratio-test

No Annotations
∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.
  ((∀n:ℕ. f[n;x] continuous for x ∈ I)
  ⇒ (∀m:{m:ℕ+| icompact(i-approx(I;m))} 
        ∃c:ℝ. ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| x ∈ i-approx(I;m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|)))))
  ⇒ Σn.f[n;x]↓ absolutely for x ∈ I)
BY
{ (Auto
   THEN Try ((DSetVars THEN FLemma `i-member-approx` [-1] THEN Auto))
   THEN Unfold `fun-series-converges-absolutely` 0
   THEN Unfold `fun-series-converges` 0
   THEN BLemma `fun-converges-on-compact` 
   THEN Auto
   THEN (With ⌜m⌝ (D (-2))⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert ⌜icompact(i-approx(I;m))⌝⋅ THENA Auto)
   THEN MoveToConcl (-2)
   THEN MoveToConcl (-1)
   THEN (Assert ∀n:ℕ. f[n;x] continuous for x ∈ i-approx(I;m) BY
               (ParallelOp 3
                THEN (Assert i-approx(I;m) ⊆ I  BY
                            Auto)
                THEN FLemma `continuous_functionality_wrt_subinterval` [-1;-2]
                THEN Auto))
   THEN MoveToConcl (-1)
   THEN ((GenConcl ⌜f = g ∈ (ℕ ⟶ i-approx(I;m) ⟶ℝ)⌝⋅ THENA Auto)
         THEN ThinVar `f'
         THEN MoveToConcl (-1)
         THEN (GenConclTerm ⌜i-approx(I;m)⌝⋅ THENA Auto)
         THEN ThinVar `m'
         THEN ThinVar `I'
         THEN RenameVar `I' (-1)
         THEN Auto)⋅) }

1
1. c : ℝ
2. r0 ≤ c
3. c < r1
4. N : ℕ
5. I : Interval
6. g : ℕ ⟶ I ⟶ℝ
7. ∀n:ℕ. g[n;x] continuous for x ∈ I
8. icompact(I)
9. ∀n:{N...}. ∀x:{x:ℝ| x ∈ I} .  (|g[n + 1;x]| ≤ (c * |g[n;x]|))
⊢ λn.Σ{|g[i;x]| | 0≤i≤n}↓ for x ∈ I)

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}n:\mBbbN{}.  f[n;x]  continuous  for  x  \mmember{}  I)
    {}\mRightarrow{}  (\mforall{}m:\{m:\mBbbN{}\msupplus{}|  icompact(i-approx(I;m))\} 
                \mexists{}c:\mBbbR{}
                  ((r0  \mleq{}  c)
                  \mwedge{}  (c  <  r1)
                  \mwedge{}  (\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx(I;m)\}  .    (|f[n  +  1;x]|  \mleq{}  (c  *  |f[n;x]|)))))
    {}\mRightarrow{}  \mSigma{}n.f[n;x]\mdownarrow{}  absolutely  for  x  \mmember{}  I)


By

---

Latex:
(Auto
  THEN  Try  ((DSetVars  THEN  FLemma  `i-member-approx`  [-1]  THEN  Auto))
  THEN  Unfold  `fun-series-converges-absolutely`  0
  THEN  Unfold  `fun-series-converges`  0
  THEN  BLemma  `fun-converges-on-compact` 
  THEN  Auto
  THEN  (With  \mkleeneopen{}m\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}icompact(i-approx(I;m))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-2)
  THEN  MoveToConcl  (-1)
  THEN  (Assert  \mforall{}n:\mBbbN{}.  f[n;x]  continuous  for  x  \mmember{}  i-approx(I;m)  BY
                          (ParallelOp  3
                            THEN  (Assert  i-approx(I;m)  \msubseteq{}  I    BY
                                                    Auto)
                            THEN  FLemma  `continuous\_functionality\_wrt\_subinterval`  [-1;-2]
                            THEN  Auto))
  THEN  MoveToConcl  (-1)
  THEN  ((GenConcl  \mkleeneopen{}f  =  g\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ThinVar  `f'
              THEN  MoveToConcl  (-1)
              THEN  (GenConclTerm  \mkleeneopen{}i-approx(I;m)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ThinVar  `m'
              THEN  ThinVar  `I'
              THEN  RenameVar  `I'  (-1)
              THEN  Auto)\mcdot{})

---

Home Index