Metamath Proof Explorer

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 = ( 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. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctayl 
 |-  Tayl
1 vs 
 |-  s
2 cr 
 |-  RR
3 cc 
 |-  CC
4 2 3 cpr 
 |-  { RR , CC }
5 vf 
 |-  f
6 cpm 
 |-  ^pm
7 1 cv 
 |-  s
8 3 7 6 co 
 |-  ( CC ^pm s )
9 vn 
 |-  n
10 cn0 
 |-  NN0
11 cpnf 
 |-  +oo
12 11 csn 
 |-  { +oo }
13 10 12 cun 
 |-  ( NN0 u. { +oo } )
14 va 
 |-  a
15 vk 
 |-  k
16 cc0 
 |-  0
17 cicc 
 |-  [,]
18 9 cv 
 |-  n
19 16 18 17 co 
 |-  ( 0 [,] n )
20 cz 
 |-  ZZ
21 19 20 cin 
 |-  ( ( 0 [,] n ) i^i ZZ )
22 cdvn 
 |-  Dn
23 5 cv 
 |-  f
24 7 23 22 co 
 |-  ( s Dn f )
25 15 cv 
 |-  k
26 25 24 cfv 
 |-  ( ( s Dn f ) ` k )
27 26 cdm 
 |-  dom ( ( s Dn f ) ` k )
28 15 21 27 ciin 
 |-  |^|_ k e. ( ( 0 [,] n ) i^i ZZ ) dom ( ( s Dn f ) ` k )
29 vx 
 |-  x
30 29 cv 
 |-  x
31 30 csn 
 |-  { x }
32 ccnfld 
 |-  CCfld
33 ctsu 
 |-  tsums
34 14 cv 
 |-  a
35 34 26 cfv 
 |-  ( ( ( s Dn f ) ` k ) ` a )
36 cdiv 
 |-  /
37 cfa 
 |-  !
38 25 37 cfv 
 |-  ( ! ` k )
39 35 38 36 co 
 |-  ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) )
40 cmul 
 |-  x.
41 cmin 
 |-  -
42 30 34 41 co 
 |-  ( x - a )
43 cexp 
 |-  ^
44 42 25 43 co 
 |-  ( ( x - a ) ^ k )
45 39 44 40 co 
 |-  ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) )
46 15 21 45 cmpt 
 |-  ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) )
47 32 46 33 co 
 |-  ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) )
48 31 47 cxp 
 |-  ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) )
49 29 3 48 ciun 
 |-  U_ x e. CC ( { x } X. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) )
50 9 14 13 28 49 cmpo 
 |-  ( 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. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) )
51 1 5 4 8 50 cmpo 
 |-  ( 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. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )
52 0 51 wceq 
 |-  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. ( CCfld tsums ( k e. ( ( 0 [,] n ) i^i ZZ ) |-> ( ( ( ( ( s Dn f ) ` k ) ` a ) / ( ! ` k ) ) x. ( ( x - a ) ^ k ) ) ) ) ) ) )