Step
*
1
1
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)
12. i : ℕn + 1
⊢ ifun(λx.λi,t. ((F[i;a]/r((i)!)) * t - a^i)[i;x];[rmin(b;x), rmax(b;x)])
BY
{ ((RepUR ``so_apply`` 0 THEN D 0 THEN Auto) THEN Reduce 0) }
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 : ℕn + 1
13. x@0 : {x@0:ℝ| x@0 ∈ [left-endpoint([rmin(b;x), rmax(b;x)]), right-endpoint([rmin(b;x), rmax(b;x)])]}
14. y : {x@0:ℝ| x@0 ∈ [left-endpoint([rmin(b;x), rmax(b;x)]), right-endpoint([rmin(b;x), rmax(b;x)])]}
15. x@0 = y
⊢ ((F i a/r((i)!)) * x@0 - a^i) = ((F i a/r((i)!)) * y - a^i)
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)
12. i : \mBbbN{}n + 1
\mvdash{} ifun(\mlambda{}x.\mlambda{}i,t. ((F[i;a]/r((i)!)) * t - a\^{}i)[i;x];[rmin(b;x), rmax(b;x)])
By
Latex:
((RepUR ``so\_apply`` 0 THEN D 0 THEN Auto) THEN Reduce 0)
Home
Index