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