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

Definition df-tayl 20263
 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 20261 . 2 Tayl
2 vs . . 3
3 vf . . 3
4 cr 8981 . . . 4
5 cc 8980 . . . 4
64, 5cpr 3807 . . 3
72cv 1651 . . . 4
8 cpm 7011 . . . 4
95, 7, 8co 6073 . . 3
10 vn . . . 4
11 va . . . 4
12 cn0 10213 . . . . 5
13 cpnf 9109 . . . . . 6
1413csn 3806 . . . . 5
1512, 14cun 3310 . . . 4
16 vk . . . . 5
17 cc0 8982 . . . . . . 7
1810cv 1651 . . . . . . 7
19 cicc 10911 . . . . . . 7
2017, 18, 19co 6073 . . . . . 6
21 cz 10274 . . . . . 6
2220, 21cin 3311 . . . . 5
2316cv 1651 . . . . . . 7
243cv 1651 . . . . . . . 8
25 cdvn 19743 . . . . . . . 8
267, 24, 25co 6073 . . . . . . 7
2723, 26cfv 5446 . . . . . 6
2827cdm 4870 . . . . 5
2916, 22, 28ciin 4086 . . . 4
30 vx . . . . 5
3130cv 1651 . . . . . . 7
3231csn 3806 . . . . . 6
33 ccnfld 16695 . . . . . . 7 fld
3411cv 1651 . . . . . . . . . . 11
3534, 27cfv 5446 . . . . . . . . . 10
36 cfa 11558 . . . . . . . . . . 11
3723, 36cfv 5446 . . . . . . . . . 10
38 cdiv 9669 . . . . . . . . . 10
3935, 37, 38co 6073 . . . . . . . . 9
40 cmin 9283 . . . . . . . . . . 11
4131, 34, 40co 6073 . . . . . . . . . 10
42 cexp 11374 . . . . . . . . . 10
4341, 23, 42co 6073 . . . . . . . . 9
44 cmul 8987 . . . . . . . . 9
4539, 43, 44co 6073 . . . . . . . 8
4616, 22, 45cmpt 4258 . . . . . . 7
47 ctsu 18147 . . . . . . 7 tsums
4833, 46, 47co 6073 . . . . . 6 fld tsums
4932, 48cxp 4868 . . . . 5 fld tsums
5030, 5, 49ciun 4085 . . . 4 fld tsums
5110, 11, 15, 29, 50cmpt2 6075 . . 3 fld tsums
522, 3, 6, 9, 51cmpt2 6075 . 2 fld tsums
531, 52wceq 1652 1 Tayl fld tsums
 Colors of variables: wff set class This definition is referenced by:  taylfval  20267
 Copyright terms: Public domain W3C validator