Theorem taylpfval

Description: Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: S is the base set with respect to evaluate the derivatives (generally RR or CC ), F is the function we are approximating, at point B , to order N . The result is a polynomial function of x . (Contributed by Mario Carneiro, 31-Dec-2016)

	Ref	Expression
Hypotheses	taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
	taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion	taylpfval	⊢ ( 𝜑 → 𝑇 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylpfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylpfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylpfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
5		taylpfval.b	⊢ ( 𝜑 → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) )
6		taylpfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7	4	orcd	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
8	1 2 3 4 5	taylplem1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
9	1 2 3 7 8 6	taylfval	⊢ ( 𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
10		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
11		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
12		cnring	⊢ ℂfld ∈ Ring
13		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
14	12 13	mp1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ℂfld ∈ CMnd )
15		cnfldtps	⊢ ℂfld ∈ TopSp
16	15	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ℂfld ∈ TopSp )
17		ovex	⊢ ( 0 [,] 𝑁 ) ∈ V
18	17	inex1	⊢ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V
19	18	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V )
20	1 2 3 7 8	taylfvallem1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
21	20	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) : ( ( 0 [,] 𝑁 ) ∩ ℤ ) ⟶ ℂ )
22		eqid	⊢ ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
23		0z	⊢ 0 ∈ ℤ
24	4	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
25		fzval2	⊢ ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 ... 𝑁 ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
26	23 24 25	sylancr	⊢ ( 𝜑 → ( 0 ... 𝑁 ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 ... 𝑁 ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
28		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 ... 𝑁 ) ∈ Fin )
29	27 28	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ Fin )
30		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ∈ V )
31		c0ex	⊢ 0 ∈ V
32	31	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 0 ∈ V )
33	22 29 30 32	fsuppmptdm	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) finSupp 0 )
34		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
35	34	cnfldhaus	⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
36	35	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( TopOpen ‘ ℂfld ) ∈ Haus )
37	10 11 14 16 19 21 33 34 36	haustsmsid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = { ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) } )
38	29 20	gsumfsum	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
39	27	sumeq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
40	38 39	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
41	40	sneqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → { ( ℂfld Σg ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) } = { Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) } )
42	37 41	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) = { Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) } )
43	42	xpeq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) = ( { 𝑥 } × { Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) } ) )
44	43	iuneq2dv	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × { Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) } ) )
45	9 44	eqtrd	⊢ ( 𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × { Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) } ) )
46		dfmpt3	⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × { Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) } )
47	45 46	eqtr4di	⊢ ( 𝜑 → 𝑇 = ( 𝑥 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )