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 23830
Description: Define the Taylor polynomial or Taylor series of a function. (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 23828 . 2 class Tayl
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cr 9791 . . . 4 class
5 cc 9790 . . . 4 class
64, 5cpr 4126 . . 3 class {ℝ, ℂ}
72cv 1473 . . . 4 class 𝑠
8 cpm 7722 . . . 4 class pm
95, 7, 8co 6527 . . 3 class (ℂ ↑pm 𝑠)
10 vn . . . 4 setvar 𝑛
11 va . . . 4 setvar 𝑎
12 cn0 11139 . . . . 5 class 0
13 cpnf 9927 . . . . . 6 class +∞
1413csn 4124 . . . . 5 class {+∞}
1512, 14cun 3537 . . . 4 class (ℕ0 ∪ {+∞})
16 vk . . . . 5 setvar 𝑘
17 cc0 9792 . . . . . . 7 class 0
1810cv 1473 . . . . . . 7 class 𝑛
19 cicc 12005 . . . . . . 7 class [,]
2017, 18, 19co 6527 . . . . . 6 class (0[,]𝑛)
21 cz 11210 . . . . . 6 class
2220, 21cin 3538 . . . . 5 class ((0[,]𝑛) ∩ ℤ)
2316cv 1473 . . . . . . 7 class 𝑘
243cv 1473 . . . . . . . 8 class 𝑓
25 cdvn 23351 . . . . . . . 8 class D𝑛
267, 24, 25co 6527 . . . . . . 7 class (𝑠 D𝑛 𝑓)
2723, 26cfv 5790 . . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
2827cdm 5028 . . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
2916, 22, 28ciin 4450 . . . 4 class 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30 vx . . . . 5 setvar 𝑥
3130cv 1473 . . . . . . 7 class 𝑥
3231csn 4124 . . . . . 6 class {𝑥}
33 ccnfld 19513 . . . . . . 7 class fld
3411cv 1473 . . . . . . . . . . 11 class 𝑎
3534, 27cfv 5790 . . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36 cfa 12877 . . . . . . . . . . 11 class !
3723, 36cfv 5790 . . . . . . . . . 10 class (!‘𝑘)
38 cdiv 10533 . . . . . . . . . 10 class /
3935, 37, 38co 6527 . . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40 cmin 10117 . . . . . . . . . . 11 class
4131, 34, 40co 6527 . . . . . . . . . 10 class (𝑥𝑎)
42 cexp 12677 . . . . . . . . . 10 class
4341, 23, 42co 6527 . . . . . . . . 9 class ((𝑥𝑎)↑𝑘)
44 cmul 9797 . . . . . . . . 9 class ·
4539, 43, 44co 6527 . . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))
4616, 22, 45cmpt 4637 . . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))
47 ctsu 21681 . . . . . . 7 class tsums
4833, 46, 47co 6527 . . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))
4932, 48cxp 5026 . . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5030, 5, 49ciun 4449 . . . 4 class 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5110, 11, 15, 29, 50cmpt2 6529 . . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))))
522, 3, 6, 9, 51cmpt2 6529 . 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
531, 52wceq 1474 1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
Colors of variables: wff setvar class
This definition is referenced by:  taylfval  23834
  Copyright terms: Public domain W3C validator