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 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℝ )
55 54 recnd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑖 ∈ ( 0 ... 𝑛 ) ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ )
56 55 mulid2d ⊢ ( ( ( 𝐹 ∈ ( ( 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 68 72 syl ⊢ ( ( 𝑛 = 0 ∧ 𝑖 ∈ { 0 } ) → ¬ 𝑖 = 1 )
74 47 notbii ⊢ ( ¬ 𝑖 = 1 ↔ ¬ 𝑖 ∈ { 1 } )
75 74 biimpi ⊢ ( ¬ 𝑖 = 1 → ¬ 𝑖 ∈ { 1 } )
76 iffalse ⊢ ( ¬ 𝑖 ∈ { 1 } → if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
77 73 75 76 3syl ⊢ ( ( 𝑛 = 0 ∧ 𝑖 ∈ { 0 } ) → if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
78 66 77 sumeq12rdv ⊢ ( 𝑛 = 0 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = Σ 𝑖 ∈ { 0 } 0 )
79 snfi ⊢ { 0 } ∈ Fin
80 79 olci ⊢ ( { 0 } ⊆ ( ℤ≥ ‘ 0 ) ∨ { 0 } ∈ Fin )
81 sumz ⊢ ( ( { 0 } ⊆ ( ℤ≥ ‘ 0 ) ∨ { 0 } ∈ Fin ) → Σ 𝑖 ∈ { 0 } 0 = 0 )
82 80 81 ax-mp ⊢ Σ 𝑖 ∈ { 0 } 0 = 0
83 78 82 eqtrdi ⊢ ( 𝑛 = 0 → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
84 83 adantl ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ 𝑛 = 0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = 0 )
85 simpll ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) )
86 33 adantr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ0 )
87 simpr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → ¬ 𝑛 = 0 )
88 87 neqned ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ≠ 0 )
89 elnnne0 ⊢ ( 𝑛 ∈ ℕ ↔ ( 𝑛 ∈ ℕ0 ∧ 𝑛 ≠ 0 ) )
90 86 88 89 sylanbrc ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → 𝑛 ∈ ℕ )
91 1nn0 ⊢ 1 ∈ ℕ0
92 91 a1i ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ ℕ0 )
93 simpr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ )
94 93 nnnn0d ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ℕ0 )
95 93 nnge1d ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 1 ≤ 𝑛 )
96 elfz2nn0 ⊢ ( 1 ∈ ( 0 ... 𝑛 ) ↔ ( 1 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0 ∧ 1 ≤ 𝑛 ) )
97 92 94 95 96 syl3anbrc ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → 1 ∈ ( 0 ... 𝑛 ) )
98 97 snssd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → { 1 } ⊆ ( 0 ... 𝑛 ) )
99 50 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
100 oveq2 ⊢ ( 𝑖 = 1 → ( 𝑛 − 𝑖 ) = ( 𝑛 − 1 ) )
101 46 100 sylbi ⊢ ( 𝑖 ∈ { 1 } → ( 𝑛 − 𝑖 ) = ( 𝑛 − 1 ) )
102 101 adantl ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( 𝑛 − 𝑖 ) = ( 𝑛 − 1 ) )
103 nnm1nn0 ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
104 103 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( 𝑛 − 1 ) ∈ ℕ0 )
105 102 104 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( 𝑛 − 𝑖 ) ∈ ℕ0 )
106 99 105 ffvelrnd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℝ )
107 106 recnd ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑖 ∈ { 1 } ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ )
108 107 ralrimiva ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ∀ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ )
109 fzfi ⊢ ( 0 ... 𝑛 ) ∈ Fin
110 109 olci ⊢ ( ( 0 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑛 ) ∈ Fin )
111 110 a1i ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( ( 0 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑛 ) ∈ Fin ) )
112 sumss2 ⊢ ( ( ( { 1 } ⊆ ( 0 ... 𝑛 ) ∧ ∀ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ∈ ℂ ) ∧ ( ( 0 ... 𝑛 ) ⊆ ( ℤ≥ ‘ 0 ) ∨ ( 0 ... 𝑛 ) ∈ Fin ) ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) )
113 98 108 111 112 syl21anc ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) )
114 50 adantr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( coeff ‘ 𝐹 ) : ℕ0 ⟶ ℝ )
115 103 adantl ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( 𝑛 − 1 ) ∈ ℕ0 )
116 114 115 ffvelrnd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
117 116 recnd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
118 100 fveq2d ⊢ ( 𝑖 = 1 → ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
119 118 sumsn ⊢ ( ( 1 ∈ ℝ ∧ ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ∈ ℂ ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
120 3 117 119 sylancr ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ { 1 } ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
121 113 120 eqtr3d ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
122 85 90 121 syl2anc ⊢ ( ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) ∧ ¬ 𝑛 = 0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) )
123 60 61 84 122 ifbothda ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 ∈ { 1 } , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) , 0 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
124 59 123 eqtrd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → Σ 𝑖 ∈ ( 0 ... 𝑛 ) if ( 𝑖 = 1 , ( 1 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) , ( 0 · ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 𝑖 ) ) ) ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
125 37 45 124 3eqtrd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( Xp ∘f · 𝐹 ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
126 30 125 eqtrd ⊢ ( ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) ∧ 𝑛 ∈ ℕ0 ) → ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) = if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) )
127 126 mpteq2dva ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( 𝑛 ∈ ℕ0 ↦ ( ( coeff ‘ ( 𝐹 ∘f · Xp ) ) ‘ 𝑛 ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) ) )
128 16 127 eqtrd ⊢ ( 𝐹 ∈ ( ( Poly ‘ ℝ ) ∖ { 0𝑝 } ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) ) )