Metamath Proof Explorer

Theorem plymulx0

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

Ref Expression
Assertion plymulx0 ⊢F∈Poly⁡ℝ∖0𝑝→coeff⁡F×fXp=n∈ℕ0⟼ifn=00coeff⁡F⁡n−1

Proof

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