---

Step * 2 1 of Lemma fun-ratio-test-everywhere


1. f : ℕ ⟶ ℝ ⟶ ℝ
2. ∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y]))
3. ∀m:ℕ+. ∃c:ℝ. ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|))))
4. 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]|))))
BY
{ ((InstHyp [⌜m⌝] (-2)⋅ THENA Auto) THEN ParallelLast THEN Auto) }

1
1. f : ℕ ⟶ ℝ ⟶ ℝ
2. ∀n:ℕ. ∀x,y:ℝ.  ((x = y) ⇒ (f[n;x] = f[n;y]))
3. ∀m:ℕ+. ∃c:ℝ. ((r0 ≤ c) ∧ (c < r1) ∧ (∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|))))
4. m : {m:ℕ+| icompact(i-approx((-∞, ∞);m))} 
5. c : ℝ
6. r0 ≤ c
7. c < r1
8. ∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|))
9. r0 ≤ c
10. c < r1
⊢ ∃N:ℕ. ∀n:{N...}. ∀x:{x:ℝ| x ∈ i-approx((-∞, ∞);m)} .  (|f[n + 1;x]| ≤ (c * |f[n;x]|))

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbR{}
2.  \mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}.    ((x  =  y)  {}\mRightarrow{}  (f[n;x]  =  f[n;y]))
3.  \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]|))))
4.  m  :  \{m:\mBbbN{}\msupplus{}|  icompact(i-approx((-\minfty{},  \minfty{});m))\} 
\mvdash{}  \mexists{}c:\mBbbR{}
      ((r0  \mleq{}  c)
      \mwedge{}  (c  <  r1)
      \mwedge{}  (\mexists{}N:\mBbbN{}.  \mforall{}n:\{N...\}.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  i-approx((-\minfty{},  \minfty{});m)\}  .    (|f[n  +  1;x]|  \mleq{}  (c  *  |f[n;x]|))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  ParallelLast  THEN  Auto)

---

Home Index