MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tayl Unicode version

Definition df-tayl 19734
Description: Define the Taylor polynomial or Taylor series of a function. (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  D n f ) `  k )  |->  U_ x  e.  CC  ( { x }  X.  (fld tsums 
( k  e.  ( ( 0 [,] n
)  i^i  ZZ )  |->  ( ( ( ( ( s  D n
f ) `  k
) `  a )  /  ( ! `  k ) )  x.  ( ( x  -  a ) ^ k
) ) ) ) ) ) )
Distinct variable group:    k, a, n, x, f, s

Detailed syntax breakdown of Definition df-tayl
StepHypRef Expression
1 ctayl 19732 . 2  class Tayl
2 vs . . 3  set  s
3 vf . . 3  set  f
4 cr 8736 . . . 4  class  RR
5 cc 8735 . . . 4  class  CC
64, 5cpr 3641 . . 3  class  { RR ,  CC }
72cv 1622 . . . 4  class  s
8 cpm 6773 . . . 4  class  ^pm
95, 7, 8co 5858 . . 3  class  ( CC 
^pm  s )
10 vn . . . 4  set  n
11 va . . . 4  set  a
12 cn0 9965 . . . . 5  class  NN0
13 cpnf 8864 . . . . . 6  class  +oo
1413csn 3640 . . . . 5  class  {  +oo }
1512, 14cun 3150 . . . 4  class  ( NN0 
u.  {  +oo } )
16 vk . . . . 5  set  k
17 cc0 8737 . . . . . . 7  class  0
1810cv 1622 . . . . . . 7  class  n
19 cicc 10659 . . . . . . 7  class  [,]
2017, 18, 19co 5858 . . . . . 6  class  ( 0 [,] n )
21 cz 10024 . . . . . 6  class  ZZ
2220, 21cin 3151 . . . . 5  class  ( ( 0 [,] n )  i^i  ZZ )
2316cv 1622 . . . . . . 7  class  k
243cv 1622 . . . . . . . 8  class  f
25 cdvn 19214 . . . . . . . 8  class  D n
267, 24, 25co 5858 . . . . . . 7  class  ( s  D n f )
2723, 26cfv 5255 . . . . . 6  class  ( ( s  D n f ) `  k )
2827cdm 4689 . . . . 5  class  dom  (
( s  D n
f ) `  k
)
2916, 22, 28ciin 3906 . . . 4  class  |^|_ k  e.  ( ( 0 [,] n )  i^i  ZZ ) dom  ( ( s  D n f ) `
 k )
30 vx . . . . 5  set  x
3130cv 1622 . . . . . . 7  class  x
3231csn 3640 . . . . . 6  class  { x }
33 ccnfld 16377 . . . . . . 7  classfld
3411cv 1622 . . . . . . . . . . 11  class  a
3534, 27cfv 5255 . . . . . . . . . 10  class  ( ( ( s  D n
f ) `  k
) `  a )
36 cfa 11288 . . . . . . . . . . 11  class  !
3723, 36cfv 5255 . . . . . . . . . 10  class  ( ! `
 k )
38 cdiv 9423 . . . . . . . . . 10  class  /
3935, 37, 38co 5858 . . . . . . . . 9  class  ( ( ( ( s  D n f ) `  k ) `  a
)  /  ( ! `
 k ) )
40 cmin 9037 . . . . . . . . . . 11  class  -
4131, 34, 40co 5858 . . . . . . . . . 10  class  ( x  -  a )
42 cexp 11104 . . . . . . . . . 10  class  ^
4341, 23, 42co 5858 . . . . . . . . 9  class  ( ( x  -  a ) ^ k )
44 cmul 8742 . . . . . . . . 9  class  x.
4539, 43, 44co 5858 . . . . . . . 8  class  ( ( ( ( ( s  D n f ) `
 k ) `  a )  /  ( ! `  k )
)  x.  ( ( x  -  a ) ^ k ) )
4616, 22, 45cmpt 4077 . . . . . . 7  class  ( k  e.  ( ( 0 [,] n )  i^i 
ZZ )  |->  ( ( ( ( ( s  D n f ) `
 k ) `  a )  /  ( ! `  k )
)  x.  ( ( x  -  a ) ^ k ) ) )
47 ctsu 17808 . . . . . . 7  class tsums
4833, 46, 47co 5858 . . . . . 6  class  (fld tsums  ( k  e.  ( ( 0 [,] n )  i^i  ZZ )  |->  ( ( ( ( ( s  D n f ) `  k ) `  a
)  /  ( ! `
 k ) )  x.  ( ( x  -  a ) ^
k ) ) ) )
4932, 48cxp 4687 . . . . 5  class  ( { x }  X.  (fld tsums  ( k  e.  ( ( 0 [,] n )  i^i 
ZZ )  |->  ( ( ( ( ( s  D n f ) `
 k ) `  a )  /  ( ! `  k )
)  x.  ( ( x  -  a ) ^ k ) ) ) ) )
5030, 5, 49ciun 3905 . . . 4  class  U_ x  e.  CC  ( { x }  X.  (fld tsums 
( k  e.  ( ( 0 [,] n
)  i^i  ZZ )  |->  ( ( ( ( ( s  D n
f ) `  k
) `  a )  /  ( ! `  k ) )  x.  ( ( x  -  a ) ^ k
) ) ) ) )
5110, 11, 15, 29, 50cmpt2 5860 . . 3  class  ( n  e.  ( NN0  u.  { 
+oo } ) ,  a  e.  |^|_ k  e.  ( ( 0 [,] n
)  i^i  ZZ ) dom  ( ( s  D n f ) `  k )  |->  U_ x  e.  CC  ( { x }  X.  (fld tsums 
( k  e.  ( ( 0 [,] n
)  i^i  ZZ )  |->  ( ( ( ( ( s  D n
f ) `  k
) `  a )  /  ( ! `  k ) )  x.  ( ( x  -  a ) ^ k
) ) ) ) ) )
522, 3, 6, 9, 51cmpt2 5860 . 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  D n f ) `  k )  |->  U_ x  e.  CC  ( { x }  X.  (fld tsums 
( k  e.  ( ( 0 [,] n
)  i^i  ZZ )  |->  ( ( ( ( ( s  D n
f ) `  k
) `  a )  /  ( ! `  k ) )  x.  ( ( x  -  a ) ^ k
) ) ) ) ) ) )
531, 52wceq 1623 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  D n f ) `  k )  |->  U_ x  e.  CC  ( { x }  X.  (fld tsums 
( k  e.  ( ( 0 [,] n
)  i^i  ZZ )  |->  ( ( ( ( ( s  D n
f ) `  k
) `  a )  /  ( ! `  k ) )  x.  ( ( x  -  a ) ^ k
) ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  taylfval  19738
  Copyright terms: Public domain W3C validator