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

Definition df-tayl 21779
 Description: Define the Taylor polynomial or Taylor series of a function. (Contributed by Mario Carneiro, 30-Dec-2016.)
Assertion
Ref Expression
df-tayl Tayl fld tsums
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-tayl
StepHypRef Expression
1 ctayl 21777 . 2 Tayl
2 vs . . 3
3 vf . . 3
4 cr 9277 . . . 4
5 cc 9276 . . . 4
64, 5cpr 3876 . . 3
72cv 1363 . . . 4
8 cpm 7211 . . . 4
95, 7, 8co 6090 . . 3
10 vn . . . 4
11 va . . . 4
12 cn0 10575 . . . . 5
13 cpnf 9411 . . . . . 6
1413csn 3874 . . . . 5
1512, 14cun 3323 . . . 4
16 vk . . . . 5
17 cc0 9278 . . . . . . 7
1810cv 1363 . . . . . . 7
19 cicc 11299 . . . . . . 7
2017, 18, 19co 6090 . . . . . 6
21 cz 10642 . . . . . 6
2220, 21cin 3324 . . . . 5
2316cv 1363 . . . . . . 7
243cv 1363 . . . . . . . 8
25 cdvn 21298 . . . . . . . 8
267, 24, 25co 6090 . . . . . . 7
2723, 26cfv 5415 . . . . . 6
2827cdm 4836 . . . . 5
2916, 22, 28ciin 4169 . . . 4
30 vx . . . . 5
3130cv 1363 . . . . . . 7
3231csn 3874 . . . . . 6
33 ccnfld 17777 . . . . . . 7 fld
3411cv 1363 . . . . . . . . . . 11
3534, 27cfv 5415 . . . . . . . . . 10
36 cfa 12047 . . . . . . . . . . 11
3723, 36cfv 5415 . . . . . . . . . 10
38 cdiv 9989 . . . . . . . . . 10
3935, 37, 38co 6090 . . . . . . . . 9
40 cmin 9591 . . . . . . . . . . 11
4131, 34, 40co 6090 . . . . . . . . . 10
42 cexp 11861 . . . . . . . . . 10
4341, 23, 42co 6090 . . . . . . . . 9
44 cmul 9283 . . . . . . . . 9
4539, 43, 44co 6090 . . . . . . . 8
4616, 22, 45cmpt 4347 . . . . . . 7
47 ctsu 19655 . . . . . . 7 tsums
4833, 46, 47co 6090 . . . . . 6 fld tsums
4932, 48cxp 4834 . . . . 5 fld tsums
5030, 5, 49ciun 4168 . . . 4 fld tsums
5110, 11, 15, 29, 50cmpt2 6092 . . 3 fld tsums
522, 3, 6, 9, 51cmpt2 6092 . 2 fld tsums
531, 52wceq 1364 1 Tayl fld tsums
 Colors of variables: wff setvar class This definition is referenced by:  taylfval  21783
 Copyright terms: Public domain W3C validator