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

Definition df-tayl 19750
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 19748 . 2  class Tayl
2 vs . . 3  set  s
3 vf . . 3  set  f
4 cr 8752 . . . 4  class  RR
5 cc 8751 . . . 4  class  CC
64, 5cpr 3654 . . 3  class  { RR ,  CC }
72cv 1631 . . . 4  class  s
8 cpm 6789 . . . 4  class  ^pm
95, 7, 8co 5874 . . 3  class  ( CC 
^pm  s )
10 vn . . . 4  set  n
11 va . . . 4  set  a
12 cn0 9981 . . . . 5  class  NN0
13 cpnf 8880 . . . . . 6  class  +oo
1413csn 3653 . . . . 5  class  {  +oo }
1512, 14cun 3163 . . . 4  class  ( NN0 
u.  {  +oo } )
16 vk . . . . 5  set  k
17 cc0 8753 . . . . . . 7  class  0
1810cv 1631 . . . . . . 7  class  n
19 cicc 10675 . . . . . . 7  class  [,]
2017, 18, 19co 5874 . . . . . 6  class  ( 0 [,] n )
21 cz 10040 . . . . . 6  class  ZZ
2220, 21cin 3164 . . . . 5  class  ( ( 0 [,] n )  i^i  ZZ )
2316cv 1631 . . . . . . 7  class  k
243cv 1631 . . . . . . . 8  class  f
25 cdvn 19230 . . . . . . . 8  class  D n
267, 24, 25co 5874 . . . . . . 7  class  ( s  D n f )
2723, 26cfv 5271 . . . . . 6  class  ( ( s  D n f ) `  k )
2827cdm 4705 . . . . 5  class  dom  (
( s  D n
f ) `  k
)
2916, 22, 28ciin 3922 . . . 4  class  |^|_ k  e.  ( ( 0 [,] n )  i^i  ZZ ) dom  ( ( s  D n f ) `
 k )
30 vx . . . . 5  set  x
3130cv 1631 . . . . . . 7  class  x
3231csn 3653 . . . . . 6  class  { x }
33 ccnfld 16393 . . . . . . 7  classfld
3411cv 1631 . . . . . . . . . . 11  class  a
3534, 27cfv 5271 . . . . . . . . . 10  class  ( ( ( s  D n
f ) `  k
) `  a )
36 cfa 11304 . . . . . . . . . . 11  class  !
3723, 36cfv 5271 . . . . . . . . . 10  class  ( ! `
 k )
38 cdiv 9439 . . . . . . . . . 10  class  /
3935, 37, 38co 5874 . . . . . . . . 9  class  ( ( ( ( s  D n f ) `  k ) `  a
)  /  ( ! `
 k ) )
40 cmin 9053 . . . . . . . . . . 11  class  -
4131, 34, 40co 5874 . . . . . . . . . 10  class  ( x  -  a )
42 cexp 11120 . . . . . . . . . 10  class  ^
4341, 23, 42co 5874 . . . . . . . . 9  class  ( ( x  -  a ) ^ k )
44 cmul 8758 . . . . . . . . 9  class  x.
4539, 43, 44co 5874 . . . . . . . 8  class  ( ( ( ( ( s  D n f ) `
 k ) `  a )  /  ( ! `  k )
)  x.  ( ( x  -  a ) ^ k ) )
4616, 22, 45cmpt 4093 . . . . . . 7  class  ( k  e.  ( ( 0 [,] n )  i^i 
ZZ )  |->  ( ( ( ( ( s  D n f ) `
 k ) `  a )  /  ( ! `  k )
)  x.  ( ( x  -  a ) ^ k ) ) )
47 ctsu 17824 . . . . . . 7  class tsums
4833, 46, 47co 5874 . . . . . 6  class  (fld tsums  ( k  e.  ( ( 0 [,] n )  i^i  ZZ )  |->  ( ( ( ( ( s  D n f ) `  k ) `  a
)  /  ( ! `
 k ) )  x.  ( ( x  -  a ) ^
k ) ) ) )
4932, 48cxp 4703 . . . . 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 3921 . . . 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 5876 . . 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 5876 . 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 1632 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  19754
  Copyright terms: Public domain W3C validator