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

Definition df-tayl 25730
Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: ๐‘› โˆˆ (โ„•0 โˆช {+โˆž}) should be replaced by ๐‘› โˆˆ โ„•0*. (Contributed by Mario Carneiro, 30-Dec-2016.)
Assertion
Ref Expression
df-tayl Tayl = (๐‘  โˆˆ {โ„, โ„‚}, ๐‘“ โˆˆ (โ„‚ โ†‘pm ๐‘ ) โ†ฆ (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))))
Distinct variable group:   ๐‘˜,๐‘Ž,๐‘›,๐‘ฅ,๐‘“,๐‘ 

Detailed syntax breakdown of Definition df-tayl
StepHypRef Expression
1 ctayl 25728 . 2 class Tayl
2 vs . . 3 setvar ๐‘ 
3 vf . . 3 setvar ๐‘“
4 cr 11057 . . . 4 class โ„
5 cc 11056 . . . 4 class โ„‚
64, 5cpr 4593 . . 3 class {โ„, โ„‚}
72cv 1541 . . . 4 class ๐‘ 
8 cpm 8773 . . . 4 class โ†‘pm
95, 7, 8co 7362 . . 3 class (โ„‚ โ†‘pm ๐‘ )
10 vn . . . 4 setvar ๐‘›
11 va . . . 4 setvar ๐‘Ž
12 cn0 12420 . . . . 5 class โ„•0
13 cpnf 11193 . . . . . 6 class +โˆž
1413csn 4591 . . . . 5 class {+โˆž}
1512, 14cun 3913 . . . 4 class (โ„•0 โˆช {+โˆž})
16 vk . . . . 5 setvar ๐‘˜
17 cc0 11058 . . . . . . 7 class 0
1810cv 1541 . . . . . . 7 class ๐‘›
19 cicc 13274 . . . . . . 7 class [,]
2017, 18, 19co 7362 . . . . . 6 class (0[,]๐‘›)
21 cz 12506 . . . . . 6 class โ„ค
2220, 21cin 3914 . . . . 5 class ((0[,]๐‘›) โˆฉ โ„ค)
2316cv 1541 . . . . . . 7 class ๐‘˜
243cv 1541 . . . . . . . 8 class ๐‘“
25 cdvn 25244 . . . . . . . 8 class D๐‘›
267, 24, 25co 7362 . . . . . . 7 class (๐‘  D๐‘› ๐‘“)
2723, 26cfv 6501 . . . . . 6 class ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)
2827cdm 5638 . . . . 5 class dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)
2916, 22, 28ciin 4960 . . . 4 class โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)
30 vx . . . . 5 setvar ๐‘ฅ
3130cv 1541 . . . . . . 7 class ๐‘ฅ
3231csn 4591 . . . . . 6 class {๐‘ฅ}
33 ccnfld 20812 . . . . . . 7 class โ„‚fld
3411cv 1541 . . . . . . . . . . 11 class ๐‘Ž
3534, 27cfv 6501 . . . . . . . . . 10 class (((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž)
36 cfa 14180 . . . . . . . . . . 11 class !
3723, 36cfv 6501 . . . . . . . . . 10 class (!โ€˜๐‘˜)
38 cdiv 11819 . . . . . . . . . 10 class /
3935, 37, 38co 7362 . . . . . . . . 9 class ((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜))
40 cmin 11392 . . . . . . . . . . 11 class โˆ’
4131, 34, 40co 7362 . . . . . . . . . 10 class (๐‘ฅ โˆ’ ๐‘Ž)
42 cexp 13974 . . . . . . . . . 10 class โ†‘
4341, 23, 42co 7362 . . . . . . . . 9 class ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)
44 cmul 11063 . . . . . . . . 9 class ยท
4539, 43, 44co 7362 . . . . . . . 8 class (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜))
4616, 22, 45cmpt 5193 . . . . . . 7 class (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))
47 ctsu 23493 . . . . . . 7 class tsums
4833, 46, 47co 7362 . . . . . 6 class (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜))))
4932, 48cxp 5636 . . . . 5 class ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))
5030, 5, 49ciun 4959 . . . 4 class โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))
5110, 11, 15, 29, 50cmpo 7364 . . 3 class (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜))))))
522, 3, 6, 9, 51cmpo 7364 . 2 class (๐‘  โˆˆ {โ„, โ„‚}, ๐‘“ โˆˆ (โ„‚ โ†‘pm ๐‘ ) โ†ฆ (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))))
531, 52wceq 1542 1 wff Tayl = (๐‘  โˆˆ {โ„, โ„‚}, ๐‘“ โˆˆ (โ„‚ โ†‘pm ๐‘ ) โ†ฆ (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))))
Colors of variables: wff setvar class
This definition is referenced by:  taylfval  25734
  Copyright terms: Public domain W3C validator