Definition df-tayl 26396

Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: 𝑛 ∈ (ℕ₀ ∪ {+∞}) should be replaced by 𝑛 ∈ ℕ₀^*. (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

Step	Hyp	Ref	Expression
1		ctayl 26394	. 2 class Tayl
2		vs	. . 3 setvar 𝑠
3		vf	. . 3 setvar 𝑓
4		cr 11154	. . . 4 class ℝ
5		cc 11153	. . . 4 class ℂ
6	4, 5	cpr 4628	. . 3 class {ℝ, ℂ}
7	2	cv 1539	. . . 4 class 𝑠
8		cpm 8867	. . . 4 class ↑pm
9	5, 7, 8	co 7431	. . 3 class (ℂ ↑pm 𝑠)
10		vn	. . . 4 setvar 𝑛
11		va	. . . 4 setvar 𝑎
12		cn0 12526	. . . . 5 class ℕ0
13		cpnf 11292	. . . . . 6 class +∞
14	13	csn 4626	. . . . 5 class {+∞}
15	12, 14	cun 3949	. . . 4 class (ℕ0 ∪ {+∞})
16		vk	. . . . 5 setvar 𝑘
17		cc0 11155	. . . . . . 7 class 0
18	10	cv 1539	. . . . . . 7 class 𝑛
19		cicc 13390	. . . . . . 7 class [,]
20	17, 18, 19	co 7431	. . . . . 6 class (0[,]𝑛)
21		cz 12613	. . . . . 6 class ℤ
22	20, 21	cin 3950	. . . . 5 class ((0[,]𝑛) ∩ ℤ)
23	16	cv 1539	. . . . . . 7 class 𝑘
24	3	cv 1539	. . . . . . . 8 class 𝑓
25		cdvn 25899	. . . . . . . 8 class D𝑛
26	7, 24, 25	co 7431	. . . . . . 7 class (𝑠 D𝑛 𝑓)
27	23, 26	cfv 6561	. . . . . 6 class ((𝑠 D𝑛 𝑓)‘𝑘)
28	27	cdm 5685	. . . . 5 class dom ((𝑠 D𝑛 𝑓)‘𝑘)
29	16, 22, 28	ciin 4992	. . . 4 class ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘)
30		vx	. . . . 5 setvar 𝑥
31	30	cv 1539	. . . . . . 7 class 𝑥
32	31	csn 4626	. . . . . 6 class {𝑥}
33		ccnfld 21364	. . . . . . 7 class ℂfld
34	11	cv 1539	. . . . . . . . . . 11 class 𝑎
35	34, 27	cfv 6561	. . . . . . . . . 10 class (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎)
36		cfa 14312	. . . . . . . . . . 11 class !
37	23, 36	cfv 6561	. . . . . . . . . 10 class (!‘𝑘)
38		cdiv 11920	. . . . . . . . . 10 class /
39	35, 37, 38	co 7431	. . . . . . . . 9 class ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘))
40		cmin 11492	. . . . . . . . . . 11 class −
41	31, 34, 40	co 7431	. . . . . . . . . 10 class (𝑥 − 𝑎)
42		cexp 14102	. . . . . . . . . 10 class ↑
43	41, 23, 42	co 7431	. . . . . . . . 9 class ((𝑥 − 𝑎)↑𝑘)
44		cmul 11160	. . . . . . . . 9 class ·
45	39, 43, 44	co 7431	. . . . . . . 8 class (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))
46	16, 22, 45	cmpt 5225	. . . . . . 7 class (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))
47		ctsu 24134	. . . . . . 7 class tsums
48	33, 46, 47	co 7431	. . . . . 6 class (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))
49	32, 48	cxp 5683	. . . . 5 class ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))
50	30, 5, 49	ciun 4991	. . . 4 class ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))
51	10, 11, 15, 29, 50	cmpo 7433	. . 3 class (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))
52	2, 3, 6, 9, 51	cmpo 7433	. 2 class (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))
53	1, 52	wceq 1540	1 wff Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ ↑pm 𝑠) ↦ (𝑛 ∈ (ℕ0 ∪ {+∞}), 𝑎 ∈ ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))

This definition is referenced by:  taylfval  26400