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

Theorem vieta1 24884
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 6644 . . . . . . 7 (𝑓 = 𝐹 → (deg‘𝑓) = (deg‘𝐹))
32eqeq2d 2831 . . . . . 6 (𝑓 = 𝐹 → (𝑁 = (deg‘𝑓) ↔ 𝑁 = (deg‘𝐹)))
4 cnveq 5718 . . . . . . . . . 10 (𝑓 = 𝐹𝑓 = 𝐹)
54imaeq1d 5902 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓 “ {0}) = (𝐹 “ {0}))
6 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
75, 6syl6eqr 2873 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓 “ {0}) = 𝑅)
87fveq2d 6648 . . . . . . 7 (𝑓 = 𝐹 → (♯‘(𝑓 “ {0})) = (♯‘𝑅))
9 vieta1.2 . . . . . . . 8 𝑁 = (deg‘𝐹)
102, 9syl6eqr 2873 . . . . . . 7 (𝑓 = 𝐹 → (deg‘𝑓) = 𝑁)
118, 10eqeq12d 2836 . . . . . 6 (𝑓 = 𝐹 → ((♯‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘𝑅) = 𝑁))
123, 11anbi12d 632 . . . . 5 (𝑓 = 𝐹 → ((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑁 = (deg‘𝐹) ∧ (♯‘𝑅) = 𝑁)))
139biantrur 533 . . . . 5 ((♯‘𝑅) = 𝑁 ↔ (𝑁 = (deg‘𝐹) ∧ (♯‘𝑅) = 𝑁))
1412, 13syl6bbr 291 . . . 4 (𝑓 = 𝐹 → ((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (♯‘𝑅) = 𝑁))
157sumeq1d 15036 . . . . 5 (𝑓 = 𝐹 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥𝑅 𝑥)
16 fveq2 6644 . . . . . . . . 9 (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
17 vieta1.1 . . . . . . . . 9 𝐴 = (coeff‘𝐹)
1816, 17syl6eqr 2873 . . . . . . . 8 (𝑓 = 𝐹 → (coeff‘𝑓) = 𝐴)
1910oveq1d 7146 . . . . . . . 8 (𝑓 = 𝐹 → ((deg‘𝑓) − 1) = (𝑁 − 1))
2018, 19fveq12d 6651 . . . . . . 7 (𝑓 = 𝐹 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = (𝐴‘(𝑁 − 1)))
2118, 10fveq12d 6651 . . . . . . 7 (𝑓 = 𝐹 → ((coeff‘𝑓)‘(deg‘𝑓)) = (𝐴𝑁))
2220, 21oveq12d 7149 . . . . . 6 (𝑓 = 𝐹 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
2322negeqd 10856 . . . . 5 (𝑓 = 𝐹 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
2415, 23eqeq12d 2836 . . . 4 (𝑓 = 𝐹 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁))))
2514, 24imbi12d 347 . . 3 (𝑓 = 𝐹 → (((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((♯‘𝑅) = 𝑁 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))))
26 vieta1.6 . . . 4 (𝜑𝑁 ∈ ℕ)
27 eqeq1 2824 . . . . . . . 8 (𝑦 = 1 → (𝑦 = (deg‘𝑓) ↔ 1 = (deg‘𝑓)))
2827anbi1d 631 . . . . . . 7 (𝑦 = 1 → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
2928imbi1d 344 . . . . . 6 (𝑦 = 1 → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
3029ralbidv 3184 . . . . 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 2824 . . . . . . . 8 (𝑦 = 𝑑 → (𝑦 = (deg‘𝑓) ↔ 𝑑 = (deg‘𝑓)))
3231anbi1d 631 . . . . . . 7 (𝑦 = 𝑑 → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
3332imbi1d 344 . . . . . 6 (𝑦 = 𝑑 → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
3433ralbidv 3184 . . . . 5 (𝑦 = 𝑑 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
35 eqeq1 2824 . . . . . . . 8 (𝑦 = (𝑑 + 1) → (𝑦 = (deg‘𝑓) ↔ (𝑑 + 1) = (deg‘𝑓)))
3635anbi1d 631 . . . . . . 7 (𝑦 = (𝑑 + 1) → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ ((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
3736imbi1d 344 . . . . . 6 (𝑦 = (𝑑 + 1) → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ (((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
3837ralbidv 3184 . . . . 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 2824 . . . . . . . 8 (𝑦 = 𝑁 → (𝑦 = (deg‘𝑓) ↔ 𝑁 = (deg‘𝑓)))
4039anbi1d 631 . . . . . . 7 (𝑦 = 𝑁 → ((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
4140imbi1d 344 . . . . . 6 (𝑦 = 𝑁 → (((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
4241ralbidv 3184 . . . . 5 (𝑦 = 𝑁 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
43 eqid 2820 . . . . . . . . . . . . . . 15 (coeff‘𝑓) = (coeff‘𝑓)
4443coef3 24805 . . . . . . . . . . . . . 14 (𝑓 ∈ (Poly‘ℂ) → (coeff‘𝑓):ℕ0⟶ℂ)
4544adantr 483 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (coeff‘𝑓):ℕ0⟶ℂ)
46 0nn0 11889 . . . . . . . . . . . . 13 0 ∈ ℕ0
47 ffvelrn 6823 . . . . . . . . . . . . 13 (((coeff‘𝑓):ℕ0⟶ℂ ∧ 0 ∈ ℕ0) → ((coeff‘𝑓)‘0) ∈ ℂ)
4845, 46, 47sylancl 588 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘0) ∈ ℂ)
49 1nn0 11890 . . . . . . . . . . . . 13 1 ∈ ℕ0
50 ffvelrn 6823 . . . . . . . . . . . . 13 (((coeff‘𝑓):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((coeff‘𝑓)‘1) ∈ ℂ)
5145, 49, 50sylancl 588 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) ∈ ℂ)
52 simpr 487 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 1 = (deg‘𝑓))
5352fveq2d 6648 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) = ((coeff‘𝑓)‘(deg‘𝑓)))
54 ax-1ne0 10582 . . . . . . . . . . . . . . . . 17 1 ≠ 0
5554a1i 11 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 1 ≠ 0)
5652, 55eqnetrrd 3074 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (deg‘𝑓) ≠ 0)
57 fveq2 6644 . . . . . . . . . . . . . . . . 17 (𝑓 = 0𝑝 → (deg‘𝑓) = (deg‘0𝑝))
58 dgr0 24835 . . . . . . . . . . . . . . . . 17 (deg‘0𝑝) = 0
5957, 58syl6eq 2871 . . . . . . . . . . . . . . . 16 (𝑓 = 0𝑝 → (deg‘𝑓) = 0)
6059necon3i 3038 . . . . . . . . . . . . . . 15 ((deg‘𝑓) ≠ 0 → 𝑓 ≠ 0𝑝)
6156, 60syl 17 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 𝑓 ≠ 0𝑝)
62 eqid 2820 . . . . . . . . . . . . . . . . 17 (deg‘𝑓) = (deg‘𝑓)
6362, 43dgreq0 24838 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Poly‘ℂ) → (𝑓 = 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) = 0))
6463necon3bid 3050 . . . . . . . . . . . . . . 15 (𝑓 ∈ (Poly‘ℂ) → (𝑓 ≠ 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0))
6564adantr 483 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓 ≠ 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0))
6661, 65mpbid 234 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0)
6753, 66eqnetrd 3073 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) ≠ 0)
6848, 51, 67divcld 11392 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ)
6968negcld 10960 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ)
70 id 22 . . . . . . . . . . 11 (𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) → 𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
7170sumsn 15079 . . . . . . . . . 10 ((-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
7269, 69, 71syl2anc 586 . . . . . . . . 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 2820 . . . . . . . . . . . . . 14 (𝑓 “ {0}) = (𝑓 “ {0})
7574fta1 24880 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 𝑓 ≠ 0𝑝) → ((𝑓 “ {0}) ∈ Fin ∧ (♯‘(𝑓 “ {0})) ≤ (deg‘𝑓)))
7661, 75syldan 593 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((𝑓 “ {0}) ∈ Fin ∧ (♯‘(𝑓 “ {0})) ≤ (deg‘𝑓)))
7776simpld 497 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓 “ {0}) ∈ Fin)
7877adantrr 715 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → (𝑓 “ {0}) ∈ Fin)
7943, 62coeid2 24812 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
8069, 79syldan 593 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
8152oveq2d 7147 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (0...1) = (0...(deg‘𝑓)))
8281sumeq1d 15036 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
83 nn0uz 12257 . . . . . . . . . . . . . . . 16 0 = (ℤ‘0)
84 1e0p1 12117 . . . . . . . . . . . . . . . 16 1 = (0 + 1)
85 fveq2 6644 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ((coeff‘𝑓)‘𝑘) = ((coeff‘𝑓)‘1))
86 oveq2 7139 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) = (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))
8785, 86oveq12d 7149 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)))
8845ffvelrnda 6825 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → ((coeff‘𝑓)‘𝑘) ∈ ℂ)
89 expcl 13430 . . . . . . . . . . . . . . . . . 18 ((-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) ∈ ℂ)
9069, 89sylan 582 . . . . . . . . . . . . . . . . 17 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) ∈ ℂ)
9188, 90mulcld 10637 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) ∈ ℂ)
92 0z 11969 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℤ
9369exp0d 13487 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0) = 1)
9493oveq2d 7147 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) = (((coeff‘𝑓)‘0) · 1))
9548mulid1d 10634 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · 1) = ((coeff‘𝑓)‘0))
9694, 95eqtrd 2855 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) = ((coeff‘𝑓)‘0))
9796, 48eqeltrd 2911 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) ∈ ℂ)
98 fveq2 6644 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → ((coeff‘𝑓)‘𝑘) = ((coeff‘𝑓)‘0))
99 oveq2 7139 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) = (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0))
10098, 99oveq12d 7149 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
101100fsum1 15080 . . . . . . . . . . . . . . . . . . 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 589 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
103102, 96eqtrd 2855 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = ((coeff‘𝑓)‘0))
104103, 46jctil 522 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (0 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = ((coeff‘𝑓)‘0)))
10569exp1d 13488 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1) = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
106105oveq2d 7147 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)) = (((coeff‘𝑓)‘1) · -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))))
10751, 68mulneg2d 11070 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = -(((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))))
10848, 51, 67divcan2d 11394 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = ((coeff‘𝑓)‘0))
109108negeqd 10856 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = -((coeff‘𝑓)‘0))
110106, 107, 1093eqtrd 2859 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)) = -((coeff‘𝑓)‘0))
111110oveq2d 7147 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))) = (((coeff‘𝑓)‘0) + -((coeff‘𝑓)‘0)))
11248negidd 10963 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + -((coeff‘𝑓)‘0)) = 0)
113111, 112eqtrd 2855 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))) = 0)
11483, 84, 87, 91, 104, 113fsump1i 15102 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (1 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = 0))
115114simprd 498 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = 0)
11680, 82, 1153eqtr2d 2861 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)
117 plyf 24771 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Poly‘ℂ) → 𝑓:ℂ⟶ℂ)
118117ffnd 6489 . . . . . . . . . . . . . . 15 (𝑓 ∈ (Poly‘ℂ) → 𝑓 Fn ℂ)
119118adantr 483 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 𝑓 Fn ℂ)
120 fniniseg 6804 . . . . . . . . . . . . . 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 4716 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}))
124123adantrr 715 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}))
125 hashsng 13713 . . . . . . . . . . . . . . 15 (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = 1)
12669, 125syl 17 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = 1)
127126, 52eqtrd 2855 . . . . . . . . . . . . 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 2858 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → (♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (♯‘(𝑓 “ {0})))
131 snfi 8570 . . . . . . . . . . . . 13 {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ∈ Fin
132 hashen 13690 . . . . . . . . . . . . 13 (({-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ∈ Fin ∧ (𝑓 “ {0}) ∈ Fin) → ((♯‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (♯‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
133131, 77, 132sylancr 589 . . . . . . . . . . . 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 234 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0}))
136 fisseneq 8705 . . . . . . . . . 10 (((𝑓 “ {0}) ∈ Fin ∧ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}) ∧ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} = (𝑓 “ {0}))
13778, 124, 135, 136syl3anc 1367 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} = (𝑓 “ {0}))
138137sumeq1d 15036 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = Σ𝑥 ∈ (𝑓 “ {0})𝑥)
139 1m1e0 11686 . . . . . . . . . . . . 13 (1 − 1) = 0
14052oveq1d 7146 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (1 − 1) = ((deg‘𝑓) − 1))
141139, 140syl5eqr 2869 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 0 = ((deg‘𝑓) − 1))
142141fveq2d 6648 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘0) = ((coeff‘𝑓)‘((deg‘𝑓) − 1)))
143142, 53oveq12d 7149 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
144143negeqd 10856 . . . . . . . . 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 2863 . . . . . . 7 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
147146ex 415 . . . . . 6 (𝑓 ∈ (Poly‘ℂ) → ((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
148147rgen 3135 . . . . 5 𝑓 ∈ (Poly‘ℂ)((1 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
149 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑥𝑦 = 𝑥)
150149cbvsumv 15031 . . . . . . . . . . 11 Σ𝑦 ∈ (𝑓 “ {0})𝑦 = Σ𝑥 ∈ (𝑓 “ {0})𝑥
151150eqeq1i 2825 . . . . . . . . . 10 𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
152151imbi2i 338 . . . . . . . . 9 (((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
153152ralbii 3152 . . . . . . . 8 (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
154 eqid 2820 . . . . . . . . . 10 (coeff‘𝑔) = (coeff‘𝑔)
155 eqid 2820 . . . . . . . . . 10 (deg‘𝑔) = (deg‘𝑔)
156 eqid 2820 . . . . . . . . . 10 (𝑔 “ {0}) = (𝑔 “ {0})
157 simp1r 1194 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → 𝑔 ∈ (Poly‘ℂ))
158 simp3r 1198 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → (♯‘(𝑔 “ {0})) = (deg‘𝑔))
159 simp1l 1193 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → 𝑑 ∈ ℕ)
160 simp3l 1197 . . . . . . . . . 10 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → (𝑑 + 1) = (deg‘𝑔))
161 simp2 1133 . . . . . . . . . . 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 220 . . . . . . . . . 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 2820 . . . . . . . . . 10 (𝑔 quot (Xpf − (ℂ × {𝑧}))) = (𝑔 quot (Xpf − (ℂ × {𝑧})))
164154, 155, 156, 157, 158, 159, 160, 162, 163vieta1lem2 24883 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔))) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))
1651643exp 1115 . . . . . . . 8 ((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → (((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
166153, 165syl5bir 245 . . . . . . 7 ((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → (((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
167166ralrimdva 3176 . . . . . 6 (𝑑 ∈ ℕ → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ∀𝑔 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
168 fveq2 6644 . . . . . . . . . 10 (𝑔 = 𝑓 → (deg‘𝑔) = (deg‘𝑓))
169168eqeq2d 2831 . . . . . . . . 9 (𝑔 = 𝑓 → ((𝑑 + 1) = (deg‘𝑔) ↔ (𝑑 + 1) = (deg‘𝑓)))
170 cnveq 5718 . . . . . . . . . . . 12 (𝑔 = 𝑓𝑔 = 𝑓)
171170imaeq1d 5902 . . . . . . . . . . 11 (𝑔 = 𝑓 → (𝑔 “ {0}) = (𝑓 “ {0}))
172171fveq2d 6648 . . . . . . . . . 10 (𝑔 = 𝑓 → (♯‘(𝑔 “ {0})) = (♯‘(𝑓 “ {0})))
173172, 168eqeq12d 2836 . . . . . . . . 9 (𝑔 = 𝑓 → ((♯‘(𝑔 “ {0})) = (deg‘𝑔) ↔ (♯‘(𝑓 “ {0})) = (deg‘𝑓)))
174169, 173anbi12d 632 . . . . . . . 8 (𝑔 = 𝑓 → (((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) ↔ ((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓))))
175171sumeq1d 15036 . . . . . . . . 9 (𝑔 = 𝑓 → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = Σ𝑥 ∈ (𝑓 “ {0})𝑥)
176 fveq2 6644 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (coeff‘𝑔) = (coeff‘𝑓))
177168oveq1d 7146 . . . . . . . . . . . 12 (𝑔 = 𝑓 → ((deg‘𝑔) − 1) = ((deg‘𝑓) − 1))
178176, 177fveq12d 6651 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((coeff‘𝑔)‘((deg‘𝑔) − 1)) = ((coeff‘𝑓)‘((deg‘𝑓) − 1)))
179176, 168fveq12d 6651 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((coeff‘𝑔)‘(deg‘𝑔)) = ((coeff‘𝑓)‘(deg‘𝑓)))
180178, 179oveq12d 7149 . . . . . . . . . 10 (𝑔 = 𝑓 → (((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) = (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
181180negeqd 10856 . . . . . . . . 9 (𝑔 = 𝑓 → -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
182175, 181eqeq12d 2836 . . . . . . . 8 (𝑔 = 𝑓 → (Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) ↔ Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
183174, 182imbi12d 347 . . . . . . 7 (𝑔 = 𝑓 → ((((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔)))) ↔ (((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
184183cbvralvw 3428 . . . . . 6 (∀𝑔 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑔) ∧ (♯‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
185167, 184syl6ib 253 . . . . 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 11632 . . . 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 24773 . . . 4 (Poly‘𝑆) ⊆ (Poly‘ℂ)
189 vieta1.4 . . . 4 (𝜑𝐹 ∈ (Poly‘𝑆))
190188, 189sseldi 3941 . . 3 (𝜑𝐹 ∈ (Poly‘ℂ))
19125, 187, 190rspcdva 3604 . 2 (𝜑 → ((♯‘𝑅) = 𝑁 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁))))
1921, 191mpd 15 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398  w3a 1083   = wceq 1537  wcel 2114  wne 3006  wral 3125  wss 3912  {csn 4541   class class class wbr 5040   × cxp 5527  ccnv 5528  cima 5532   Fn wfn 6324  wf 6325  cfv 6329  (class class class)co 7131  f cof 7383  cen 8482  Fincfn 8485  cc 10511  0cc0 10513  1c1 10514   + caddc 10516   · cmul 10518  cle 10652  cmin 10846  -cneg 10847   / cdiv 11273  cn 11614  0cn0 11874  cz 11958  ...cfz 12874  cexp 13412  chash 13673  Σcsu 15020  0𝑝c0p 24249  Polycply 24757  Xpcidp 24758  coeffccoe 24759  degcdgr 24760   quot cquot 24862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5164  ax-sep 5177  ax-nul 5184  ax-pow 5240  ax-pr 5304  ax-un 7437  ax-inf2 9080  ax-cnex 10569  ax-resscn 10570  ax-1cn 10571  ax-icn 10572  ax-addcl 10573  ax-addrcl 10574  ax-mulcl 10575  ax-mulrcl 10576  ax-mulcom 10577  ax-addass 10578  ax-mulass 10579  ax-distr 10580  ax-i2m1 10581  ax-1ne0 10582  ax-1rid 10583  ax-rnegex 10584  ax-rrecex 10585  ax-cnre 10586  ax-pre-lttri 10587  ax-pre-lttrn 10588  ax-pre-ltadd 10589  ax-pre-mulgt0 10590  ax-pre-sup 10591  ax-addf 10592
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3752  df-csb 3860  df-dif 3915  df-un 3917  df-in 3919  df-ss 3928  df-pss 3930  df-nul 4268  df-if 4442  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4813  df-int 4851  df-iun 4895  df-br 5041  df-opab 5103  df-mpt 5121  df-tr 5147  df-id 5434  df-eprel 5439  df-po 5448  df-so 5449  df-fr 5488  df-se 5489  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6122  df-ord 6168  df-on 6169  df-lim 6170  df-suc 6171  df-iota 6288  df-fun 6331  df-fn 6332  df-f 6333  df-f1 6334  df-fo 6335  df-f1o 6336  df-fv 6337  df-isom 6338  df-riota 7089  df-ov 7134  df-oprab 7135  df-mpo 7136  df-of 7385  df-om 7557  df-1st 7665  df-2nd 7666  df-wrecs 7923  df-recs 7984  df-rdg 8022  df-1o 8078  df-oadd 8082  df-er 8265  df-map 8384  df-pm 8385  df-en 8486  df-dom 8487  df-sdom 8488  df-fin 8489  df-sup 8882  df-inf 8883  df-oi 8950  df-dju 9306  df-card 9344  df-pnf 10653  df-mnf 10654  df-xr 10655  df-ltxr 10656  df-le 10657  df-sub 10848  df-neg 10849  df-div 11274  df-nn 11615  df-2 11677  df-3 11678  df-n0 11875  df-xnn0 11945  df-z 11959  df-uz 12221  df-rp 12367  df-fz 12875  df-fzo 13016  df-fl 13144  df-seq 13352  df-exp 13413  df-hash 13674  df-cj 14436  df-re 14437  df-im 14438  df-sqrt 14572  df-abs 14573  df-clim 14823  df-rlim 14824  df-sum 15021  df-0p 24250  df-ply 24761  df-idp 24762  df-coe 24763  df-dgr 24764  df-quot 24863
This theorem is referenced by:  basellem5  25646
  Copyright terms: Public domain W3C validator