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 25866
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 25864 . 2 class Tayl
2 vs . . 3 setvar ๐‘ 
3 vf . . 3 setvar ๐‘“
4 cr 11108 . . . 4 class โ„
5 cc 11107 . . . 4 class โ„‚
64, 5cpr 4630 . . 3 class {โ„, โ„‚}
72cv 1540 . . . 4 class ๐‘ 
8 cpm 8820 . . . 4 class โ†‘pm
95, 7, 8co 7408 . . 3 class (โ„‚ โ†‘pm ๐‘ )
10 vn . . . 4 setvar ๐‘›
11 va . . . 4 setvar ๐‘Ž
12 cn0 12471 . . . . 5 class โ„•0
13 cpnf 11244 . . . . . 6 class +โˆž
1413csn 4628 . . . . 5 class {+โˆž}
1512, 14cun 3946 . . . 4 class (โ„•0 โˆช {+โˆž})
16 vk . . . . 5 setvar ๐‘˜
17 cc0 11109 . . . . . . 7 class 0
1810cv 1540 . . . . . . 7 class ๐‘›
19 cicc 13326 . . . . . . 7 class [,]
2017, 18, 19co 7408 . . . . . 6 class (0[,]๐‘›)
21 cz 12557 . . . . . 6 class โ„ค
2220, 21cin 3947 . . . . 5 class ((0[,]๐‘›) โˆฉ โ„ค)
2316cv 1540 . . . . . . 7 class ๐‘˜
243cv 1540 . . . . . . . 8 class ๐‘“
25 cdvn 25380 . . . . . . . 8 class D๐‘›
267, 24, 25co 7408 . . . . . . 7 class (๐‘  D๐‘› ๐‘“)
2723, 26cfv 6543 . . . . . 6 class ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)
2827cdm 5676 . . . . 5 class dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)
2916, 22, 28ciin 4998 . . . 4 class โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)
30 vx . . . . 5 setvar ๐‘ฅ
3130cv 1540 . . . . . . 7 class ๐‘ฅ
3231csn 4628 . . . . . 6 class {๐‘ฅ}
33 ccnfld 20943 . . . . . . 7 class โ„‚fld
3411cv 1540 . . . . . . . . . . 11 class ๐‘Ž
3534, 27cfv 6543 . . . . . . . . . 10 class (((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž)
36 cfa 14232 . . . . . . . . . . 11 class !
3723, 36cfv 6543 . . . . . . . . . 10 class (!โ€˜๐‘˜)
38 cdiv 11870 . . . . . . . . . 10 class /
3935, 37, 38co 7408 . . . . . . . . 9 class ((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜))
40 cmin 11443 . . . . . . . . . . 11 class โˆ’
4131, 34, 40co 7408 . . . . . . . . . 10 class (๐‘ฅ โˆ’ ๐‘Ž)
42 cexp 14026 . . . . . . . . . 10 class โ†‘
4341, 23, 42co 7408 . . . . . . . . 9 class ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)
44 cmul 11114 . . . . . . . . 9 class ยท
4539, 43, 44co 7408 . . . . . . . 8 class (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜))
4616, 22, 45cmpt 5231 . . . . . . 7 class (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))
47 ctsu 23629 . . . . . . 7 class tsums
4833, 46, 47co 7408 . . . . . 6 class (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜))))
4932, 48cxp 5674 . . . . 5 class ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))
5030, 5, 49ciun 4997 . . . 4 class โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))
5110, 11, 15, 29, 50cmpo 7410 . . 3 class (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜))))))
522, 3, 6, 9, 51cmpo 7410 . 2 class (๐‘  โˆˆ {โ„, โ„‚}, ๐‘“ โˆˆ (โ„‚ โ†‘pm ๐‘ ) โ†ฆ (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))))
531, 52wceq 1541 1 wff Tayl = (๐‘  โˆˆ {โ„, โ„‚}, ๐‘“ โˆˆ (โ„‚ โ†‘pm ๐‘ ) โ†ฆ (๐‘› โˆˆ (โ„•0 โˆช {+โˆž}), ๐‘Ž โˆˆ โˆฉ ๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค)dom ((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜) โ†ฆ โˆช ๐‘ฅ โˆˆ โ„‚ ({๐‘ฅ} ร— (โ„‚fld tsums (๐‘˜ โˆˆ ((0[,]๐‘›) โˆฉ โ„ค) โ†ฆ (((((๐‘  D๐‘› ๐‘“)โ€˜๐‘˜)โ€˜๐‘Ž) / (!โ€˜๐‘˜)) ยท ((๐‘ฅ โˆ’ ๐‘Ž)โ†‘๐‘˜)))))))
Colors of variables: wff setvar class
This definition is referenced by:  taylfval  25870
  Copyright terms: Public domain W3C validator