Definition df-tayl

Description: Define the Taylor polynomial or Taylor series of a function. TODO-AV: n e. ( NN0 u. { +oo } ) should be replaced by n e. NN0* . (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Assertion	df-tayl	$$⊢\mathrm{Tayl}=\left(s\in \left\{ℝ,ℂ\right\},f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼\left(n\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right),a\in \bigcap _{k\in \left[0,n\right]\cap \mathbb{Z}}\mathrm{dom}\left(s{D}^{n}f\right)\left(k\right)⟼\bigcup _{x\in ℂ}\left(\left\{x\right\}\times \left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctayl	$$class\mathrm{Tayl}$$
1		vs	$$setvars$$
2		cr	$$classℝ$$
3		cc	$$classℂ$$
4	2 3	cpr	$$class\left\{ℝ,ℂ\right\}$$
5		vf	$$setvarf$$
6		cpm	$$class{\uparrow }_{𝑝𝑚}$$
7	1	cv	$$setvars$$
8	3 7 6	co	$$class\left(ℂ{\uparrow }_{𝑝𝑚}s\right)$$
9		vn	$$setvarn$$
10		cn0	$$class{\mathbb{N}}_0$$
11		cpnf	$$class\mathrm{+\infty }$$
12	11	csn	$$class\left\{\mathrm{+\infty }\right\}$$
13	10 12	cun	$$class\left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right)$$
14		va	$$setvara$$
15		vk	$$setvark$$
16		cc0	$$class0$$
17		cicc	$$class\left[.\right]$$
18	9	cv	$$setvarn$$
19	16 18 17	co	$$class\left[0,n\right]$$
20		cz	$$class\mathbb{Z}$$
21	19 20	cin	$$class\left(\left[0,n\right]\cap \mathbb{Z}\right)$$
22		cdvn	$$class{D}^n$$
23	5	cv	$$setvarf$$
24	7 23 22	co	$$class\left(s{D}^{n}f\right)$$
25	15	cv	$$setvark$$
26	25 24	cfv	$$class\left(s{D}^{n}f\right)\left(k\right)$$
27	26	cdm	$$class\mathrm{dom}\left(s{D}^{n}f\right)\left(k\right)$$
28	15 21 27	ciin	$$class\bigcap _{k\in \left[0,n\right]\cap \mathbb{Z}}\mathrm{dom}\left(s{D}^{n}f\right)\left(k\right)$$
29		vx	$$setvarx$$
30	29	cv	$$setvarx$$
31	30	csn	$$class\left\{x\right\}$$
32		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
33		ctsu	$$class\mathrm{tsums}$$
34	14	cv	$$setvara$$
35	34 26	cfv	$$class\left(s{D}^{n}f\right)\left(k\right)\left(a\right)$$
36		cdiv	$$class÷$$
37		cfa	$$class!$$
38	25 37	cfv	$$classk!$$
39	35 38 36	co	$$class\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right)$$
40		cmul	$$class\times$$
41		cmin	$$class-$$
42	30 34 41	co	$$class\left(x-a\right)$$
43		cexp	$$class^$$
44	42 25 43	co	$$class{\left(x-a\right)}^k$$
45	39 44 40	co	$$class\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k$$
46	15 21 45	cmpt	$$class\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)$$
47	32 46 33	co	$$class\left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)$$
48	31 47	cxp	$$class\left(\left\{x\right\}\times \left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)\right)$$
49	29 3 48	ciun	$$class\bigcup _{x\in ℂ}\left(\left\{x\right\}\times \left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)\right)$$
50	9 14 13 28 49	cmpo	$$class\left(n\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right),a\in \bigcap _{k\in \left[0,n\right]\cap \mathbb{Z}}\mathrm{dom}\left(s{D}^{n}f\right)\left(k\right)⟼\bigcup _{x\in ℂ}\left(\left\{x\right\}\times \left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)\right)\right)$$
51	1 5 4 8 50	cmpo	$$class\left(s\in \left\{ℝ,ℂ\right\},f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼\left(n\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right),a\in \bigcap _{k\in \left[0,n\right]\cap \mathbb{Z}}\mathrm{dom}\left(s{D}^{n}f\right)\left(k\right)⟼\bigcup _{x\in ℂ}\left(\left\{x\right\}\times \left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)\right)\right)\right)$$
52	0 51	wceq	$$wff\mathrm{Tayl}=\left(s\in \left\{ℝ,ℂ\right\},f\in \left(ℂ{\uparrow }_{𝑝𝑚}s\right)⟼\left(n\in \left({\mathbb{N}}_0\cup \left\{\mathrm{+\infty }\right\}\right),a\in \bigcap _{k\in \left[0,n\right]\cap \mathbb{Z}}\mathrm{dom}\left(s{D}^{n}f\right)\left(k\right)⟼\bigcup _{x\in ℂ}\left(\left\{x\right\}\times \left({ℂ}_{\mathrm{fld}}\mathrm{tsums}\left(k\in \left(\left[0,n\right]\cap \mathbb{Z}\right)⟼\left(\frac{\left(s{D}^{n}f\right)\left(k\right)\left(a\right)}{k!}\right){\left(x-a\right)}^k\right)\right)\right)\right)\right)$$