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

Theorem vieta1 23816
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 plyssc 23705 . . 3 (Poly‘𝑆) ⊆ (Poly‘ℂ)
2 vieta1.4 . . 3 (𝜑𝐹 ∈ (Poly‘𝑆))
31, 2sseldi 3566 . 2 (𝜑𝐹 ∈ (Poly‘ℂ))
4 vieta1.6 . . 3 (𝜑𝑁 ∈ ℕ)
5 eqeq1 2614 . . . . . . 7 (𝑦 = 1 → (𝑦 = (deg‘𝑓) ↔ 1 = (deg‘𝑓)))
65anbi1d 737 . . . . . 6 (𝑦 = 1 → ((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))))
76imbi1d 330 . . . . 5 (𝑦 = 1 → (((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
87ralbidv 2969 . . . 4 (𝑦 = 1 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
9 eqeq1 2614 . . . . . . 7 (𝑦 = 𝑑 → (𝑦 = (deg‘𝑓) ↔ 𝑑 = (deg‘𝑓)))
109anbi1d 737 . . . . . 6 (𝑦 = 𝑑 → ((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))))
1110imbi1d 330 . . . . 5 (𝑦 = 𝑑 → (((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
1211ralbidv 2969 . . . 4 (𝑦 = 𝑑 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
13 eqeq1 2614 . . . . . . 7 (𝑦 = (𝑑 + 1) → (𝑦 = (deg‘𝑓) ↔ (𝑑 + 1) = (deg‘𝑓)))
1413anbi1d 737 . . . . . 6 (𝑦 = (𝑑 + 1) → ((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ ((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))))
1514imbi1d 330 . . . . 5 (𝑦 = (𝑑 + 1) → (((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ (((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
1615ralbidv 2969 . . . 4 (𝑦 = (𝑑 + 1) → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
17 eqeq1 2614 . . . . . . 7 (𝑦 = 𝑁 → (𝑦 = (deg‘𝑓) ↔ 𝑁 = (deg‘𝑓)))
1817anbi1d 737 . . . . . 6 (𝑦 = 𝑁 → ((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))))
1918imbi1d 330 . . . . 5 (𝑦 = 𝑁 → (((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
2019ralbidv 2969 . . . 4 (𝑦 = 𝑁 → (∀𝑓 ∈ (Poly‘ℂ)((𝑦 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
21 eqid 2610 . . . . . . . . . . . . . 14 (coeff‘𝑓) = (coeff‘𝑓)
2221coef3 23737 . . . . . . . . . . . . 13 (𝑓 ∈ (Poly‘ℂ) → (coeff‘𝑓):ℕ0⟶ℂ)
2322adantr 480 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (coeff‘𝑓):ℕ0⟶ℂ)
24 0nn0 11157 . . . . . . . . . . . 12 0 ∈ ℕ0
25 ffvelrn 6250 . . . . . . . . . . . 12 (((coeff‘𝑓):ℕ0⟶ℂ ∧ 0 ∈ ℕ0) → ((coeff‘𝑓)‘0) ∈ ℂ)
2623, 24, 25sylancl 693 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘0) ∈ ℂ)
27 1nn0 11158 . . . . . . . . . . . 12 1 ∈ ℕ0
28 ffvelrn 6250 . . . . . . . . . . . 12 (((coeff‘𝑓):ℕ0⟶ℂ ∧ 1 ∈ ℕ0) → ((coeff‘𝑓)‘1) ∈ ℂ)
2923, 27, 28sylancl 693 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) ∈ ℂ)
30 simpr 476 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 1 = (deg‘𝑓))
3130fveq2d 6092 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) = ((coeff‘𝑓)‘(deg‘𝑓)))
32 ax-1ne0 9862 . . . . . . . . . . . . . . . 16 1 ≠ 0
3332a1i 11 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 1 ≠ 0)
3430, 33eqnetrrd 2850 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (deg‘𝑓) ≠ 0)
35 fveq2 6088 . . . . . . . . . . . . . . . 16 (𝑓 = 0𝑝 → (deg‘𝑓) = (deg‘0𝑝))
36 dgr0 23767 . . . . . . . . . . . . . . . 16 (deg‘0𝑝) = 0
3735, 36syl6eq 2660 . . . . . . . . . . . . . . 15 (𝑓 = 0𝑝 → (deg‘𝑓) = 0)
3837necon3i 2814 . . . . . . . . . . . . . 14 ((deg‘𝑓) ≠ 0 → 𝑓 ≠ 0𝑝)
3934, 38syl 17 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 𝑓 ≠ 0𝑝)
40 eqid 2610 . . . . . . . . . . . . . . . 16 (deg‘𝑓) = (deg‘𝑓)
4140, 21dgreq0 23770 . . . . . . . . . . . . . . 15 (𝑓 ∈ (Poly‘ℂ) → (𝑓 = 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) = 0))
4241necon3bid 2826 . . . . . . . . . . . . . 14 (𝑓 ∈ (Poly‘ℂ) → (𝑓 ≠ 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0))
4342adantr 480 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓 ≠ 0𝑝 ↔ ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0))
4439, 43mpbid 221 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘(deg‘𝑓)) ≠ 0)
4531, 44eqnetrd 2849 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘1) ≠ 0)
4626, 29, 45divcld 10653 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ)
4746negcld 10231 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ)
48 id 22 . . . . . . . . . 10 (𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) → 𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
4948sumsn 14268 . . . . . . . . 9 ((-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
5047, 47, 49syl2anc 691 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
5150adantrr 749 . . . . . . 7 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
52 eqid 2610 . . . . . . . . . . . . 13 (𝑓 “ {0}) = (𝑓 “ {0})
5352fta1 23812 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 𝑓 ≠ 0𝑝) → ((𝑓 “ {0}) ∈ Fin ∧ (#‘(𝑓 “ {0})) ≤ (deg‘𝑓)))
5439, 53syldan 486 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((𝑓 “ {0}) ∈ Fin ∧ (#‘(𝑓 “ {0})) ≤ (deg‘𝑓)))
5554simpld 474 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓 “ {0}) ∈ Fin)
5655adantrr 749 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → (𝑓 “ {0}) ∈ Fin)
5721, 40coeid2 23744 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
5847, 57syldan 486 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
5930oveq2d 6543 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (0...1) = (0...(deg‘𝑓)))
6059sumeq1d 14228 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = Σ𝑘 ∈ (0...(deg‘𝑓))(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)))
61 nn0uz 11557 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
62 1e0p1 11387 . . . . . . . . . . . . . . 15 1 = (0 + 1)
63 fveq2 6088 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → ((coeff‘𝑓)‘𝑘) = ((coeff‘𝑓)‘1))
64 oveq2 6535 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) = (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))
6563, 64oveq12d 6545 . . . . . . . . . . . . . . 15 (𝑘 = 1 → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)))
6623ffvelrnda 6252 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → ((coeff‘𝑓)‘𝑘) ∈ ℂ)
67 expcl 12698 . . . . . . . . . . . . . . . . 17 ((-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ 𝑘 ∈ ℕ0) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) ∈ ℂ)
6847, 67sylan 487 . . . . . . . . . . . . . . . 16 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) ∈ ℂ)
6966, 68mulcld 9917 . . . . . . . . . . . . . . 15 (((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) ∧ 𝑘 ∈ ℕ0) → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) ∈ ℂ)
70 0z 11224 . . . . . . . . . . . . . . . . . 18 0 ∈ ℤ
7147exp0d 12822 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0) = 1)
7271oveq2d 6543 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) = (((coeff‘𝑓)‘0) · 1))
7326mulid1d 9914 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · 1) = ((coeff‘𝑓)‘0))
7472, 73eqtrd 2644 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) = ((coeff‘𝑓)‘0))
7574, 26eqeltrd 2688 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) ∈ ℂ)
76 fveq2 6088 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → ((coeff‘𝑓)‘𝑘) = ((coeff‘𝑓)‘0))
77 oveq2 6535 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘) = (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0))
7876, 77oveq12d 6545 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
7978fsum1 14269 . . . . . . . . . . . . . . . . . 18 ((0 ∈ ℤ ∧ (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
8070, 75, 79sylancr 694 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = (((coeff‘𝑓)‘0) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑0)))
8180, 74eqtrd 2644 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = ((coeff‘𝑓)‘0))
8281, 24jctil 558 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (0 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...0)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = ((coeff‘𝑓)‘0)))
8347exp1d 12823 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1) = -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)))
8483oveq2d 6543 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)) = (((coeff‘𝑓)‘1) · -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))))
8529, 46mulneg2d 10336 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = -(((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))))
8626, 29, 45divcan2d 10655 . . . . . . . . . . . . . . . . . . 19 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = ((coeff‘𝑓)‘0))
8786negeqd 10127 . . . . . . . . . . . . . . . . . 18 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘1) · (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = -((coeff‘𝑓)‘0))
8884, 85, 873eqtrd 2648 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1)) = -((coeff‘𝑓)‘0))
8988oveq2d 6543 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))) = (((coeff‘𝑓)‘0) + -((coeff‘𝑓)‘0)))
9026negidd 10234 . . . . . . . . . . . . . . . 16 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + -((coeff‘𝑓)‘0)) = 0)
9189, 90eqtrd 2644 . . . . . . . . . . . . . . 15 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) + (((coeff‘𝑓)‘1) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑1))) = 0)
9261, 62, 65, 69, 82, 91fsump1i 14291 . . . . . . . . . . . . . 14 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (1 ∈ ℕ0 ∧ Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = 0))
9392simprd 478 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → Σ𝑘 ∈ (0...1)(((coeff‘𝑓)‘𝑘) · (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))↑𝑘)) = 0)
9458, 60, 933eqtr2d 2650 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)
95 plyf 23703 . . . . . . . . . . . . . . 15 (𝑓 ∈ (Poly‘ℂ) → 𝑓:ℂ⟶ℂ)
96 ffn 5944 . . . . . . . . . . . . . . 15 (𝑓:ℂ⟶ℂ → 𝑓 Fn ℂ)
9795, 96syl 17 . . . . . . . . . . . . . 14 (𝑓 ∈ (Poly‘ℂ) → 𝑓 Fn ℂ)
9897adantr 480 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 𝑓 Fn ℂ)
99 fniniseg 6231 . . . . . . . . . . . . 13 (𝑓 Fn ℂ → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ (𝑓 “ {0}) ↔ (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)))
10098, 99syl 17 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ (𝑓 “ {0}) ↔ (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ ∧ (𝑓‘-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))) = 0)))
10147, 94, 100mpbir2and 959 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ (𝑓 “ {0}))
102101snssd 4281 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}))
103102adantrr 749 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}))
104 hashsng 12975 . . . . . . . . . . . . . 14 (-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) ∈ ℂ → (#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = 1)
10547, 104syl 17 . . . . . . . . . . . . 13 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = 1)
106105, 30eqtrd 2644 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (deg‘𝑓))
107106adantrr 749 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → (#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (deg‘𝑓))
108 simprr 792 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → (#‘(𝑓 “ {0})) = (deg‘𝑓))
109107, 108eqtr4d 2647 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → (#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (#‘(𝑓 “ {0})))
110 snfi 7901 . . . . . . . . . . . 12 {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ∈ Fin
111 hashen 12952 . . . . . . . . . . . 12 (({-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ∈ Fin ∧ (𝑓 “ {0}) ∈ Fin) → ((#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (#‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
112110, 55, 111sylancr 694 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (#‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
113112adantrr 749 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → ((#‘{-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}) = (#‘(𝑓 “ {0})) ↔ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})))
114109, 113mpbid 221 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0}))
115 fisseneq 8034 . . . . . . . . 9 (((𝑓 “ {0}) ∈ Fin ∧ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ⊆ (𝑓 “ {0}) ∧ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} ≈ (𝑓 “ {0})) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} = (𝑓 “ {0}))
11656, 103, 114, 115syl3anc 1318 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))} = (𝑓 “ {0}))
117116sumeq1d 14228 . . . . . . 7 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ {-(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1))}𝑥 = Σ𝑥 ∈ (𝑓 “ {0})𝑥)
118 1m1e0 10939 . . . . . . . . . . . 12 (1 − 1) = 0
11930oveq1d 6542 . . . . . . . . . . . 12 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (1 − 1) = ((deg‘𝑓) − 1))
120118, 119syl5eqr 2658 . . . . . . . . . . 11 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → 0 = ((deg‘𝑓) − 1))
121120fveq2d 6092 . . . . . . . . . 10 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → ((coeff‘𝑓)‘0) = ((coeff‘𝑓)‘((deg‘𝑓) − 1)))
122121, 31oveq12d 6545 . . . . . . . . 9 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → (((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
123122negeqd 10127 . . . . . . . 8 ((𝑓 ∈ (Poly‘ℂ) ∧ 1 = (deg‘𝑓)) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
124123adantrr 749 . . . . . . 7 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → -(((coeff‘𝑓)‘0) / ((coeff‘𝑓)‘1)) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
12551, 117, 1243eqtr3d 2652 . . . . . 6 ((𝑓 ∈ (Poly‘ℂ) ∧ (1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
126125ex 449 . . . . 5 (𝑓 ∈ (Poly‘ℂ) → ((1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
127126rgen 2906 . . . 4 𝑓 ∈ (Poly‘ℂ)((1 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
128 id 22 . . . . . . . . . . 11 (𝑦 = 𝑥𝑦 = 𝑥)
129128cbvsumv 14223 . . . . . . . . . 10 Σ𝑦 ∈ (𝑓 “ {0})𝑦 = Σ𝑥 ∈ (𝑓 “ {0})𝑥
130129eqeq1i 2615 . . . . . . . . 9 𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
131130imbi2i 325 . . . . . . . 8 (((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
132131ralbii 2963 . . . . . . 7 (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
133 eqid 2610 . . . . . . . . 9 (coeff‘𝑔) = (coeff‘𝑔)
134 eqid 2610 . . . . . . . . 9 (deg‘𝑔) = (deg‘𝑔)
135 eqid 2610 . . . . . . . . 9 (𝑔 “ {0}) = (𝑔 “ {0})
136 simp1r 1079 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔))) → 𝑔 ∈ (Poly‘ℂ))
137 simp3r 1083 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔))) → (#‘(𝑔 “ {0})) = (deg‘𝑔))
138 simp1l 1078 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔))) → 𝑑 ∈ ℕ)
139 simp3l 1082 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔))) → (𝑑 + 1) = (deg‘𝑔))
140 simp2 1055 . . . . . . . . . 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‘𝑓)))))
141140, 132sylib 207 . . . . . . . . 9 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (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‘𝑓)))))
142 eqid 2610 . . . . . . . . 9 (𝑔 quot (Xp𝑓 − (ℂ × {𝑧}))) = (𝑔 quot (Xp𝑓 − (ℂ × {𝑧})))
143133, 134, 135, 136, 137, 138, 139, 141, 142vieta1lem2 23815 . . . . . . . 8 (((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) ∧ ∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ∧ ((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔))) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))
1441433exp 1256 . . . . . . 7 ((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑦 ∈ (𝑓 “ {0})𝑦 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → (((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
145132, 144syl5bir 232 . . . . . 6 ((𝑑 ∈ ℕ ∧ 𝑔 ∈ (Poly‘ℂ)) → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → (((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
146145ralrimdva 2952 . . . . 5 (𝑑 ∈ ℕ → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ∀𝑔 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))))))
147 fveq2 6088 . . . . . . . . 9 (𝑔 = 𝑓 → (deg‘𝑔) = (deg‘𝑓))
148147eqeq2d 2620 . . . . . . . 8 (𝑔 = 𝑓 → ((𝑑 + 1) = (deg‘𝑔) ↔ (𝑑 + 1) = (deg‘𝑓)))
149 cnveq 5206 . . . . . . . . . . 11 (𝑔 = 𝑓𝑔 = 𝑓)
150149imaeq1d 5371 . . . . . . . . . 10 (𝑔 = 𝑓 → (𝑔 “ {0}) = (𝑓 “ {0}))
151150fveq2d 6092 . . . . . . . . 9 (𝑔 = 𝑓 → (#‘(𝑔 “ {0})) = (#‘(𝑓 “ {0})))
152151, 147eqeq12d 2625 . . . . . . . 8 (𝑔 = 𝑓 → ((#‘(𝑔 “ {0})) = (deg‘𝑔) ↔ (#‘(𝑓 “ {0})) = (deg‘𝑓)))
153148, 152anbi12d 743 . . . . . . 7 (𝑔 = 𝑓 → (((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔)) ↔ ((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓))))
154150sumeq1d 14228 . . . . . . . 8 (𝑔 = 𝑓 → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = Σ𝑥 ∈ (𝑓 “ {0})𝑥)
155 fveq2 6088 . . . . . . . . . . 11 (𝑔 = 𝑓 → (coeff‘𝑔) = (coeff‘𝑓))
156147oveq1d 6542 . . . . . . . . . . 11 (𝑔 = 𝑓 → ((deg‘𝑔) − 1) = ((deg‘𝑓) − 1))
157155, 156fveq12d 6094 . . . . . . . . . 10 (𝑔 = 𝑓 → ((coeff‘𝑔)‘((deg‘𝑔) − 1)) = ((coeff‘𝑓)‘((deg‘𝑓) − 1)))
158155, 147fveq12d 6094 . . . . . . . . . 10 (𝑔 = 𝑓 → ((coeff‘𝑔)‘(deg‘𝑔)) = ((coeff‘𝑓)‘(deg‘𝑓)))
159157, 158oveq12d 6545 . . . . . . . . 9 (𝑔 = 𝑓 → (((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) = (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
160159negeqd 10127 . . . . . . . 8 (𝑔 = 𝑓 → -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))
161154, 160eqeq12d 2625 . . . . . . 7 (𝑔 = 𝑓 → (Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔))) ↔ Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
162153, 161imbi12d 333 . . . . . 6 (𝑔 = 𝑓 → ((((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔)))) ↔ (((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
163162cbvralv 3147 . . . . 5 (∀𝑔 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑔) ∧ (#‘(𝑔 “ {0})) = (deg‘𝑔)) → Σ𝑥 ∈ (𝑔 “ {0})𝑥 = -(((coeff‘𝑔)‘((deg‘𝑔) − 1)) / ((coeff‘𝑔)‘(deg‘𝑔)))) ↔ ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
164146, 163syl6ib 240 . . . 4 (𝑑 ∈ ℕ → (∀𝑓 ∈ (Poly‘ℂ)((𝑑 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ∀𝑓 ∈ (Poly‘ℂ)(((𝑑 + 1) = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))))))
1658, 12, 16, 20, 127, 164nnind 10888 . . 3 (𝑁 ∈ ℕ → ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
1664, 165syl 17 . 2 (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
167 vieta1.5 . 2 (𝜑 → (#‘𝑅) = 𝑁)
168 fveq2 6088 . . . . . . 7 (𝑓 = 𝐹 → (deg‘𝑓) = (deg‘𝐹))
169168eqeq2d 2620 . . . . . 6 (𝑓 = 𝐹 → (𝑁 = (deg‘𝑓) ↔ 𝑁 = (deg‘𝐹)))
170 cnveq 5206 . . . . . . . . . 10 (𝑓 = 𝐹𝑓 = 𝐹)
171170imaeq1d 5371 . . . . . . . . 9 (𝑓 = 𝐹 → (𝑓 “ {0}) = (𝐹 “ {0}))
172 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
173171, 172syl6eqr 2662 . . . . . . . 8 (𝑓 = 𝐹 → (𝑓 “ {0}) = 𝑅)
174173fveq2d 6092 . . . . . . 7 (𝑓 = 𝐹 → (#‘(𝑓 “ {0})) = (#‘𝑅))
175 vieta1.2 . . . . . . . 8 𝑁 = (deg‘𝐹)
176168, 175syl6eqr 2662 . . . . . . 7 (𝑓 = 𝐹 → (deg‘𝑓) = 𝑁)
177174, 176eqeq12d 2625 . . . . . 6 (𝑓 = 𝐹 → ((#‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (#‘𝑅) = 𝑁))
178169, 177anbi12d 743 . . . . 5 (𝑓 = 𝐹 → ((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝑁 = (deg‘𝐹) ∧ (#‘𝑅) = 𝑁)))
179175biantrur 526 . . . . 5 ((#‘𝑅) = 𝑁 ↔ (𝑁 = (deg‘𝐹) ∧ (#‘𝑅) = 𝑁))
180178, 179syl6bbr 277 . . . 4 (𝑓 = 𝐹 → ((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (#‘𝑅) = 𝑁))
181173sumeq1d 14228 . . . . 5 (𝑓 = 𝐹 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥𝑅 𝑥)
182 fveq2 6088 . . . . . . . . 9 (𝑓 = 𝐹 → (coeff‘𝑓) = (coeff‘𝐹))
183 vieta1.1 . . . . . . . . 9 𝐴 = (coeff‘𝐹)
184182, 183syl6eqr 2662 . . . . . . . 8 (𝑓 = 𝐹 → (coeff‘𝑓) = 𝐴)
185176oveq1d 6542 . . . . . . . 8 (𝑓 = 𝐹 → ((deg‘𝑓) − 1) = (𝑁 − 1))
186184, 185fveq12d 6094 . . . . . . 7 (𝑓 = 𝐹 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = (𝐴‘(𝑁 − 1)))
187184, 176fveq12d 6094 . . . . . . 7 (𝑓 = 𝐹 → ((coeff‘𝑓)‘(deg‘𝑓)) = (𝐴𝑁))
188186, 187oveq12d 6545 . . . . . 6 (𝑓 = 𝐹 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
189188negeqd 10127 . . . . 5 (𝑓 = 𝐹 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
190181, 189eqeq12d 2625 . . . 4 (𝑓 = 𝐹 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁))))
191180, 190imbi12d 333 . . 3 (𝑓 = 𝐹 → (((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((#‘𝑅) = 𝑁 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))))
192191rspcv 3278 . 2 (𝐹 ∈ (Poly‘ℂ) → (∀𝑓 ∈ (Poly‘ℂ)((𝑁 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ((#‘𝑅) = 𝑁 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))))
1933, 166, 167, 192syl3c 64 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wral 2896  wss 3540  {csn 4125   class class class wbr 4578   × cxp 5026  ccnv 5027  cima 5031   Fn wfn 5785  wf 5786  cfv 5790  (class class class)co 6527  𝑓 cof 6771  cen 7816  Fincfn 7819  cc 9791  0cc0 9793  1c1 9794   + caddc 9796   · cmul 9798  cle 9932  cmin 10118  -cneg 10119   / cdiv 10536  cn 10870  0cn0 11142  cz 11213  ...cfz 12155  cexp 12680  #chash 12937  Σcsu 14213  0𝑝c0p 23187  Polycply 23689  Xpcidp 23690  coeffccoe 23691  degcdgr 23692   quot cquot 23794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4694  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-inf2 8399  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870  ax-pre-sup 9871  ax-addf 9872
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-fal 1481  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4368  df-int 4406  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-tr 4676  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-se 4988  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-isom 5799  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-of 6773  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-sup 8209  df-inf 8210  df-oi 8276  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-div 10537  df-nn 10871  df-2 10929  df-3 10930  df-n0 11143  df-z 11214  df-uz 11523  df-rp 11668  df-fz 12156  df-fzo 12293  df-fl 12413  df-seq 12622  df-exp 12681  df-hash 12938  df-cj 13636  df-re 13637  df-im 13638  df-sqrt 13772  df-abs 13773  df-clim 14016  df-rlim 14017  df-sum 14214  df-0p 23188  df-ply 23693  df-idp 23694  df-coe 23695  df-dgr 23696  df-quot 23795
This theorem is referenced by:  basellem5  24556
  Copyright terms: Public domain W3C validator