MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vieta1 Structured version   Visualization version   GIF version

Theorem vieta1 26340
Description: The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas). If a polynomial of degree 𝑁 has 𝑁 distinct roots, then the sum over these roots can be calculated as -𝐴(𝑁 − 1) / 𝐴(𝑁). (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.)
Hypotheses
Ref Expression
vieta1.1 𝐴 = (coeff‘𝐹)
vieta1.2 𝑁 = (deg‘𝐹)
vieta1.3 𝑅 = (𝐹 “ {0})
vieta1.4 (𝜑𝐹 ∈ (Poly‘𝑆))
vieta1.5 (𝜑 → (♯‘𝑅) = 𝑁)
vieta1.6 (𝜑𝑁 ∈ ℕ)
Assertion
Ref Expression
vieta1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Distinct variable groups:   𝑥,𝑅   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝑆(𝑥)   𝐹(𝑥)   𝑁(𝑥)

Proof of Theorem vieta1
Dummy variables 𝑓 𝑘 𝑦 𝑧 𝑑 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vieta1.5 . 2 (𝜑 → (♯‘𝑅) = 𝑁)
2 fveq2 6901 . . . . . . 7 (𝑓 = 𝐹 → (deg‘𝑓) = (deg‘𝐹))
32eqeq2d 2737 . . . . . 6 (𝑓 = 𝐹 → (𝑁 = (deg‘𝑓) ↔ 𝑁 = (deg‘𝐹)))
4 cnveq 5880 . . . . . . . . . 10 (𝑓 = 𝐹𝑓 = 𝐹)
54imaeq1d 6068 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓 “ {0}) = (𝐹 “ {0}))
6 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
75, 6eqtr4di 2784 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓 “ {0}) = 𝑅)
87fveq2d 6905 . . . . . . 7 (𝑓 = 𝐹 → (♯‘(𝑓 “ {0})) = (♯‘𝑅))
9 vieta1.2 . . . . . . . 8 𝑁 = (deg‘𝐹)
102, 9eqtr4di 2784 . . . . . . 7 (𝑓 = 𝐹 → (deg‘𝑓) = 𝑁)
118, 10eqeq12d 2742 . . . . . 6 (𝑓 = 𝐹 → ((♯‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘𝑅) = 𝑁))
123, 11anbi12d 630 . . . . 5 (𝑓 = 𝐹 → ((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑁 = (deg‘𝐹) ∧ (♯‘𝑅) = 𝑁)))
139biantrur 529 . . . . 5 ((♯‘𝑅) = 𝑁 ↔ (𝑁 = (deg‘𝐹) ∧ (♯‘𝑅) = 𝑁))
1412, 13bitr4di 288 . . . 4 (𝑓 = 𝐹 → ((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (♯‘𝑅) = 𝑁))
157sumeq1d 15705 . . . . 5 (𝑓 = 𝐹 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥𝑅 𝑥)
16 fveq2 6901 . . . . . . . . 9 (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
17 vieta1.1 . . . . . . . . 9 𝐴 = (coeff‘𝐹)
1816, 17eqtr4di 2784 . . . . . . . 8 (𝑓 = 𝐹 → (coeff‘𝑓) = 𝐴)
1910oveq1d 7439 . . . . . . . 8 (𝑓 = 𝐹 → ((deg‘𝑓) − 1) = (𝑁 − 1))
2018, 19fveq12d 6908 . . . . . . 7 (𝑓 = 𝐹 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = (𝐴‘(𝑁 − 1)))
2118, 10fveq12d 6908 . . . . . . 7 (𝑓 = 𝐹 → ((coeff‘𝑓)‘(deg‘𝑓)) = (𝐴𝑁))
2220, 21oveq12d 7442 . . . . . 6 (𝑓 = 𝐹 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
2322negeqd 11504 . . . . 5 (𝑓 = 𝐹 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
2415, 23eqeq12d 2742 . . . 4 (𝑓 = 𝐹 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁))))
2514, 24imbi12d 343 . . 3 (𝑓 = 𝐹 → (((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((♯‘𝑅) = 𝑁 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))))
26 vieta1.6 . . . 4 (𝜑𝑁 ∈ ℕ)
27 eqeq1 2730 . . . . . . . 8 (𝑦 = 1 → (𝑦 = (deg‘𝑓) ↔ 1 = (deg‘𝑓)))
2827anbi1d 629 . . . . . . 7 (𝑦 = 1 → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
2928imbi1d 340 . . . . . 6 (𝑦 = 1 → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
3029ralbidv 3168 . . . . 5 (𝑦 = 1 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
31 eqeq1 2730 . . . . . . . 8 (𝑦 = 𝑑 → (𝑦 = (deg‘𝑓) ↔ 𝑑 = (deg‘𝑓)))
3231anbi1d 629 . . . . . . 7 (𝑦 = 𝑑 → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
3332imbi1d 340 . . . . . 6 (𝑦 = 𝑑 → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
3433ralbidv 3168 . . . . 5 (𝑦 = 𝑑 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
35 eqeq1 2730 . . . . . . . 8 (𝑦 = (𝑑 + 1) → (𝑦 = (deg‘𝑓) ↔ (𝑑 + 1) = (deg‘𝑓)))
3635anbi1d 629 . . . . . . 7 (𝑦 = (𝑑 + 1) → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ ((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
3736imbi1d 340 . . . . . 6 (𝑦 = (𝑑 + 1) → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ (((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
3837ralbidv 3168 . . . . 5 (𝑦 = (𝑑 + 1) → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
39 eqeq1 2730 . . . . . . . 8 (𝑦 = 𝑁 → (𝑦 = (deg‘𝑓) ↔ 𝑁 = (deg‘𝑓)))
4039anbi1d 629 . . . . . . 7 (𝑦 = 𝑁 → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
4140imbi1d 340 . . . . . 6 (𝑦 = 𝑁 → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
4241ralbidv 3168 . . . . 5 (𝑦 = 𝑁 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
43 eqid 2726 . . . . . . . . . . . . . . 15 (coeff‘𝑓) = (coeff‘𝑓)
4443coef3 26259 . . . . . . . . . . . . . 14 (𝑓 ∈ (Poly‘ℂ) → (coeff‘𝑓):ℕ0⟶ℂ)
4544adantr 479 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (coeff‘𝑓):ℕ0⟶ℂ)
46 0nn0 12539 . . . . . . . . . . . . 13 0 ∈ ℕ0
47 ffvelcdm 7095 . . . . . . . . . . . . 13 (((coeff‘𝑓):ℕ0⟶ℂ ∧ 0 ∈ ℕ0) → ((coeff‘𝑓)‘0) ∈ ℂ)
4845, 46, 47sylancl 584 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘0) ∈ ℂ)
49 1nn0 12540 . . . . . . . . . . . . 13 1 ∈ ℕ0
50 ffvelcdm 7095 . . . . . . . . . . . . 13 (((coeff‘𝑓):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((coeff‘𝑓)‘1) ∈ ℂ)
5145, 49, 50sylancl 584 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) ∈ ℂ)
52 simpr 483 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 1 = (deg‘𝑓))
5352fveq2d 6905 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) = ((coeff‘𝑓)‘(deg‘𝑓)))
54 ax-1ne0 11227 . . . . . . . . . . . . . . . . 17 1 ≠ 0
5554a1i 11 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 1 ≠ 0)
5652, 55eqnetrrd 2999 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (deg‘𝑓) ≠ 0)
57 fveq2 6901 . . . . . . . . . . . . . . . . 17 (𝑓 = 0𝑝 → (deg‘𝑓) = (deg‘0𝑝))
58 dgr0 26290 . . . . . . . . . . . . . . . . 17 (deg‘0𝑝) = 0
5957, 58eqtrdi 2782 . . . . . . . . . . . . . . . 16 (𝑓 = 0𝑝 → (deg‘𝑓) = 0)
6059necon3i 2963 . . . . . . . . . . . . . . 15 ((deg‘𝑓) ≠ 0 → 𝑓 ≠ 0𝑝)
6156, 60syl 17 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 𝑓 ≠ 0𝑝)
62 eqid 2726 . . . . . . . . . . . . . . . . 17 (deg‘𝑓) = (deg‘𝑓)
6362, 43dgreq0 26293 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Poly‘ℂ) → (𝑓 = 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) = 0))
6463necon3bid 2975 . . . . . . . . . . . . . . 15 (𝑓 ∈ (Poly‘ℂ) → (𝑓 ≠ 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0))
6564adantr 479 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓 ≠ 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0))
6661, 65mpbid 231 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0)
6753, 66eqnetrd 2998 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) ≠ 0)
6848, 51, 67divcld 12041 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ)
6968negcld 11608 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ)
70 id 22 . . . . . . . . . . 11 (𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) → 𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
7170sumsn 15750 . . . . . . . . . 10 ((-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
7269, 69, 71syl2anc 582 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
7372adantrr 715 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
74 eqid 2726 . . . . . . . . . . . . . 14 (𝑓 “ {0}) = (𝑓 “ {0})
7574fta1 26336 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 𝑓 ≠ 0𝑝) → ((𝑓 “ {0}) ∈ Fin ∧ (♯‘(𝑓 “ {0})) ≤ (deg‘𝑓)))
7661, 75syldan 589 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((𝑓 “ {0}) ∈ Fin ∧ (♯‘(𝑓 “ {0})) ≤ (deg‘𝑓)))
7776simpld 493 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓 “ {0}) ∈ Fin)
7877adantrr 715 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → (𝑓 “ {0}) ∈ Fin)
7943, 62coeid2 26266 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
8069, 79syldan 589 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
8152oveq2d 7440 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (0...1) = (0...(deg‘𝑓)))
8281sumeq1d 15705 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
83 nn0uz 12916 . . . . . . . . . . . . . . . 16 0 = (ℤ‘0)
84 1e0p1 12771 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
85 fveq2 6901 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ((coeff‘𝑓)‘𝑘) = ((coeff‘𝑓)‘1))
86 oveq2 7432 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) = (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))
8785, 86oveq12d 7442 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)))
8845ffvelcdmda 7098 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → ((coeff‘𝑓)‘𝑘) ∈ ℂ)
89 expcl 14099 . . . . . . . . . . . . . . . . . 18 ((-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) ∈ ℂ)
9069, 89sylan 578 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) ∈ ℂ)
9188, 90mulcld 11284 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) ∈ ℂ)
92 0z 12621 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℤ
9369exp0d 14159 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0) = 1)
9493oveq2d 7440 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) = (((coeff‘𝑓)‘0) · 1))
9548mulridd 11281 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · 1) = ((coeff‘𝑓)‘0))
9694, 95eqtrd 2766 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) = ((coeff‘𝑓)‘0))
9796, 48eqeltrd 2826 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) ∈ ℂ)
98 fveq2 6901 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → ((coeff‘𝑓)‘𝑘) = ((coeff‘𝑓)‘0))
99 oveq2 7432 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) = (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0))
10098, 99oveq12d 7442 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
101100fsum1 15751 . . . . . . . . . . . . . . . . . . 19 ((0 ∈ ℤ ∧ (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
10292, 97, 101sylancr 585 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
103102, 96eqtrd 2766 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = ((coeff‘𝑓)‘0))
104103, 46jctil 518 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (0 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = ((coeff‘𝑓)‘0)))
10569exp1d 14160 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1) = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
106105oveq2d 7440 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)) = (((coeff‘𝑓)‘1) · -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))))
10751, 68mulneg2d 11718 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = -(((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))))
10848, 51, 67divcan2d 12043 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = ((coeff‘𝑓)‘0))
109108negeqd 11504 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = -((coeff‘𝑓)‘0))
110106, 107, 1093eqtrd 2770 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)) = -((coeff‘𝑓)‘0))
111110oveq2d 7440 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))) = (((coeff‘𝑓)‘0) + -((coeff‘𝑓)‘0)))
11248negidd 11611 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + -((coeff‘𝑓)‘0)) = 0)
113111, 112eqtrd 2766 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))) = 0)
11483, 84, 87, 91, 104, 113fsump1i 15773 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (1 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = 0))
115114simprd 494 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = 0)
11680, 82, 1153eqtr2d 2772 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)
117 plyf 26225 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Poly‘ℂ) → 𝑓:ℂ⟶ℂ)
118117ffnd 6729 . . . . . . . . . . . . . . 15 (𝑓 ∈ (Poly‘ℂ) → 𝑓 Fn ℂ)
119118adantr 479 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 𝑓 Fn ℂ)
120 fniniseg 7073 . . . . . . . . . . . . . 14 (𝑓 Fn ℂ → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ (𝑓 “ {0}) ↔ (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)))
121119, 120syl 17 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ (𝑓 “ {0}) ↔ (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)))
12269, 116, 121mpbir2and 711 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ (𝑓 “ {0}))
123122snssd 4818 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}))
124123adantrr 715 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}))
125 hashsng 14386 . . . . . . . . . . . . . . 15 (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = 1)
12669, 125syl 17 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = 1)
127126, 52eqtrd 2766 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (deg‘𝑓))
128127adantrr 715 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (deg‘𝑓))
129 simprr 771 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → (♯‘(𝑓 “ {0})) = (deg‘𝑓))
130128, 129eqtr4d 2769 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (♯‘(𝑓 “ {0})))
131 snfi 9081 . . . . . . . . . . . . 13 {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ∈ Fin
132 hashen 14364 . . . . . . . . . . . . 13 (({-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ∈ Fin ∧ (𝑓 “ {0}) ∈ Fin) → ((♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (♯‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
133131, 77, 132sylancr 585 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (♯‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
134133adantrr 715 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → ((♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (♯‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
135130, 134mpbid 231 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0}))
136 fisseneq 9291 . . . . . . . . . 10 (((𝑓 “ {0}) ∈ Fin ∧ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}) ∧ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} = (𝑓 “ {0}))
13778, 124, 135, 136syl3anc 1368 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} = (𝑓 “ {0}))
138137sumeq1d 15705 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = Σ𝑥 ∈ (𝑓 “ {0})𝑥)
139 1m1e0 12336 . . . . . . . . . . . . 13 (1 − 1) = 0
14052oveq1d 7439 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (1 − 1) = ((deg‘𝑓) − 1))
141139, 140eqtr3id 2780 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 0 = ((deg‘𝑓) − 1))
142141fveq2d 6905 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘0) = ((coeff‘𝑓)‘((deg‘𝑓) − 1)))
143142, 53oveq12d 7442 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
144143negeqd 11504 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
145144adantrr 715 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
14673, 138, 1453eqtr3d 2774 . . . . . . 7 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
147146ex 411 . . . . . 6 (𝑓 ∈ (Poly‘ℂ) → ((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
148147rgen 3053 . . . . 5 𝑓 ∈ (Poly‘ℂ)((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
149 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑦 = 𝑥)
150149cbvsumv 15700 . . . . . . . . . . 11 Σ𝑦 ∈ (𝑓 “ {0})𝑦 = Σ𝑥 ∈ (𝑓 “ {0})𝑥
151150eqeq1i 2731 . . . . . . . . . 10 𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
152151imbi2i 335 . . . . . . . . 9 (((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
153152ralbii 3083 . . . . . . . 8 (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
154 eqid 2726 . . . . . . . . . 10 (coeff‘𝑔) = (coeff‘𝑔)
155 eqid 2726 . . . . . . . . . 10 (deg‘𝑔) = (deg‘𝑔)
156 eqid 2726 . . . . . . . . . 10 (𝑔 “ {0}) = (𝑔 “ {0})
157 simp1r 1195 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → 𝑔 ∈ (Poly‘ℂ))
158 simp3r 1199 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → (♯‘(𝑔 “ {0})) = (deg‘𝑔))
159 simp1l 1194 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → 𝑑 ∈ ℕ)
160 simp3l 1198 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → (𝑑 + 1) = (deg‘𝑔))
161 simp2 1134 . . . . . . . . . . 11 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
162161, 153sylib 217 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
163 eqid 2726 . . . . . . . . . 10 (𝑔 quot (Xpf − (ℂ × {𝑧}))) = (𝑔 quot (Xpf − (ℂ × {𝑧})))
164154, 155, 156, 157, 158, 159, 160, 162, 163vieta1lem2 26339 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))
1651643exp 1116 . . . . . . . 8 ((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → (((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
166153, 165biimtrrid 242 . . . . . . 7 ((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → (((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
167166ralrimdva 3144 . . . . . 6 (𝑑 ∈ ℕ → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ∀𝑔 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
168 fveq2 6901 . . . . . . . . . 10 (𝑔 = 𝑓 → (deg‘𝑔) = (deg‘𝑓))
169168eqeq2d 2737 . . . . . . . . 9 (𝑔 = 𝑓 → ((𝑑 + 1) = (deg‘𝑔) ↔ (𝑑 + 1) = (deg‘𝑓)))
170 cnveq 5880 . . . . . . . . . . . 12 (𝑔 = 𝑓𝑔 = 𝑓)
171170imaeq1d 6068 . . . . . . . . . . 11 (𝑔 = 𝑓 → (𝑔 “ {0}) = (𝑓 “ {0}))
172171fveq2d 6905 . . . . . . . . . 10 (𝑔 = 𝑓 → (♯‘(𝑔 “ {0})) = (♯‘(𝑓 “ {0})))
173172, 168eqeq12d 2742 . . . . . . . . 9 (𝑔 = 𝑓 → ((♯‘(𝑔 “ {0})) = (deg‘𝑔) ↔ (♯‘(𝑓 “ {0})) = (deg‘𝑓)))
174169, 173anbi12d 630 . . . . . . . 8 (𝑔 = 𝑓 → (((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) ↔ ((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
175171sumeq1d 15705 . . . . . . . . 9 (𝑔 = 𝑓 → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = Σ𝑥 ∈ (𝑓 “ {0})𝑥)
176 fveq2 6901 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (coeff‘𝑔) = (coeff‘𝑓))
177168oveq1d 7439 . . . . . . . . . . . 12 (𝑔 = 𝑓 → ((deg‘𝑔) − 1) = ((deg‘𝑓) − 1))
178176, 177fveq12d 6908 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((coeff‘𝑔)‘((deg‘𝑔) − 1)) = ((coeff‘𝑓)‘((deg‘𝑓) − 1)))
179176, 168fveq12d 6908 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((coeff‘𝑔)‘(deg‘𝑔)) = ((coeff‘𝑓)‘(deg‘𝑓)))
180178, 179oveq12d 7442 . . . . . . . . . 10 (𝑔 = 𝑓 → (((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) = (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
181180negeqd 11504 . . . . . . . . 9 (𝑔 = 𝑓 → -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
182175, 181eqeq12d 2742 . . . . . . . 8 (𝑔 = 𝑓 → (Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) ↔ Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
183174, 182imbi12d 343 . . . . . . 7 (𝑔 = 𝑓 → ((((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔)))) ↔ (((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
184183cbvralvw 3225 . . . . . 6 (∀𝑔 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
185167, 184imbitrdi 250 . . . . 5 (𝑑 ∈ ℕ → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
18630, 34, 38, 42, 148, 185nnind 12282 . . . 4 (𝑁 ∈ ℕ → ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
18726, 186syl 17 . . 3 (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
188 plyssc 26227 . . . 4 (Poly‘𝑆) ⊆ (Poly‘ℂ)
189 vieta1.4 . . . 4 (𝜑𝐹 ∈ (Poly‘𝑆))
190188, 189sselid 3977 . . 3 (𝜑𝐹 ∈ (Poly‘ℂ))
19125, 187, 190rspcdva 3609 . 2 (𝜑 → ((♯‘𝑅) = 𝑁 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁))))
1921, 191mpd 15 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wral 3051  wss 3947  {csn 4633   class class class wbr 5153   × cxp 5680  ccnv 5681  cima 5685   Fn wfn 6549  wf 6550  cfv 6554  (class class class)co 7424  f cof 7688  cen 8971  Fincfn 8974  cc 11156  0cc0 11158  1c1 11159   + caddc 11161   · cmul 11163  cle 11299  cmin 11494  -cneg 11495   / cdiv 11921  cn 12264  0cn0 12524  cz 12610  ...cfz 13538  cexp 14081  chash 14347  Σcsu 15690  0𝑝c0p 25689  Polycply 26211  Xpcidp 26212  coeffccoe 26213  degcdgr 26214   quot cquot 26318
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-inf2 9684  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-se 5638  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-isom 6563  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7690  df-om 7877  df-1st 8003  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-1o 8496  df-oadd 8500  df-er 8734  df-map 8857  df-pm 8858  df-en 8975  df-dom 8976  df-sdom 8977  df-fin 8978  df-sup 9485  df-inf 9486  df-oi 9553  df-dju 9944  df-card 9982  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12597  df-z 12611  df-uz 12875  df-rp 13029  df-fz 13539  df-fzo 13682  df-fl 13812  df-seq 14022  df-exp 14082  df-hash 14348  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241  df-clim 15490  df-rlim 15491  df-sum 15691  df-0p 25690  df-ply 26215  df-idp 26216  df-coe 26217  df-dgr 26218  df-quot 26319
This theorem is referenced by:  basellem5  27113
  Copyright terms: Public domain W3C validator