Step
*
1
2
1
of Lemma
integral-from-Taylor
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} . ((x = y)
⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
6. ∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t)
7. b : {b:ℝ| b ∈ (a - t, a + t)}
8. lim n→∞.b_∫-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λx.b_∫-x F[0;t] dt for x ∈ (a - t, a + t)
9. n : ℕ
10. x : {x:ℝ| x ∈ (a - t, a + t)}
11. [rmin(b;x), rmax(b;x)] ⊆ (a - t, a + t)
⊢ b_∫-x (F[i;a]/r((i)!)) * t - a^i dt = (F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)) for i ∈ [0,n]
BY
{ (D 0 THEN Auto) }
1
1. a : ℝ
2. t : {t:ℝ| r0 < t}
3. F : ℕ ⟶ (a - t, a + t) ⟶ℝ
4. ∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} . ((x = y)
⇒ (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
6. ∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t)
7. b : {b:ℝ| b ∈ (a - t, a + t)}
8. lim n→∞.b_∫-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λx.b_∫-x F[0;t] dt for x ∈ (a - t, a + t)
9. n : ℕ
10. x : {x:ℝ| x ∈ (a - t, a + t)}
11. [rmin(b;x), rmax(b;x)] ⊆ (a - t, a + t)
12. i : ℤ
13. 0 ≤ i
14. i ≤ n
⊢ b_∫-x (F[i;a]/r((i)!)) * t - a^i dt = ((F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)))
Latex:
Latex:
1. a : \mBbbR{}
2. t : \{t:\mBbbR{}| r0 < t\}
3. F : \mBbbN{} {}\mrightarrow{} (a - t, a + t) {}\mrightarrow{}\mBbbR{}
4. \mforall{}k:\mBbbN{}. \mforall{}x,y:\{x:\mBbbR{}| x \mmember{} (a - t, a + t)\} . ((x = y) {}\mRightarrow{} (F[k;x] = F[k;y]))
5. infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
6. \mforall{}r:\{r:\mBbbR{}| (r0 \mleq{} r) \mwedge{} (r < t)\} . lim k\mrightarrow{}\minfty{}.r\^{}k * (F[k + 1;x]/r((k)!)) = \mlambda{}x.r0 for x \mmember{} (a - t, a + t)
7. b : \{b:\mBbbR{}| b \mmember{} (a - t, a + t)\}
8. lim n\mrightarrow{}\minfty{}.b\_\mint{}\msupminus{}x \mSigma{}\{(F[i;a]/r((i)!)) * t - a\^{}i | 0\mleq{}i\mleq{}n\} dt = \mlambda{}x.b\_\mint{}\msupminus{}x F[0;t] dt for x \mmember{} (a - t, a
+ t)
9. n : \mBbbN{}
10. x : \{x:\mBbbR{}| x \mmember{} (a - t, a + t)\}
11. [rmin(b;x), rmax(b;x)] \msubseteq{} (a - t, a + t)
\mvdash{} b\_\mint{}\msupminus{}x (F[i;a]/r((i)!)) * t - a\^{}i dt = (F[i;a]/r((i)!))
* (x - a\^{}i + 1 - b - a\^{}i + 1/r(i + 1)) for i \mmember{} [0,n]
By
Latex:
(D 0 THEN Auto)
Home
Index