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

Definition df-tayl 23913
 Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ0 ∪ {+∞}) can/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 23911 . 2 class Tayl
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cr 9814 . . . 4 class
5 cc 9813 . . . 4 class
64, 5cpr 4127 . . 3 class {ℝ, ℂ}
72cv 1474 . . . 4 class 𝑠
8 cpm 7745 . . . 4 class pm
95, 7, 8co 6549 . . 3 class (ℂ ↑pm 𝑠)
10 vn . . . 4 setvar 𝑛
11 va . . . 4 setvar 𝑎
12 cn0 11169 . . . . 5 class 0
13 cpnf 9950 . . . . . 6 class +∞
1413csn 4125 . . . . 5 class {+∞}
1512, 14cun 3538 . . . 4 class (ℕ0 ∪ {+∞})
16 vk . . . . 5 setvar 𝑘
17 cc0 9815 . . . . . . 7 class 0
1810cv 1474 . . . . . . 7 class 𝑛
19 cicc 12049 . . . . . . 7 class [,]
2017, 18, 19co 6549 . . . . . 6 class (0[,]𝑛)
21 cz 11254 . . . . . 6 class
2220, 21cin 3539 . . . . 5 class ((0[,]𝑛) ∩ ℤ)
2316cv 1474 . . . . . . 7 class 𝑘
243cv 1474 . . . . . . . 8 class 𝑓
25 cdvn 23434 . . . . . . . 8 class D𝑛
267, 24, 25co 6549 . . . . . . 7 class (𝑠 D𝑛 𝑓)
2723, 26cfv 5804 . . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
2827cdm 5038 . . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
2916, 22, 28ciin 4456 . . . 4 class 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30 vx . . . . 5 setvar 𝑥
3130cv 1474 . . . . . . 7 class 𝑥
3231csn 4125 . . . . . 6 class {𝑥}
33 ccnfld 19567 . . . . . . 7 class fld
3411cv 1474 . . . . . . . . . . 11 class 𝑎
3534, 27cfv 5804 . . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36 cfa 12922 . . . . . . . . . . 11 class !
3723, 36cfv 5804 . . . . . . . . . 10 class (!‘𝑘)
38 cdiv 10563 . . . . . . . . . 10 class /
3935, 37, 38co 6549 . . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40 cmin 10145 . . . . . . . . . . 11 class
4131, 34, 40co 6549 . . . . . . . . . 10 class (𝑥𝑎)
42 cexp 12722 . . . . . . . . . 10 class
4341, 23, 42co 6549 . . . . . . . . 9 class ((𝑥𝑎)↑𝑘)
44 cmul 9820 . . . . . . . . 9 class ·
4539, 43, 44co 6549 . . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))
4616, 22, 45cmpt 4643 . . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))
47 ctsu 21739 . . . . . . 7 class tsums
4833, 46, 47co 6549 . . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))
4932, 48cxp 5036 . . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5030, 5, 49ciun 4455 . . . 4 class 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5110, 11, 15, 29, 50cmpt2 6551 . . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))))
522, 3, 6, 9, 51cmpt2 6551 . 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
531, 52wceq 1475 1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
 Colors of variables: wff setvar class This definition is referenced by:  taylfval  23917
 Copyright terms: Public domain W3C validator