Metamath Proof Explorer


Theorem vieta1

Description: The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas ). If a polynomial of degree N has N distinct roots, then the sum over these roots can be calculated as -u A ( N - 1 ) / A ( N ) . (If the roots are not distinct, then this formula is still true but must double-count some of the roots according to their multiplicities.) (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses vieta1.1 A=coeffF
vieta1.2 N=degF
vieta1.3 R=F-10
vieta1.4 φFPolyS
vieta1.5 φR=N
vieta1.6 φN
Assertion vieta1 φxRx=AN1AN

Proof

Step Hyp Ref Expression
1 vieta1.1 A=coeffF
2 vieta1.2 N=degF
3 vieta1.3 R=F-10
4 vieta1.4 φFPolyS
5 vieta1.5 φR=N
6 vieta1.6 φN
7 fveq2 f=Fdegf=degF
8 7 eqeq2d f=FN=degfN=degF
9 cnveq f=Ff-1=F-1
10 9 imaeq1d f=Ff-10=F-10
11 10 3 eqtr4di f=Ff-10=R
12 11 fveq2d f=Ff-10=R
13 7 2 eqtr4di f=Fdegf=N
14 12 13 eqeq12d f=Ff-10=degfR=N
15 8 14 anbi12d f=FN=degff-10=degfN=degFR=N
16 2 biantrur R=NN=degFR=N
17 15 16 bitr4di f=FN=degff-10=degfR=N
18 11 sumeq1d f=Fxf-10x=xRx
19 fveq2 f=Fcoefff=coeffF
20 19 1 eqtr4di f=Fcoefff=A
21 13 oveq1d f=Fdegf1=N1
22 20 21 fveq12d f=Fcoefffdegf1=AN1
23 20 13 fveq12d f=Fcoefffdegf=AN
24 22 23 oveq12d f=Fcoefffdegf1coefffdegf=AN1AN
25 24 negeqd f=Fcoefffdegf1coefffdegf=AN1AN
26 18 25 eqeq12d f=Fxf-10x=coefffdegf1coefffdegfxRx=AN1AN
27 17 26 imbi12d f=FN=degff-10=degfxf-10x=coefffdegf1coefffdegfR=NxRx=AN1AN
28 eqeq1 y=1y=degf1=degf
29 28 anbi1d y=1y=degff-10=degf1=degff-10=degf
30 29 imbi1d y=1y=degff-10=degfxf-10x=coefffdegf1coefffdegf1=degff-10=degfxf-10x=coefffdegf1coefffdegf
31 30 ralbidv y=1fPolyy=degff-10=degfxf-10x=coefffdegf1coefffdegffPoly1=degff-10=degfxf-10x=coefffdegf1coefffdegf
32 eqeq1 y=dy=degfd=degf
33 32 anbi1d y=dy=degff-10=degfd=degff-10=degf
34 33 imbi1d y=dy=degff-10=degfxf-10x=coefffdegf1coefffdegfd=degff-10=degfxf-10x=coefffdegf1coefffdegf
35 34 ralbidv y=dfPolyy=degff-10=degfxf-10x=coefffdegf1coefffdegffPolyd=degff-10=degfxf-10x=coefffdegf1coefffdegf
36 eqeq1 y=d+1y=degfd+1=degf
37 36 anbi1d y=d+1y=degff-10=degfd+1=degff-10=degf
38 37 imbi1d y=d+1y=degff-10=degfxf-10x=coefffdegf1coefffdegfd+1=degff-10=degfxf-10x=coefffdegf1coefffdegf
39 38 ralbidv y=d+1fPolyy=degff-10=degfxf-10x=coefffdegf1coefffdegffPolyd+1=degff-10=degfxf-10x=coefffdegf1coefffdegf
40 eqeq1 y=Ny=degfN=degf
41 40 anbi1d y=Ny=degff-10=degfN=degff-10=degf
42 41 imbi1d y=Ny=degff-10=degfxf-10x=coefffdegf1coefffdegfN=degff-10=degfxf-10x=coefffdegf1coefffdegf
43 42 ralbidv y=NfPolyy=degff-10=degfxf-10x=coefffdegf1coefffdegffPolyN=degff-10=degfxf-10x=coefffdegf1coefffdegf
44 eqid coefff=coefff
45 44 coef3 fPolycoefff:0
46 45 adantr fPoly1=degfcoefff:0
47 0nn0 00
48 ffvelcdm coefff:000coefff0
49 46 47 48 sylancl fPoly1=degfcoefff0
50 1nn0 10
51 ffvelcdm coefff:010coefff1
52 46 50 51 sylancl fPoly1=degfcoefff1
53 simpr fPoly1=degf1=degf
54 53 fveq2d fPoly1=degfcoefff1=coefffdegf
55 ax-1ne0 10
56 55 a1i fPoly1=degf10
57 53 56 eqnetrrd fPoly1=degfdegf0
58 fveq2 f=0𝑝degf=deg0𝑝
59 dgr0 deg0𝑝=0
60 58 59 eqtrdi f=0𝑝degf=0
61 60 necon3i degf0f0𝑝
62 57 61 syl fPoly1=degff0𝑝
63 eqid degf=degf
64 63 44 dgreq0 fPolyf=0𝑝coefffdegf=0
65 64 necon3bid fPolyf0𝑝coefffdegf0
66 65 adantr fPoly1=degff0𝑝coefffdegf0
67 62 66 mpbid fPoly1=degfcoefffdegf0
68 54 67 eqnetrd fPoly1=degfcoefff10
69 49 52 68 divcld fPoly1=degfcoefff0coefff1
70 69 negcld fPoly1=degfcoefff0coefff1
71 id x=coefff0coefff1x=coefff0coefff1
72 71 sumsn coefff0coefff1coefff0coefff1xcoefff0coefff1x=coefff0coefff1
73 70 70 72 syl2anc fPoly1=degfxcoefff0coefff1x=coefff0coefff1
74 73 adantrr fPoly1=degff-10=degfxcoefff0coefff1x=coefff0coefff1
75 eqid f-10=f-10
76 75 fta1 fPolyf0𝑝f-10Finf-10degf
77 62 76 syldan fPoly1=degff-10Finf-10degf
78 77 simpld fPoly1=degff-10Fin
79 78 adantrr fPoly1=degff-10=degff-10Fin
80 44 63 coeid2 fPolycoefff0coefff1fcoefff0coefff1=k=0degfcoefffkcoefff0coefff1k
81 70 80 syldan fPoly1=degffcoefff0coefff1=k=0degfcoefffkcoefff0coefff1k
82 53 oveq2d fPoly1=degf01=0degf
83 82 sumeq1d fPoly1=degfk=01coefffkcoefff0coefff1k=k=0degfcoefffkcoefff0coefff1k
84 nn0uz 0=0
85 1e0p1 1=0+1
86 fveq2 k=1coefffk=coefff1
87 oveq2 k=1coefff0coefff1k=coefff0coefff11
88 86 87 oveq12d k=1coefffkcoefff0coefff1k=coefff1coefff0coefff11
89 46 ffvelcdmda fPoly1=degfk0coefffk
90 expcl coefff0coefff1k0coefff0coefff1k
91 70 90 sylan fPoly1=degfk0coefff0coefff1k
92 89 91 mulcld fPoly1=degfk0coefffkcoefff0coefff1k
93 0z 0
94 70 exp0d fPoly1=degfcoefff0coefff10=1
95 94 oveq2d fPoly1=degfcoefff0coefff0coefff10=coefff01
96 49 mulridd fPoly1=degfcoefff01=coefff0
97 95 96 eqtrd fPoly1=degfcoefff0coefff0coefff10=coefff0
98 97 49 eqeltrd fPoly1=degfcoefff0coefff0coefff10
99 fveq2 k=0coefffk=coefff0
100 oveq2 k=0coefff0coefff1k=coefff0coefff10
101 99 100 oveq12d k=0coefffkcoefff0coefff1k=coefff0coefff0coefff10
102 101 fsum1 0coefff0coefff0coefff10k=00coefffkcoefff0coefff1k=coefff0coefff0coefff10
103 93 98 102 sylancr fPoly1=degfk=00coefffkcoefff0coefff1k=coefff0coefff0coefff10
104 103 97 eqtrd fPoly1=degfk=00coefffkcoefff0coefff1k=coefff0
105 104 47 jctil fPoly1=degf00k=00coefffkcoefff0coefff1k=coefff0
106 70 exp1d fPoly1=degfcoefff0coefff11=coefff0coefff1
107 106 oveq2d fPoly1=degfcoefff1coefff0coefff11=coefff1coefff0coefff1
108 52 69 mulneg2d fPoly1=degfcoefff1coefff0coefff1=coefff1coefff0coefff1
109 49 52 68 divcan2d fPoly1=degfcoefff1coefff0coefff1=coefff0
110 109 negeqd fPoly1=degfcoefff1coefff0coefff1=coefff0
111 107 108 110 3eqtrd fPoly1=degfcoefff1coefff0coefff11=coefff0
112 111 oveq2d fPoly1=degfcoefff0+coefff1coefff0coefff11=coefff0+coefff0
113 49 negidd fPoly1=degfcoefff0+coefff0=0
114 112 113 eqtrd fPoly1=degfcoefff0+coefff1coefff0coefff11=0
115 84 85 88 92 105 114 fsump1i fPoly1=degf10k=01coefffkcoefff0coefff1k=0
116 115 simprd fPoly1=degfk=01coefffkcoefff0coefff1k=0
117 81 83 116 3eqtr2d fPoly1=degffcoefff0coefff1=0
118 plyf fPolyf:
119 118 ffnd fPolyfFn
120 119 adantr fPoly1=degffFn
121 fniniseg fFncoefff0coefff1f-10coefff0coefff1fcoefff0coefff1=0
122 120 121 syl fPoly1=degfcoefff0coefff1f-10coefff0coefff1fcoefff0coefff1=0
123 70 117 122 mpbir2and fPoly1=degfcoefff0coefff1f-10
124 123 snssd fPoly1=degfcoefff0coefff1f-10
125 124 adantrr fPoly1=degff-10=degfcoefff0coefff1f-10
126 hashsng coefff0coefff1coefff0coefff1=1
127 70 126 syl fPoly1=degfcoefff0coefff1=1
128 127 53 eqtrd fPoly1=degfcoefff0coefff1=degf
129 128 adantrr fPoly1=degff-10=degfcoefff0coefff1=degf
130 simprr fPoly1=degff-10=degff-10=degf
131 129 130 eqtr4d fPoly1=degff-10=degfcoefff0coefff1=f-10
132 snfi coefff0coefff1Fin
133 hashen coefff0coefff1Finf-10Fincoefff0coefff1=f-10coefff0coefff1f-10
134 132 78 133 sylancr fPoly1=degfcoefff0coefff1=f-10coefff0coefff1f-10
135 134 adantrr fPoly1=degff-10=degfcoefff0coefff1=f-10coefff0coefff1f-10
136 131 135 mpbid fPoly1=degff-10=degfcoefff0coefff1f-10
137 fisseneq f-10Fincoefff0coefff1f-10coefff0coefff1f-10coefff0coefff1=f-10
138 79 125 136 137 syl3anc fPoly1=degff-10=degfcoefff0coefff1=f-10
139 138 sumeq1d fPoly1=degff-10=degfxcoefff0coefff1x=xf-10x
140 1m1e0 11=0
141 53 oveq1d fPoly1=degf11=degf1
142 140 141 eqtr3id fPoly1=degf0=degf1
143 142 fveq2d fPoly1=degfcoefff0=coefffdegf1
144 143 54 oveq12d fPoly1=degfcoefff0coefff1=coefffdegf1coefffdegf
145 144 negeqd fPoly1=degfcoefff0coefff1=coefffdegf1coefffdegf
146 145 adantrr fPoly1=degff-10=degfcoefff0coefff1=coefffdegf1coefffdegf
147 74 139 146 3eqtr3d fPoly1=degff-10=degfxf-10x=coefffdegf1coefffdegf
148 147 ex fPoly1=degff-10=degfxf-10x=coefffdegf1coefffdegf
149 148 rgen fPoly1=degff-10=degfxf-10x=coefffdegf1coefffdegf
150 id y=xy=x
151 150 cbvsumv yf-10y=xf-10x
152 151 eqeq1i yf-10y=coefffdegf1coefffdegfxf-10x=coefffdegf1coefffdegf
153 152 imbi2i d=degff-10=degfyf-10y=coefffdegf1coefffdegfd=degff-10=degfxf-10x=coefffdegf1coefffdegf
154 153 ralbii fPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegffPolyd=degff-10=degfxf-10x=coefffdegf1coefffdegf
155 eqid coeffg=coeffg
156 eqid degg=degg
157 eqid g-10=g-10
158 simp1r dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=degggPoly
159 simp3r dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggg-10=degg
160 simp1l dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggd
161 simp3l dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggd+1=degg
162 simp2 dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegf
163 162 154 sylib dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggfPolyd=degff-10=degfxf-10x=coefffdegf1coefffdegf
164 eqid gquotXpf×z=gquotXpf×z
165 155 156 157 158 159 160 161 163 164 vieta1lem2 dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggxg-10x=coeffgdegg1coeffgdegg
166 165 3exp dgPolyfPolyd=degff-10=degfyf-10y=coefffdegf1coefffdegfd+1=deggg-10=deggxg-10x=coeffgdegg1coeffgdegg
167 154 166 biimtrrid dgPolyfPolyd=degff-10=degfxf-10x=coefffdegf1coefffdegfd+1=deggg-10=deggxg-10x=coeffgdegg1coeffgdegg
168 167 ralrimdva dfPolyd=degff-10=degfxf-10x=coefffdegf1coefffdegfgPolyd+1=deggg-10=deggxg-10x=coeffgdegg1coeffgdegg
169 fveq2 g=fdegg=degf
170 169 eqeq2d g=fd+1=deggd+1=degf
171 cnveq g=fg-1=f-1
172 171 imaeq1d g=fg-10=f-10
173 172 fveq2d g=fg-10=f-10
174 173 169 eqeq12d g=fg-10=deggf-10=degf
175 170 174 anbi12d g=fd+1=deggg-10=deggd+1=degff-10=degf
176 172 sumeq1d g=fxg-10x=xf-10x
177 fveq2 g=fcoeffg=coefff
178 169 oveq1d g=fdegg1=degf1
179 177 178 fveq12d g=fcoeffgdegg1=coefffdegf1
180 177 169 fveq12d g=fcoeffgdegg=coefffdegf
181 179 180 oveq12d g=fcoeffgdegg1coeffgdegg=coefffdegf1coefffdegf
182 181 negeqd g=fcoeffgdegg1coeffgdegg=coefffdegf1coefffdegf
183 176 182 eqeq12d g=fxg-10x=coeffgdegg1coeffgdeggxf-10x=coefffdegf1coefffdegf
184 175 183 imbi12d g=fd+1=deggg-10=deggxg-10x=coeffgdegg1coeffgdeggd+1=degff-10=degfxf-10x=coefffdegf1coefffdegf
185 184 cbvralvw gPolyd+1=deggg-10=deggxg-10x=coeffgdegg1coeffgdeggfPolyd+1=degff-10=degfxf-10x=coefffdegf1coefffdegf
186 168 185 imbitrdi dfPolyd=degff-10=degfxf-10x=coefffdegf1coefffdegffPolyd+1=degff-10=degfxf-10x=coefffdegf1coefffdegf
187 31 35 39 43 149 186 nnind NfPolyN=degff-10=degfxf-10x=coefffdegf1coefffdegf
188 6 187 syl φfPolyN=degff-10=degfxf-10x=coefffdegf1coefffdegf
189 plyssc PolySPoly
190 189 4 sselid φFPoly
191 27 188 190 rspcdva φR=NxRx=AN1AN
192 5 191 mpd φxRx=AN1AN