Metamath Proof Explorer

Theorem plymulx0

Description: Coefficients of a polynomial multiplied by Xp . (Contributed by Thierry Arnoux, 25-Sep-2018)

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

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → 𝐹 ∈ ( Poly ‘ ℝ ) )
2 ax-resscn ⊢ ℝ ⊆ ℂ
3 1re ⊢ 1 ∈ ℝ
4 plyid ⊢ ( ( ℝ ⊆ ℂ ∧ 1 ∈ ℝ ) → Xp ∈ ( Poly ‘ ℝ ) )
5 2 3 4 mp2an ⊢ Xp ∈ ( Poly ‘ ℝ )
6 5 a1i ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → Xp ∈ ( Poly ‘ ℝ ) )
7 simprl ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝑥 ∈ ℝ )
8 simprr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
9 7 8 readdcld ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 + 𝑦 ) ∈ ℝ )
10 7 8 remulcld ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
11 1 6 9 10 plymul ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( 𝐹 ∘f · Xp ) ∈ ( Poly ‘ ℝ ) )
12 0re ⊢ 0 ∈ ℝ
13 eqid ⊢ ( coeff ‘ ( 𝐹 ∘f · Xp ) ) = ( coeff ‘ ( 𝐹 ∘f · Xp ) )
14 13 coef2 ⊢ ( ( ( 𝐹 ∘f · Xp ) ∈ ( Poly ‘ ℝ ) ∧ 0 ∈ ℝ ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) : ℕ0 ⟶ ℝ )
15 11 12 14 sylancl ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) : ℕ0 ⟶ ℝ )
16 15 feqmptd ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) = ( 𝑛 ∈ ℕ0 ↦ ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) ) )
17 cnex ⊢ ℂ ∈ V
18 17 a1i ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ℂ ∈ V )
19 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → 𝐹 : ℂ ⟶ ℂ )
20 1 19 syl ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → 𝐹 : ℂ ⟶ ℂ )
21 plyf ⊢ ( Xp ∈ ( Poly ‘ ℝ ) → Xp : ℂ ⟶ ℂ )
22 5 21 ax-mp ⊢ Xp : ℂ ⟶ ℂ
23 22 a1i ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → Xp : ℂ ⟶ ℂ )
24 simprl ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑥 ∈ ℂ )
25 simprr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → 𝑦 ∈ ℂ )
26 24 25 mulcomd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
27 18 20 23 26 caofcom ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( 𝐹 ∘f · Xp ) = ( Xp ∘f · 𝐹 ) )
28 27 fveq2d ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) = ( coeff ‘ ( Xp ∘f · 𝐹 ) ) )
29 28 fveq1d ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) = ( ( coeff ‘ ( Xp ∘f · 𝐹 ) ) ‘ 𝑛 ) )
30 29 adantr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) = ( ( coeff ‘ ( Xp ∘f · 𝐹 ) ) ‘ 𝑛 ) )
31 5 a1i ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Xp ∈ ( Poly ‘ ℝ ) )
32 1 adantr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → 𝐹 ∈ ( Poly ‘ ℝ ) )
33 simpr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ℕ0 )
34 eqid ⊢ ( coeff ‘ Xp ) = ( coeff ‘ Xp )
35 eqid ⊢ ( coeff ‘ 𝐹 ) = ( coeff ‘ 𝐹 )
36 34 35 coemul ⊢ ( ( Xp ∈ ( Poly ‘ ℝ ) ∧ 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( Xp ∘f · 𝐹 ) ) ‘ 𝑛 ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ Xp ) ‘ 𝑖 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
37 31 32 33 36 syl3anc ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( Xp ∘f · 𝐹 ) ) ‘ 𝑛 ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ Xp ) ‘ 𝑖 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
38 elfznn0 ⊢ ( 𝑖 ∈ ( 0 ... 𝑛 ) → 𝑖 ∈ ℕ0 )
39 coeidp ⊢ ( 𝑖 ∈ ℕ0 → ( ( coeff ‘ Xp ) ‘ 𝑖 ) = if ( 𝑖 = 1 , 1 , 0 ) )
40 38 39 syl ⊢ ( 𝑖 ∈ ( 0 ... 𝑛 ) → ( ( coeff ‘ Xp ) ‘ 𝑖 ) = if ( 𝑖 = 1 , 1 , 0 ) )
41 40 oveq1d ⊢ ( 𝑖 ∈ ( 0 ... 𝑛 ) → ( ( ( coeff ‘ Xp ) ‘ 𝑖 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = ( if ( 𝑖 = 1 , 1 , 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
42 ovif ⊢ ( if ( 𝑖 = 1 , 1 , 0 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) )
43 41 42 eqtrdi ⊢ ( 𝑖 ∈ ( 0 ... 𝑛 ) → ( ( ( coeff ‘ Xp ) ‘ 𝑖 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) )
44 43 adantl ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( ( ( coeff ‘ Xp ) ‘ 𝑖 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) )
45 44 sumeq2dv ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) ( ( ( coeff ‘ Xp ) ‘ 𝑖 ) · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) )
46 velsn ⊢ ( 𝑖 ∈ { 1 } ↔ 𝑖 = 1 )
47 46 bicomi ⊢ ( 𝑖 = 1 ↔ 𝑖 ∈ { 1 } )
48 47 a1i ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( 𝑖 = 1 ↔ 𝑖 ∈ { 1 } ) )
49 35 coef2 ⊢ ( ( 𝐹 ∈ ( Poly ‘ ℝ ) ∧ 0 ∈ ℝ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
50 1 12 49 sylancl ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
51 50 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
52 fznn0sub ⊢ ( 𝑖 ∈ ( 0 ... 𝑛 ) → ( 𝑛 − 𝑖 ) ∈ ℕ0 )
53 52 adantl ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( 𝑛 − 𝑖 ) ∈ ℕ0 )
54 51 53 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℝ )
55 54 recnd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ )
56 55 mullidd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) )
57 55 mul02d ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) = 0 )
58 48 56 57 ifbieq12d ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) = if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) )
59 58 sumeq2dv ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) )
60 eqeq2 ⊢ ( 0 = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) → ( Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 ↔ Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) ) )
61 eqeq2 ⊢ ( ( ( 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 ⊢ ( 𝑛 = 0 → ( 0 ... 𝑛 ) = ( 0 ... 0 ) )
63 0z ⊢ 0 ∈ ℤ
64 fzsn ⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
65 63 64 ax-mp ⊢ ( 0 ... 0 ) = { 0 }
66 62 65 eqtrdi ⊢ ( 𝑛 = 0 → ( 0 ... 𝑛 ) = { 0 } )
67 elsni ⊢ ( 𝑖 ∈ { 0 } → 𝑖 = 0 )
68 67 adantl ⊢ ( ( 𝑛 = 0 ∧ 𝑖 ∈ { 0 } ) → 𝑖 = 0 )
69 ax-1ne0 ⊢ 1 ≠ 0
70 69 nesymi ⊢ ¬ 0 = 1
71 eqeq1 ⊢ ( 𝑖 = 0 → ( 𝑖 = 1 ↔ 0 = 1 ) )
72 70 71 mtbiri ⊢ ( 𝑖 = 0 → ¬ 𝑖 = 1 )
73 47 notbii ⊢ ( ¬ 𝑖 = 1 ↔ ¬ 𝑖 ∈ { 1 } )
74 73 biimpi ⊢ ( ¬ 𝑖 = 1 → ¬ 𝑖 ∈ { 1 } )
75 iffalse ⊢ ( ¬ 𝑖 ∈ { 1 } → if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
76 68 72 74 75 4syl ⊢ ( ( 𝑛 = 0 ∧ 𝑖 ∈ { 0 } ) → if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
77 66 76 sumeq12rdv ⊢ ( 𝑛 = 0 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = Σ 𝑖 ∈ { 0 } 0 )
78 snfi ⊢ { 0 } ∈ Fin
79 78 olci ⊢ ( { 0 } ⊆ ( ℤ≥ ‘ 0 ) ∨ { 0 } ∈ Fin )
80 sumz ⊢ ( ( { 0 } ⊆ ( ℤ≥ ‘ 0 ) ∨ { 0 } ∈ Fin ) → Σ 𝑖 ∈ { 0 } 0 = 0 )
81 79 80 ax-mp ⊢ Σ 𝑖 ∈ { 0 } 0 = 0
82 77 81 eqtrdi ⊢ ( 𝑛 = 0 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
83 82 adantl ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
84 simpll ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) )
85 33 adantr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ0 )
86 simpr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ¬ 𝑛 = 0 )
87 86 neqned ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ≠ 0 )
88 elnnne0 ⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0 ) )
89 85 87 88 sylanbrc ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ )
90 1nn0 ⊢ 1 ∈ ℕ0
91 90 a1i ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℕ0 )
92 simpr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
93 92 nnnn0d ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
94 92 nnge1d ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 1 ≤ 𝑛 )
95 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 𝑛 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 1 ≤ 𝑛 ) )
96 91 93 94 95 syl3anbrc ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ ( 0 ... 𝑛 ) )
97 96 snssd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → { 1 } ⊆ ( 0 ... 𝑛 ) )
98 50 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
99 oveq2 ⊢ ( 𝑖 = 1 → ( 𝑛 − 𝑖 ) = ( 𝑛 − 1 ) )
100 46 99 sylbi ⊢ ( 𝑖 ∈ { 1 } → ( 𝑛 − 𝑖 ) = ( 𝑛 − 1 ) )
101 100 adantl ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( 𝑛 − 𝑖 ) = ( 𝑛 − 1 ) )
102 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
103 102 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( 𝑛 − 1 ) ∈ ℕ0 )
104 101 103 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( 𝑛 − 𝑖 ) ∈ ℕ0 )
105 98 104 ffvelcdmd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℝ )
106 105 recnd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ )
107 106 ralrimiva ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ )
108 fzfi ⊢ ( 0 ... 𝑛 ) ∈ Fin
109 108 olci ⊢ ( ( 0 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑛 ) ∈ Fin )
110 109 a1i ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( ( 0 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑛 ) ∈ Fin ) )
111 sumss2 ⊢ ( ( ( { 1 } ⊆ ( 0 ... 𝑛 ) ∧ ∀ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ ) ∧ ( ( 0 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑛 ) ∈ Fin ) ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) )
112 97 107 110 111 syl21anc ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) )
113 50 adantr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
114 102 adantl ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 − 1 ) ∈ ℕ0 )
115 113 114 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
116 115 recnd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
117 99 fveq2d ⊢ ( 𝑖 = 1 → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
118 117 sumsn ⊢ ( ( 1 ∈ ℝ ∧ ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ∈ ℂ ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
119 3 116 118 sylancr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
120 112 119 eqtr3d ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
121 84 89 120 syl2anc ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
122 60 61 83 121 ifbothda ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
123 59 122 eqtrd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
124 37 45 123 3eqtrd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( Xp ∘f · 𝐹 ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
125 30 124 eqtrd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
126 125 mpteq2dva ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( 𝑛 ∈ ℕ0 ↦ ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) ) )
127 16 126 eqtrd ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) ) )