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

Definition df-tayl 24960
 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 24958 . 2 class Tayl
2 vs . . 3 setvar 𝑠
3 vf . . 3 setvar 𝑓
4 cr 10528 . . . 4 class
5 cc 10527 . . . 4 class
64, 5cpr 4527 . . 3 class {ℝ, ℂ}
72cv 1537 . . . 4 class 𝑠
8 cpm 8393 . . . 4 class pm
95, 7, 8co 7136 . . 3 class (ℂ ↑pm 𝑠)
10 vn . . . 4 setvar 𝑛
11 va . . . 4 setvar 𝑎
12 cn0 11888 . . . . 5 class 0
13 cpnf 10664 . . . . . 6 class +∞
1413csn 4525 . . . . 5 class {+∞}
1512, 14cun 3879 . . . 4 class (ℕ0 ∪ {+∞})
16 vk . . . . 5 setvar 𝑘
17 cc0 10529 . . . . . . 7 class 0
1810cv 1537 . . . . . . 7 class 𝑛
19 cicc 12732 . . . . . . 7 class [,]
2017, 18, 19co 7136 . . . . . 6 class (0[,]𝑛)
21 cz 11972 . . . . . 6 class
2220, 21cin 3880 . . . . 5 class ((0[,]𝑛) ∩ ℤ)
2316cv 1537 . . . . . . 7 class 𝑘
243cv 1537 . . . . . . . 8 class 𝑓
25 cdvn 24477 . . . . . . . 8 class D𝑛
267, 24, 25co 7136 . . . . . . 7 class (𝑠 D𝑛 𝑓)
2723, 26cfv 6325 . . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
2827cdm 5520 . . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
2916, 22, 28ciin 4883 . . . 4 class 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30 vx . . . . 5 setvar 𝑥
3130cv 1537 . . . . . . 7 class 𝑥
3231csn 4525 . . . . . 6 class {𝑥}
33 ccnfld 20095 . . . . . . 7 class fld
3411cv 1537 . . . . . . . . . . 11 class 𝑎
3534, 27cfv 6325 . . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36 cfa 13632 . . . . . . . . . . 11 class !
3723, 36cfv 6325 . . . . . . . . . 10 class (!‘𝑘)
38 cdiv 11289 . . . . . . . . . 10 class /
3935, 37, 38co 7136 . . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40 cmin 10862 . . . . . . . . . . 11 class
4131, 34, 40co 7136 . . . . . . . . . 10 class (𝑥𝑎)
42 cexp 13428 . . . . . . . . . 10 class
4341, 23, 42co 7136 . . . . . . . . 9 class ((𝑥𝑎)↑𝑘)
44 cmul 10534 . . . . . . . . 9 class ·
4539, 43, 44co 7136 . . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))
4616, 22, 45cmpt 5111 . . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))
47 ctsu 22741 . . . . . . 7 class tsums
4833, 46, 47co 7136 . . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))
4932, 48cxp 5518 . . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5030, 5, 49ciun 4882 . . . 4 class 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))
5110, 11, 15, 29, 50cmpo 7138 . . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘))))))
522, 3, 6, 9, 51cmpo 7138 . 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
531, 52wceq 1538 1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥𝑎)↑𝑘)))))))
 Colors of variables: wff setvar class This definition is referenced by:  taylfval  24964
 Copyright terms: Public domain W3C validator