Definition df-tayl 24109

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

Assertion

Ref	Expression
df-tayl	|- Tayl = ( s e. { RR , CC } , f e. ( CC ^pm s ) |-> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )

Distinct variable group:   k, a, n, x, f, s

Detailed syntax breakdown of Definition df-tayl

Step	Hyp	Ref	Expression
1		ctayl 24107	. 2 class Tayl
2		vs	. . 3 setvar s
3		vf	. . 3 setvar f
4		cr 9935	. . . 4 class RR
5		cc 9934	. . . 4 class CC
6	4, 5	cpr 4179	. . 3 class { RR , CC }
7	2	cv 1482	. . . 4 class s
8		cpm 7858	. . . 4 class ^pm
9	5, 7, 8	co 6650	. . 3 class ( CC ^pm s )
10		vn	. . . 4 setvar n
11		va	. . . 4 setvar a
12		cn0 11292	. . . . 5 class NN0
13		cpnf 10071	. . . . . 6 class +oo
14	13	csn 4177	. . . . 5 class { +oo }
15	12, 14	cun 3572	. . . 4 class ( NN0 u. { +oo } )
16		vk	. . . . 5 setvar k
17		cc0 9936	. . . . . . 7 class 0
18	10	cv 1482	. . . . . . 7 class n
19		cicc 12178	. . . . . . 7 class [,]
20	17, 18, 19	co 6650	. . . . . 6 class ( 0 [,] n )
21		cz 11377	. . . . . 6 class ZZ
22	20, 21	cin 3573	. . . . 5 class ( ( 0 [,] n ) i^i ZZ )
23	16	cv 1482	. . . . . . 7 class k
24	3	cv 1482	. . . . . . . 8 class f
25		cdvn 23628	. . . . . . . 8 class Dn
26	7, 24, 25	co 6650	. . . . . . 7 class ( s Dn f )
27	23, 26	cfv 5888	. . . . . 6 class ( ( s Dn f ) ` k )
28	27	cdm 5114	. . . . 5 class dom ( ( s Dn f ) ` k )
29	16, 22, 28	ciin 4521	. . . 4 class |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k )
30		vx	. . . . 5 setvar x
31	30	cv 1482	. . . . . . 7 class x
32	31	csn 4177	. . . . . 6 class { x }
33		ccnfld 19746	. . . . . . 7 class ℂfld
34	11	cv 1482	. . . . . . . . . . 11 class a
35	34, 27	cfv 5888	. . . . . . . . . 10 class ( ( ( s Dn f ) ` k ) ` a )
36		cfa 13060	. . . . . . . . . . 11 class !
37	23, 36	cfv 5888	. . . . . . . . . 10 class ( ! ` k )
38		cdiv 10684	. . . . . . . . . 10 class /
39	35, 37, 38	co 6650	. . . . . . . . 9 class ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) )
40		cmin 10266	. . . . . . . . . . 11 class -
41	31, 34, 40	co 6650	. . . . . . . . . 10 class ( x - a )
42		cexp 12860	. . . . . . . . . 10 class ^
43	41, 23, 42	co 6650	. . . . . . . . 9 class ( ( x - a ) ^ k )
44		cmul 9941	. . . . . . . . 9 class x.
45	39, 43, 44	co 6650	. . . . . . . 8 class ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) )
46	16, 22, 45	cmpt 4729	. . . . . . 7 class ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) )
47		ctsu 21929	. . . . . . 7 class tsums
48	33, 46, 47	co 6650	. . . . . 6 class (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) )
49	32, 48	cxp 5112	. . . . 5 class ( { x } X. (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) )
50	30, 5, 49	ciun 4520	. . . 4 class U_ x e. CC ( { x } X. (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) )
51	10, 11, 15, 29, 50	cmpt2 6652	. . 3 class ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) )
52	2, 3, 6, 9, 51	cmpt2 6652	. 2 class ( s e. { RR , CC } , f e. ( CC ^pm s ) |-> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )
53	1, 52	wceq 1483	1 wff Tayl = ( s e. { RR , CC } , f e. ( CC ^pm s ) |-> ( n e. ( NN0 u. { +oo } ) , a e. |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k ) |-> U_ x e. CC ( { x } X. (ℂfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )

This definition is referenced by:  taylfval  24113