Definition df-coe 26470

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

Assertion

Ref	Expression
df-coe	⊢ coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))

Distinct variable group:   𝑓,𝑎,𝑘,𝑛,𝑧

Detailed syntax breakdown of Definition df-coe

Step	Hyp	Ref	Expression
1		ccoe 26466	. 2 class coeff
2		vf	. . 3 setvar 𝑓
3		cc 11170	. . . 4 class ℂ
4		cply 26464	. . . 4 class Poly
5	3, 4	cfv 6527	. . 3 class (Poly‘ℂ)
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1569	. . . . . . . 8 class 𝑎
8		vn	. . . . . . . . . . 11 setvar 𝑛
9	8	cv 1569	. . . . . . . . . 10 class 𝑛
10		c1 11173	. . . . . . . . . 10 class 1
11		caddc 11175	. . . . . . . . . 10 class +
12	9, 10, 11	co 7408	. . . . . . . . 9 class (𝑛 + 1)
13		cuz 12935	. . . . . . . . 9 class ℤ≥
14	12, 13	cfv 6527	. . . . . . . 8 class (ℤ≥‘(𝑛 + 1))
15	7, 14	cima 5650	. . . . . . 7 class (𝑎 “ (ℤ≥‘(𝑛 + 1)))
16		cc0 11172	. . . . . . . 8 class 0
17	16	csn 4583	. . . . . . 7 class {0}
18	15, 17	wceq 1570	. . . . . 6 wff (𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0}
19	2	cv 1569	. . . . . . 7 class 𝑓
20		vz	. . . . . . . 8 setvar 𝑧
21		cfz 13609	. . . . . . . . . 10 class ...
22	16, 9, 21	co 7408	. . . . . . . . 9 class (0...𝑛)
23		vk	. . . . . . . . . . . 12 setvar 𝑘
24	23	cv 1569	. . . . . . . . . . 11 class 𝑘
25	24, 7	cfv 6527	. . . . . . . . . 10 class (𝑎‘𝑘)
26	20	cv 1569	. . . . . . . . . . 11 class 𝑧
27		cexp 14173	. . . . . . . . . . 11 class ↑
28	26, 24, 27	co 7408	. . . . . . . . . 10 class (𝑧↑𝑘)
29		cmul 11177	. . . . . . . . . 10 class ·
30	25, 28, 29	co 7408	. . . . . . . . 9 class ((𝑎‘𝑘) · (𝑧↑𝑘))
31	22, 30, 23	csu 15821	. . . . . . . 8 class Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))
32	20, 3, 31	cmpt 5185	. . . . . . 7 class (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
33	19, 32	wceq 1570	. . . . . 6 wff 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))
34	18, 33	wa 401	. . . . 5 wff ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
35		cn0 12576	. . . . 5 class ℕ0
36	34, 8, 35	wrex 3086	. . . 4 wff ∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))
37		cmap 8825	. . . . 5 class ↑m
38	3, 35, 37	co 7408	. . . 4 class (ℂ ↑m ℕ0)
39	36, 6, 38	crio 7364	. . 3 class (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
40	2, 5, 39	cmpt 5185	. 2 class (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))
41	1, 40	wceq 1570	1 wff coeff = (𝑓 ∈ (Poly‘ℂ) ↦ (℩𝑎 ∈ (ℂ ↑m ℕ0)∃𝑛 ∈ ℕ0 ((𝑎 “ (ℤ≥‘(𝑛 + 1))) = {0} ∧ 𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))))))

This definition is used by:  coeval  26504