Definition df-tayl

Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: n e. ( NN0 u. { +oo } ) should be replaced by n e. NN0* . (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Assertion	df-tayl	⊢ Tayl = ( 𝑠 ∈ { ℝ , ℂ } , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ( 𝑛 ∈ ( ℕ0 ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctayl	⊢ Tayl
1		vs	⊢ 𝑠
2		cr	⊢ ℝ
3		cc	⊢ ℂ
4	2 3	cpr	⊢ { ℝ , ℂ }
5		vf	⊢ 𝑓
6		cpm	⊢ ↑pm
7	1	cv	⊢ 𝑠
8	3 7 6	co	⊢ ( ℂ ↑pm 𝑠 )
9		vn	⊢ 𝑛
10		cn0	⊢ ℕ0
11		cpnf	⊢ +∞
12	11	csn	⊢ { +∞ }
13	10 12	cun	⊢ ( ℕ0 ∪ { +∞ } )
14		va	⊢ 𝑎
15		vk	⊢ 𝑘
16		cc0	⊢ 0
17		cicc	⊢ [,]
18	9	cv	⊢ 𝑛
19	16 18 17	co	⊢ ( 0 [,] 𝑛 )
20		cz	⊢ ℤ
21	19 20	cin	⊢ ( ( 0 [,] 𝑛 ) ∩ ℤ )
22		cdvn	⊢ D𝑛
23	5	cv	⊢ 𝑓
24	7 23 22	co	⊢ ( 𝑠 D𝑛 𝑓 )
25	15	cv	⊢ 𝑘
26	25 24	cfv	⊢ ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 )
27	26	cdm	⊢ dom ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 )
28	15 21 27	ciin	⊢ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 )
29		vx	⊢ 𝑥
30	29	cv	⊢ 𝑥
31	30	csn	⊢ { 𝑥 }
32		ccnfld	⊢ ℂfld
33		ctsu	⊢ tsums
34	14	cv	⊢ 𝑎
35	34 26	cfv	⊢ ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 )
36		cdiv	⊢ /
37		cfa	⊢ !
38	25 37	cfv	⊢ ( ! ‘ 𝑘 )
39	35 38 36	co	⊢ ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) )
40		cmul	⊢ ·
41		cmin	⊢ −
42	30 34 41	co	⊢ ( 𝑥 − 𝑎 )
43		cexp	⊢ ↑
44	42 25 43	co	⊢ ( ( 𝑥 − 𝑎 ) ↑ 𝑘 )
45	39 44 40	co	⊢ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) )
46	15 21 45	cmpt	⊢ ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) )
47	32 46 33	co	⊢ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) )
48	31 47	cxp	⊢ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) )
49	29 3 48	ciun	⊢ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) )
50	9 14 13 28 49	cmpo	⊢ ( 𝑛 ∈ ( ℕ0 ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) )
51	1 5 4 8 50	cmpo	⊢ ( 𝑠 ∈ { ℝ , ℂ } , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ( 𝑛 ∈ ( ℕ0 ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) )
52	0 51	wceq	⊢ Tayl = ( 𝑠 ∈ { ℝ , ℂ } , 𝑓 ∈ ( ℂ ↑pm 𝑠 ) ↦ ( 𝑛 ∈ ( ℕ0 ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) )