Theorem plyn0mulidp 26595

Description: Coefficients of a non-zero polynomial multiplied by the identity polynomial. (Contributed by Thierry Arnoux, 25-Sep-2018.)

Assertion

Ref	Expression
plyn0mulidp	⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹 ∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))

Distinct variable group:   𝑛,𝐹

Proof of Theorem plyn0mulidp

Dummy variables 𝑖 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 4078	. . . . 5 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → 𝐹 ∈ (Poly‘ℝ))
2		ax-resscn 11250	. . . . . . 7 ⊢ ℝ ⊆ ℂ
3		1re 11301	. . . . . . 7 ⊢ 1 ∈ ℝ
4		plyid 26520	. . . . . . 7 ⊢ ((ℝ ⊆ ℂ ∧ 1 ∈ ℝ) → Xp ∈ (Poly‘ℝ))
5	2, 3, 4	mp2an 705	. . . . . 6 ⊢ Xp ∈ (Poly‘ℝ)
6	5	a1i 11	. . . . 5 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → Xp ∈ (Poly‘ℝ))
7		simprl 783	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑥 ∈ ℝ)
8		simprr 785	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → 𝑦 ∈ ℝ)
9	7, 8	readdcld 11331	. . . . 5 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 + 𝑦) ∈ ℝ)
10	7, 8	remulcld 11332	. . . . 5 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
11	1, 6, 9, 10	plymul 26530	. . . 4 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (𝐹 ∘f · Xp) ∈ (Poly‘ℝ))
12		0re 11303	. . . 4 ⊢ 0 ∈ ℝ
13		eqid 2761	. . . . 5 ⊢ (coeff‘(𝐹 ∘f · Xp)) = (coeff‘(𝐹 ∘f · Xp))
14	13	coef2 26543	. . . 4 ⊢ (((𝐹 ∘f · Xp) ∈ (Poly‘ℝ) ∧ 0 ∈ ℝ) → (coeff‘(𝐹 ∘f · Xp)):ℕ0⟶ℝ)
15	11, 12, 14	sylancl 598	. . 3 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹 ∘f · Xp)):ℕ0⟶ℝ)
16	15	feqmptd 6951	. 2 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹 ∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ ((coeff‘(𝐹 ∘f · Xp))‘𝑛)))
17		cnex 11274	. . . . . . . . 9 ⊢ ℂ ∈ V
18	17	a1i 11	. . . . . . . 8 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → ℂ ∈ V)
19		plyf 26509	. . . . . . . . 9 ⊢ (𝐹 ∈ (Poly‘ℝ) → 𝐹:ℂ⟶ℂ)
20	1, 19	syl 18	. . . . . . . 8 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → 𝐹:ℂ⟶ℂ)
21		plyf 26509	. . . . . . . . . 10 ⊢ (Xp ∈ (Poly‘ℝ) → Xp:ℂ⟶ℂ)
22	5, 21	ax-mp 5	. . . . . . . . 9 ⊢ Xp:ℂ⟶ℂ
23	22	a1i 11	. . . . . . . 8 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → Xp:ℂ⟶ℂ)
24		simprl 783	. . . . . . . . 9 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑥 ∈ ℂ)
25		simprr 785	. . . . . . . . 9 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → 𝑦 ∈ ℂ)
26	24, 25	mulcomd 11323	. . . . . . . 8 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
27	18, 20, 23, 26	caofcom 7728	. . . . . . 7 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (𝐹 ∘f · Xp) = (Xp ∘f · 𝐹))
28	27	fveq2d 6887	. . . . . 6 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹 ∘f · Xp)) = (coeff‘(Xp ∘f · 𝐹)))
29	28	fveq1d 6885	. . . . 5 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → ((coeff‘(𝐹 ∘f · Xp))‘𝑛) = ((coeff‘(Xp ∘f · 𝐹))‘𝑛))
30	29	adantr 486	. . . 4 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → ((coeff‘(𝐹 ∘f · Xp))‘𝑛) = ((coeff‘(Xp ∘f · 𝐹))‘𝑛))
31	5	a1i 11	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → Xp ∈ (Poly‘ℝ))
32	1	adantr 486	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → 𝐹 ∈ (Poly‘ℝ))
33		simpr 490	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → 𝑛 ∈ ℕ0)
34		eqid 2761	. . . . . . 7 ⊢ (coeff‘Xp) = (coeff‘Xp)
35		eqid 2761	. . . . . . 7 ⊢ (coeff‘𝐹) = (coeff‘𝐹)
36	34, 35	coemul 26564	. . . . . 6 ⊢ ((Xp ∈ (Poly‘ℝ) ∧ 𝐹 ∈ (Poly‘ℝ) ∧ 𝑛 ∈ ℕ0) → ((coeff‘(Xp ∘f · 𝐹))‘𝑛) = Σ𝑖 ∈ (0...𝑛)(((coeff‘Xp)‘𝑖) · ((coeff‘𝐹)‘(𝑛 − 𝑖))))
37	31, 32, 33, 36	syl3anc 1398	. . . . 5 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → ((coeff‘(Xp ∘f · 𝐹))‘𝑛) = Σ𝑖 ∈ (0...𝑛)(((coeff‘Xp)‘𝑖) · ((coeff‘𝐹)‘(𝑛 − 𝑖))))
38		elfznn0 13747	. . . . . . . . . 10 ⊢ (𝑖 ∈ (0...𝑛) → 𝑖 ∈ ℕ0)
39		coeidp 26575	. . . . . . . . . 10 ⊢ (𝑖 ∈ ℕ0 → ((coeff‘Xp)‘𝑖) = if(𝑖 = 1, 1, 0))
40	38, 39	syl 18	. . . . . . . . 9 ⊢ (𝑖 ∈ (0...𝑛) → ((coeff‘Xp)‘𝑖) = if(𝑖 = 1, 1, 0))
41	40	oveq1d 7433	. . . . . . . 8 ⊢ (𝑖 ∈ (0...𝑛) → (((coeff‘Xp)‘𝑖) · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = (if(𝑖 = 1, 1, 0) · ((coeff‘𝐹)‘(𝑛 − 𝑖))))
42		ovif 7516	. . . . . . . 8 ⊢ (if(𝑖 = 1, 1, 0) · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖))))
43	41, 42	eqtrdi 2812	. . . . . . 7 ⊢ (𝑖 ∈ (0...𝑛) → (((coeff‘Xp)‘𝑖) · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖)))))
44	43	adantl 487	. . . . . 6 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → (((coeff‘Xp)‘𝑖) · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖)))))
45	44	sumeq2dv 15862	. . . . 5 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑛)(((coeff‘Xp)‘𝑖) · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = Σ𝑖 ∈ (0...𝑛)if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖)))))
46		velsn 4600	. . . . . . . . . 10 ⊢ (𝑖 ∈ {1} ↔ 𝑖 = 1)
47	46	bicomi 227	. . . . . . . . 9 ⊢ (𝑖 = 1 ↔ 𝑖 ∈ {1})
48	47	a1i 11	. . . . . . . 8 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → (𝑖 = 1 ↔ 𝑖 ∈ {1}))
49	35	coef2 26543	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (Poly‘ℝ) ∧ 0 ∈ ℝ) → (coeff‘𝐹):ℕ0⟶ℝ)
50	1, 12, 49	sylancl 598	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘𝐹):ℕ0⟶ℝ)
51	50	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → (coeff‘𝐹):ℕ0⟶ℝ)
52		fznn0sub 13683	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑛) → (𝑛 − 𝑖) ∈ ℕ0)
53	52	adantl 487	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → (𝑛 − 𝑖) ∈ ℕ0)
54	51, 53	ffvelcdmd 7083	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → ((coeff‘𝐹)‘(𝑛 − 𝑖)) ∈ ℝ)
55	54	recnd 11330	. . . . . . . . 9 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → ((coeff‘𝐹)‘(𝑛 − 𝑖)) ∈ ℂ)
56	55	mullidd 11320	. . . . . . . 8 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = ((coeff‘𝐹)‘(𝑛 − 𝑖)))
57	55	mul02d 11501	. . . . . . . 8 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖))) = 0)
58	48, 56, 57	ifbieq12d 4511	. . . . . . 7 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑖 ∈ (0...𝑛)) → if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖)))) = if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0))
59	58	sumeq2dv 15862	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑛)if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖)))) = Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0))
60		eqeq2 2773	. . . . . . 7 ⊢ (0 = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))) → (Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = 0 ↔ Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
61		eqeq2 2773	. . . . . . 7 ⊢ (((coeff‘𝐹)‘(𝑛 − 1)) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))) → (Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = ((coeff‘𝐹)‘(𝑛 − 1)) ↔ Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
62		oveq2 7426	. . . . . . . . . . 11 ⊢ (𝑛 = 0 → (0...𝑛) = (0...0))
63		0z 12697	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
64		fzsn 13693	. . . . . . . . . . . 12 ⊢ (0 ∈ ℤ → (0...0) = {0})
65	63, 64	ax-mp 5	. . . . . . . . . . 11 ⊢ (0...0) = {0}
66	62, 65	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑛 = 0 → (0...𝑛) = {0})
67		elsni 4601	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ {0} → 𝑖 = 0)
68	67	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑛 = 0 ∧ 𝑖 ∈ {0}) → 𝑖 = 0)
69		ax-1ne0 11262	. . . . . . . . . . . . 13 ⊢ 1 ≠ 0
70	69	nesymi 3013	. . . . . . . . . . . 12 ⊢ ¬ 0 = 1
71		eqeq1 2765	. . . . . . . . . . . 12 ⊢ (𝑖 = 0 → (𝑖 = 1 ↔ 0 = 1))
72	70, 71	mtbiri 330	. . . . . . . . . . 11 ⊢ (𝑖 = 0 → ¬ 𝑖 = 1)
73	47	notbii 323	. . . . . . . . . . . 12 ⊢ (¬ 𝑖 = 1 ↔ ¬ 𝑖 ∈ {1})
74	73	biimpi 219	. . . . . . . . . . 11 ⊢ (¬ 𝑖 = 1 → ¬ 𝑖 ∈ {1})
75		iffalse 4491	. . . . . . . . . . 11 ⊢ (¬ 𝑖 ∈ {1} → if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = 0)
76	68, 72, 74, 75	4syl 20	. . . . . . . . . 10 ⊢ ((𝑛 = 0 ∧ 𝑖 ∈ {0}) → if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = 0)
77	66, 76	sumeq12rdv 15866	. . . . . . . . 9 ⊢ (𝑛 = 0 → Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = Σ𝑖 ∈ {0}0)
78		snfi 9064	. . . . . . . . . . 11 ⊢ {0} ∈ Fin
79	78	olci 880	. . . . . . . . . 10 ⊢ ({0} ⊆ (ℤ≥‘0) ∨ {0} ∈ Fin)
80		sumz 15881	. . . . . . . . . 10 ⊢ (({0} ⊆ (ℤ≥‘0) ∨ {0} ∈ Fin) → Σ𝑖 ∈ {0}0 = 0)
81	79, 80	ax-mp 5	. . . . . . . . 9 ⊢ Σ𝑖 ∈ {0}0 = 0
82	77, 81	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑛 = 0 → Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = 0)
83	82	adantl 487	. . . . . . 7 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ 𝑛 = 0) → Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = 0)
84		simpll 779	. . . . . . . 8 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}))
85	33	adantr 486	. . . . . . . . 9 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ0)
86		simpr 490	. . . . . . . . . 10 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → ¬ 𝑛 = 0)
87	86	neqned 2963	. . . . . . . . 9 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ≠ 0)
88		elnnne0 12613	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0))
89	85, 87, 88	sylanbrc 595	. . . . . . . 8 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → 𝑛 ∈ ℕ)
90		1nn0 12615	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℕ0
91	90	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → 1 ∈ ℕ0)
92		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ)
93	92	nnnn0d 12660	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → 𝑛 ∈ ℕ0)
94	92	nnge1d 12379	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → 1 ≤ 𝑛)
95		elfz2nn0 13745	. . . . . . . . . . . 12 ⊢ (1 ∈ (0...𝑛) ↔ (1 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 1 ≤ 𝑛))
96	91, 93, 94, 95	syl3anbrc 1362	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → 1 ∈ (0...𝑛))
97	96	snssd 4747	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → {1} ⊆ (0...𝑛))
98	50	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ {1}) → (coeff‘𝐹):ℕ0⟶ℝ)
99		oveq2 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 1 → (𝑛 − 𝑖) = (𝑛 − 1))
100	46, 99	sylbi 220	. . . . . . . . . . . . . . 15 ⊢ (𝑖 ∈ {1} → (𝑛 − 𝑖) = (𝑛 − 1))
101	100	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ {1}) → (𝑛 − 𝑖) = (𝑛 − 1))
102		nnm1nn0 12640	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ0)
103	102	ad2antlr 740	. . . . . . . . . . . . . 14 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ {1}) → (𝑛 − 1) ∈ ℕ0)
104	101, 103	eqeltrd 2861	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ {1}) → (𝑛 − 𝑖) ∈ ℕ0)
105	98, 104	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ {1}) → ((coeff‘𝐹)‘(𝑛 − 𝑖)) ∈ ℝ)
106	105	recnd 11330	. . . . . . . . . . 11 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) ∧ 𝑖 ∈ {1}) → ((coeff‘𝐹)‘(𝑛 − 𝑖)) ∈ ℂ)
107	106	ralrimiva 3155	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → ∀𝑖 ∈ {1} ((coeff‘𝐹)‘(𝑛 − 𝑖)) ∈ ℂ)
108		fzfi 14108	. . . . . . . . . . . 12 ⊢ (0...𝑛) ∈ Fin
109	108	olci 880	. . . . . . . . . . 11 ⊢ ((0...𝑛) ⊆ (ℤ≥‘0) ∨ (0...𝑛) ∈ Fin)
110	109	a1i 11	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → ((0...𝑛) ⊆ (ℤ≥‘0) ∨ (0...𝑛) ∈ Fin))
111		sumss2 15885	. . . . . . . . . 10 ⊢ ((({1} ⊆ (0...𝑛) ∧ ∀𝑖 ∈ {1} ((coeff‘𝐹)‘(𝑛 − 𝑖)) ∈ ℂ) ∧ ((0...𝑛) ⊆ (ℤ≥‘0) ∨ (0...𝑛) ∈ Fin)) → Σ𝑖 ∈ {1} ((coeff‘𝐹)‘(𝑛 − 𝑖)) = Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0))
112	97, 107, 110, 111	syl21anc 851	. . . . . . . . 9 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → Σ𝑖 ∈ {1} ((coeff‘𝐹)‘(𝑛 − 𝑖)) = Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0))
113	50	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → (coeff‘𝐹):ℕ0⟶ℝ)
114	102	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → (𝑛 − 1) ∈ ℕ0)
115	113, 114	ffvelcdmd 7083	. . . . . . . . . . 11 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → ((coeff‘𝐹)‘(𝑛 − 1)) ∈ ℝ)
116	115	recnd 11330	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → ((coeff‘𝐹)‘(𝑛 − 1)) ∈ ℂ)
117	99	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝑖 = 1 → ((coeff‘𝐹)‘(𝑛 − 𝑖)) = ((coeff‘𝐹)‘(𝑛 − 1)))
118	117	sumsn 15905	. . . . . . . . . 10 ⊢ ((1 ∈ ℝ ∧ ((coeff‘𝐹)‘(𝑛 − 1)) ∈ ℂ) → Σ𝑖 ∈ {1} ((coeff‘𝐹)‘(𝑛 − 𝑖)) = ((coeff‘𝐹)‘(𝑛 − 1)))
119	3, 116, 118	sylancr 599	. . . . . . . . 9 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → Σ𝑖 ∈ {1} ((coeff‘𝐹)‘(𝑛 − 𝑖)) = ((coeff‘𝐹)‘(𝑛 − 1)))
120	112, 119	eqtr3d 2798	. . . . . . . 8 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ) → Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = ((coeff‘𝐹)‘(𝑛 − 1)))
121	84, 89, 120	syl2anc 596	. . . . . . 7 ⊢ (((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) ∧ ¬ 𝑛 = 0) → Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = ((coeff‘𝐹)‘(𝑛 − 1)))
122	60, 61, 83, 121	ifbothda 4521	. . . . . 6 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑛)if(𝑖 ∈ {1}, ((coeff‘𝐹)‘(𝑛 − 𝑖)), 0) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))
123	59, 122	eqtrd 2796	. . . . 5 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → Σ𝑖 ∈ (0...𝑛)if(𝑖 = 1, (1 · ((coeff‘𝐹)‘(𝑛 − 𝑖))), (0 · ((coeff‘𝐹)‘(𝑛 − 𝑖)))) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))
124	37, 45, 123	3eqtrd 2800	. . . 4 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → ((coeff‘(Xp ∘f · 𝐹))‘𝑛) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))
125	30, 124	eqtrd 2796	. . 3 ⊢ ((𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) ∧ 𝑛 ∈ ℕ0) → ((coeff‘(𝐹 ∘f · Xp))‘𝑛) = if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))
126	125	mpteq2dva 5198	. 2 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (𝑛 ∈ ℕ0 ↦ ((coeff‘(𝐹 ∘f · Xp))‘𝑛)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))
127	16, 126	eqtrd 2796	1 ⊢ (𝐹 ∈ ((Poly‘ℝ) ∖ {0𝑝}) → (coeff‘(𝐹 ∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  Vcvv 3451   ∖ cdif 3896   ⊆ wss 3899  ifcif 4482  {csn 4584   class class class wbr 5103   ↦ cmpt 5186  ⟶wf 6533  ‘cfv 6537  (class class class)co 7418   ∘_f cof 7689  Fincfn 8966  ℂcc 11191  ℝcr 11192  0cc0 11193  1c1 11194   · cmul 11198   ≤ cle 11337   − cmin 11534  ℕcn 12328  ℕ₀cn0 12599  ℤcz 12686  ℤ_≥cuz 12958  ...cfz 13632  Σcsu 15846  0_𝑝c0p 25983  Polycply 26495  X_pcidp 26496  coeffccoe 26497

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-rep 5232  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-inf2 9635  ax-cnex 11249  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270  ax-pre-sup 11271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rmo 3366  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-se 5605  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-of 7691  df-om 7876  df-1st 7999  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-1o 8469  df-er 8710  df-map 8842  df-pm 8843  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-sup 9427  df-inf 9428  df-oi 9497  df-card 10013  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-div 11967  df-nn 12329  df-2 12398  df-3 12399  df-n0 12600  df-z 12687  df-uz 12959  df-rp 13114  df-fz 13633  df-fzo 13782  df-fl 13925  df-seq 14138  df-exp 14198  df-hash 14468  df-cj 15259  df-re 15260  df-im 15261  df-sqrt 15395  df-abs 15396  df-clim 15648  df-rlim 15649  df-sum 15847  df-0p 25984  df-ply 26499  df-idp 26500  df-coe 26501  df-dgr 26502

This theorem is used by:  plymulidp  26596