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 24870
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 24868 . 2 class Tayl
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cr 10524 . . . 4 class
5 cc 10523 . . . 4 class
64, 5cpr 4559 . . 3 class {ℝ, ℂ}
72cv 1527 . . . 4 class 𝑠
8 cpm 8396 . . . 4 class pm
95, 7, 8co 7145 . . 3 class (ℂ ↑pm 𝑠)
10 vn . . . 4 setvar 𝑛
11 va . . . 4 setvar 𝑎
12 cn0 11885 . . . . 5 class 0
13 cpnf 10660 . . . . . 6 class +∞
1413csn 4557 . . . . 5 class {+∞}
1512, 14cun 3931 . . . 4 class (ℕ0 ∪ {+∞})
16 vk . . . . 5 setvar 𝑘
17 cc0 10525 . . . . . . 7 class 0
1810cv 1527 . . . . . . 7 class 𝑛
19 cicc 12729 . . . . . . 7 class [,]
2017, 18, 19co 7145 . . . . . 6 class (0[,]𝑛)
21 cz 11969 . . . . . 6 class
2220, 21cin 3932 . . . . 5 class ((0[,]𝑛) ∩ ℤ)
2316cv 1527 . . . . . . 7 class 𝑘
243cv 1527 . . . . . . . 8 class 𝑓
25 cdvn 24389 . . . . . . . 8 class D𝑛
267, 24, 25co 7145 . . . . . . 7 class (𝑠 D𝑛 𝑓)
2723, 26cfv 6348 . . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
2827cdm 5548 . . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
2916, 22, 28ciin 4911 . . . 4 class 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30 vx . . . . 5 setvar 𝑥
3130cv 1527 . . . . . . 7 class 𝑥
3231csn 4557 . . . . . 6 class {𝑥}
33 ccnfld 20473 . . . . . . 7 class fld
3411cv 1527 . . . . . . . . . . 11 class 𝑎
3534, 27cfv 6348 . . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36 cfa 13621 . . . . . . . . . . 11 class !
3723, 36cfv 6348 . . . . . . . . . 10 class (!‘𝑘)
38 cdiv 11285 . . . . . . . . . 10 class /
3935, 37, 38co 7145 . . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40 cmin 10858 . . . . . . . . . . 11 class
4131, 34, 40co 7145 . . . . . . . . . 10 class (𝑥𝑎)
42 cexp 13417 . . . . . . . . . 10 class
4341, 23, 42co 7145 . . . . . . . . 9 class ((𝑥𝑎)↑𝑘)
44 cmul 10530 . . . . . . . . 9 class ·
4539, 43, 44co 7145 . . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))
4616, 22, 45cmpt 5137 . . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))
47 ctsu 22661 . . . . . . 7 class tsums
4833, 46, 47co 7145 . . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))
4932, 48cxp 5546 . . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5030, 5, 49ciun 4910 . . . 4 class 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5110, 11, 15, 29, 50cmpo 7147 . . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))))
522, 3, 6, 9, 51cmpo 7147 . 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
531, 52wceq 1528 1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
Colors of variables: wff setvar class
This definition is referenced by:  taylfval  24874
  Copyright terms: Public domain W3C validator