Step
*
1
1
of Lemma
equal-functions-by-Taylor
1. F : ℕ ⟶ ℝ ⟶ ℝ
2. G : ℕ ⟶ ℝ ⟶ ℝ
3. ∀k:ℕ. ∀x,y:ℝ. ((x = y) ⇒ (F[k;x] = F[k;y]))
4. ∀k:ℕ. ∀x,y:ℝ. ((x = y) ⇒ (G[k;x] = G[k;y]))
5. infinite-deriv-seq((-∞, ∞);i,x.F[i;x])
6. infinite-deriv-seq((-∞, ∞);i,x.G[i;x])
7. ∀m:ℕ. ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} . (|F[k;x]| ≤ c)
8. ∀m:ℕ. ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} . (|G[k;x]| ≤ c)
9. ∀n:ℕ. (F[n;r0] = G[n;r0])
10. x : ℝ
11. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = λx.F[0;x] for x ∈ (-∞, ∞)
12. lim k→∞.Σ{(G[i;r0]/r((i)!)) * x^i | 0≤i≤k} = λx.G[0;x] for x ∈ (-∞, ∞)
13. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = F[0;x]
14. lim k→∞.Σ{(G[i;r0]/r((i)!)) * x^i | 0≤i≤k} = G[0;x]
⊢ F[0;x] = G[0;x]
BY
{ Assert ⌜lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = G[0;x]⌝⋅ }
1
.....assertion.....
1. F : ℕ ⟶ ℝ ⟶ ℝ
2. G : ℕ ⟶ ℝ ⟶ ℝ
3. ∀k:ℕ. ∀x,y:ℝ. ((x = y) ⇒ (F[k;x] = F[k;y]))
4. ∀k:ℕ. ∀x,y:ℝ. ((x = y) ⇒ (G[k;x] = G[k;y]))
5. infinite-deriv-seq((-∞, ∞);i,x.F[i;x])
6. infinite-deriv-seq((-∞, ∞);i,x.G[i;x])
7. ∀m:ℕ. ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} . (|F[k;x]| ≤ c)
8. ∀m:ℕ. ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} . (|G[k;x]| ≤ c)
9. ∀n:ℕ. (F[n;r0] = G[n;r0])
10. x : ℝ
11. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = λx.F[0;x] for x ∈ (-∞, ∞)
12. lim k→∞.Σ{(G[i;r0]/r((i)!)) * x^i | 0≤i≤k} = λx.G[0;x] for x ∈ (-∞, ∞)
13. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = F[0;x]
14. lim k→∞.Σ{(G[i;r0]/r((i)!)) * x^i | 0≤i≤k} = G[0;x]
⊢ lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = G[0;x]
2
1. F : ℕ ⟶ ℝ ⟶ ℝ
2. G : ℕ ⟶ ℝ ⟶ ℝ
3. ∀k:ℕ. ∀x,y:ℝ. ((x = y) ⇒ (F[k;x] = F[k;y]))
4. ∀k:ℕ. ∀x,y:ℝ. ((x = y) ⇒ (G[k;x] = G[k;y]))
5. infinite-deriv-seq((-∞, ∞);i,x.F[i;x])
6. infinite-deriv-seq((-∞, ∞);i,x.G[i;x])
7. ∀m:ℕ. ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} . (|F[k;x]| ≤ c)
8. ∀m:ℕ. ∃c:ℝ. ∃N:ℕ. ∀k:{N...}. ∀x:{x:ℝ| |x| ≤ r(m)} . (|G[k;x]| ≤ c)
9. ∀n:ℕ. (F[n;r0] = G[n;r0])
10. x : ℝ
11. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = λx.F[0;x] for x ∈ (-∞, ∞)
12. lim k→∞.Σ{(G[i;r0]/r((i)!)) * x^i | 0≤i≤k} = λx.G[0;x] for x ∈ (-∞, ∞)
13. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = F[0;x]
14. lim k→∞.Σ{(G[i;r0]/r((i)!)) * x^i | 0≤i≤k} = G[0;x]
15. lim k→∞.Σ{(F[i;r0]/r((i)!)) * x^i | 0≤i≤k} = G[0;x]
⊢ F[0;x] = G[0;x]
Latex:
Latex:
1. F : \mBbbN{} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
2. G : \mBbbN{} {}\mrightarrow{} \mBbbR{} {}\mrightarrow{} \mBbbR{}
3. \mforall{}k:\mBbbN{}. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (F[k;x] = F[k;y]))
4. \mforall{}k:\mBbbN{}. \mforall{}x,y:\mBbbR{}. ((x = y) {}\mRightarrow{} (G[k;x] = G[k;y]))
5. infinite-deriv-seq((-\minfty{}, \minfty{});i,x.F[i;x])
6. infinite-deriv-seq((-\minfty{}, \minfty{});i,x.G[i;x])
7. \mforall{}m:\mBbbN{}. \mexists{}c:\mBbbR{}. \mexists{}N:\mBbbN{}. \mforall{}k:\{N...\}. \mforall{}x:\{x:\mBbbR{}| |x| \mleq{} r(m)\} . (|F[k;x]| \mleq{} c)
8. \mforall{}m:\mBbbN{}. \mexists{}c:\mBbbR{}. \mexists{}N:\mBbbN{}. \mforall{}k:\{N...\}. \mforall{}x:\{x:\mBbbR{}| |x| \mleq{} r(m)\} . (|G[k;x]| \mleq{} c)
9. \mforall{}n:\mBbbN{}. (F[n;r0] = G[n;r0])
10. x : \mBbbR{}
11. lim k\mrightarrow{}\minfty{}.\mSigma{}\{(F[i;r0]/r((i)!)) * x\^{}i | 0\mleq{}i\mleq{}k\} = \mlambda{}x.F[0;x] for x \mmember{} (-\minfty{}, \minfty{})
12. lim k\mrightarrow{}\minfty{}.\mSigma{}\{(G[i;r0]/r((i)!)) * x\^{}i | 0\mleq{}i\mleq{}k\} = \mlambda{}x.G[0;x] for x \mmember{} (-\minfty{}, \minfty{})
13. lim k\mrightarrow{}\minfty{}.\mSigma{}\{(F[i;r0]/r((i)!)) * x\^{}i | 0\mleq{}i\mleq{}k\} = F[0;x]
14. lim k\mrightarrow{}\minfty{}.\mSigma{}\{(G[i;r0]/r((i)!)) * x\^{}i | 0\mleq{}i\mleq{}k\} = G[0;x]
\mvdash{} F[0;x] = G[0;x]
By
Latex:
Assert \mkleeneopen{}lim k\mrightarrow{}\minfty{}.\mSigma{}\{(F[i;r0]/r((i)!)) * x\^{}i | 0\mleq{}i\mleq{}k\} = G[0;x]\mkleeneclose{}\mcdot{}
Home
Index