Definition df-coe

Description: Define the coefficient function for a polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Assertion	df-coe	$$⊢\mathrm{coeff}=\left(f\in \mathrm{Poly}\left(ℂ\right)⟼\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccoe	$$class\mathrm{coeff}$$
1		vf	$$setvarf$$
2		cply	$$class\mathrm{Poly}$$
3		cc	$$classℂ$$
4	3 2	cfv	$$class\mathrm{Poly}\left(ℂ\right)$$
5		va	$$setvara$$
6		cmap	$$class{\uparrow }_{𝑚}$$
7		cn0	$$class{\mathbb{N}}_0$$
8	3 7 6	co	$$class\left({ℂ}^{{\mathbb{N}}_0}\right)$$
9		vn	$$setvarn$$
10	5	cv	$$setvara$$
11		cuz	$$class{\mathbb{Z}}_{\ge }$$
12	9	cv	$$setvarn$$
13		caddc	$$class+$$
14		c1	$$class1$$
15	12 14 13	co	$$class\left(n+1\right)$$
16	15 11	cfv	$$class{\mathbb{Z}}_{\ge \left(n+1\right)}$$
17	10 16	cima	$$classa\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]$$
18		cc0	$$class0$$
19	18	csn	$$class\left\{0\right\}$$
20	17 19	wceq	$$wffa\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}$$
21	1	cv	$$setvarf$$
22		vz	$$setvarz$$
23		vk	$$setvark$$
24		cfz	$$class\dots$$
25	18 12 24	co	$$class\left(0\dots n\right)$$
26	23	cv	$$setvark$$
27	26 10	cfv	$$classa\left(k\right)$$
28		cmul	$$class\times$$
29	22	cv	$$setvarz$$
30		cexp	$$class^$$
31	29 26 30	co	$$class{z}^k$$
32	27 31 28	co	$$classa\left(k\right)z^k$$
33	25 32 23	csu	$$class\sum _{k=0}^{n}a\left(k\right)z^k$$
34	22 3 33	cmpt	$$class\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
35	21 34	wceq	$$wfff=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
36	20 35	wa	$$wff\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
37	36 9 7	wrex	$$wff\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
38	37 5 8	crio	$$class\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)$$
39	1 4 38	cmpt	$$class\left(f\in \mathrm{Poly}\left(ℂ\right)⟼\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)\right)$$
40	0 39	wceq	$$wff\mathrm{coeff}=\left(f\in \mathrm{Poly}\left(ℂ\right)⟼\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)\right)$$