Metamath Proof Explorer

Theorem vieta1

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

Ref Expression
Hypotheses vieta1.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
vieta1.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
vieta1.3 ⊢ 𝑅 = ( ◡ 𝐹 “ { 0 } )
vieta1.4 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
vieta1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) = 𝑁 )
vieta1.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion vieta1 ( 𝜑 → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 vieta1.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
2 vieta1.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
3 vieta1.3 ⊢ 𝑅 = ( ◡ 𝐹 “ { 0 } )
4 vieta1.4 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
5 vieta1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) = 𝑁 )
6 vieta1.6 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
7 fveq2 ⊢ ( 𝑓 = 𝐹 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝐹 ) )
8 7 eqeq2d ⊢ ( 𝑓 = 𝐹 → ( 𝑁 = ( deg ‘ 𝑓 ) ↔ 𝑁 = ( deg ‘ 𝐹 ) ) )
9 cnveq ⊢ ( 𝑓 = 𝐹 → ◡ 𝑓 = ◡ 𝐹 )
10 9 imaeq1d ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ { 0 } ) = ( ◡ 𝐹 “ { 0 } ) )
11 10 3 eqtr4di ⊢ ( 𝑓 = 𝐹 → ( ◡ 𝑓 “ { 0 } ) = 𝑅 )
12 11 fveq2d ⊢ ( 𝑓 = 𝐹 → ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( ♯ ‘ 𝑅 ) )
13 7 2 eqtr4di ⊢ ( 𝑓 = 𝐹 → ( deg ‘ 𝑓 ) = 𝑁 )
14 12 13 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ↔ ( ♯ ‘ 𝑅 ) = 𝑁 ) )
15 8 14 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( 𝑁 = ( deg ‘ 𝐹 ) ∧ ( ♯ ‘ 𝑅 ) = 𝑁 ) ) )
16 2 biantrur ⊢ ( ( ♯ ‘ 𝑅 ) = 𝑁 ↔ ( 𝑁 = ( deg ‘ 𝐹 ) ∧ ( ♯ ‘ 𝑅 ) = 𝑁 ) )
17 15 16 bitr4di ⊢ ( 𝑓 = 𝐹 → ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( ♯ ‘ 𝑅 ) = 𝑁 ) )
18 11 sumeq1d ⊢ ( 𝑓 = 𝐹 → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = Σ 𝑥 ∈ 𝑅 𝑥 )
19 fveq2 ⊢ ( 𝑓 = 𝐹 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝐹 ) )
20 19 1 eqtr4di ⊢ ( 𝑓 = 𝐹 → ( coeff ‘ 𝑓 ) = 𝐴 )
21 13 oveq1d ⊢ ( 𝑓 = 𝐹 → ( ( deg ‘ 𝑓 ) − 1 ) = ( 𝑁 − 1 ) )
22 20 21 fveq12d ⊢ ( 𝑓 = 𝐹 → ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) = ( 𝐴 ‘ ( 𝑁 − 1 ) ) )
23 20 13 fveq12d ⊢ ( 𝑓 = 𝐹 → ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) = ( 𝐴 ‘ 𝑁 ) )
24 22 23 oveq12d ⊢ ( 𝑓 = 𝐹 → ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) = ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
25 24 negeqd ⊢ ( 𝑓 = 𝐹 → - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
26 18 25 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ↔ Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) )
27 17 26 imbi12d ⊢ ( 𝑓 = 𝐹 → ( ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( ♯ ‘ 𝑅 ) = 𝑁 → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) ) )
28 eqeq1 ⊢ ( 𝑦 = 1 → ( 𝑦 = ( deg ‘ 𝑓 ) ↔ 1 = ( deg ‘ 𝑓 ) ) )
29 28 anbi1d ⊢ ( 𝑦 = 1 → ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) )
30 29 imbi1d ⊢ ( 𝑦 = 1 → ( ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
31 30 ralbidv ⊢ ( 𝑦 = 1 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
32 eqeq1 ⊢ ( 𝑦 = 𝑑 → ( 𝑦 = ( deg ‘ 𝑓 ) ↔ 𝑑 = ( deg ‘ 𝑓 ) ) )
33 32 anbi1d ⊢ ( 𝑦 = 𝑑 → ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) )
34 33 imbi1d ⊢ ( 𝑦 = 𝑑 → ( ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
35 34 ralbidv ⊢ ( 𝑦 = 𝑑 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
36 eqeq1 ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( 𝑦 = ( deg ‘ 𝑓 ) ↔ ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ) )
37 36 anbi1d ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) )
38 37 imbi1d ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
39 38 ralbidv ⊢ ( 𝑦 = ( 𝑑 + 1 ) → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
40 eqeq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 = ( deg ‘ 𝑓 ) ↔ 𝑁 = ( deg ‘ 𝑓 ) ) )
41 40 anbi1d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) )
42 41 imbi1d ⊢ ( 𝑦 = 𝑁 → ( ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
43 42 ralbidv ⊢ ( 𝑦 = 𝑁 → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑦 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
44 eqid ⊢ ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑓 )
45 44 coef3 ⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ )
46 45 adantr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ )
47 0nn0 ⊢ 0 ∈ ℕ0
48 ffvelrn ⊢ ( ( ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ ∧ 0 ∈ ℕ0 ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) ∈ ℂ )
49 46 47 48 sylancl ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) ∈ ℂ )
50 1nn0 ⊢ 1 ∈ ℕ0
51 ffvelrn ⊢ ( ( ( coeff ‘ 𝑓 ) : ℕ0 ⟶ ℂ ∧ 1 ∈ ℕ0 ) → ( ( coeff ‘ 𝑓 ) ‘ 1 ) ∈ ℂ )
52 46 50 51 sylancl ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( coeff ‘ 𝑓 ) ‘ 1 ) ∈ ℂ )
53 simpr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → 1 = ( deg ‘ 𝑓 ) )
54 53 fveq2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( coeff ‘ 𝑓 ) ‘ 1 ) = ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) )
55 ax-1ne0 ⊢ 1 ≠ 0
56 55 a1i ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → 1 ≠ 0 )
57 53 56 eqnetrrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( deg ‘ 𝑓 ) ≠ 0 )
58 fveq2 ⊢ ( 𝑓 = 0𝑝 → ( deg ‘ 𝑓 ) = ( deg ‘ 0𝑝 ) )
59 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
60 58 59 eqtrdi ⊢ ( 𝑓 = 0𝑝 → ( deg ‘ 𝑓 ) = 0 )
61 60 necon3i ⊢ ( ( deg ‘ 𝑓 ) ≠ 0 → 𝑓 ≠ 0𝑝 )
62 57 61 syl ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → 𝑓 ≠ 0𝑝 )
63 eqid ⊢ ( deg ‘ 𝑓 ) = ( deg ‘ 𝑓 )
64 63 44 dgreq0 ⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( 𝑓 = 0𝑝 ↔ ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) = 0 ) )
65 64 necon3bid ⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( 𝑓 ≠ 0𝑝 ↔ ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ≠ 0 ) )
66 65 adantr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 𝑓 ≠ 0𝑝 ↔ ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ≠ 0 ) )
67 62 66 mpbid ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ≠ 0 )
68 54 67 eqnetrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( coeff ‘ 𝑓 ) ‘ 1 ) ≠ 0 )
69 49 52 68 divcld ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ )
70 69 negcld ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ )
71 id ⊢ ( 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) → 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) )
72 71 sumsn ⊢ ( ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ ∧ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ ) → Σ 𝑥 ∈ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) )
73 70 70 72 syl2anc ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) )
74 73 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → Σ 𝑥 ∈ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) )
75 eqid ⊢ ( ◡ 𝑓 “ { 0 } ) = ( ◡ 𝑓 “ { 0 } )
76 75 fta1 ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 𝑓 ≠ 0𝑝 ) → ( ( ◡ 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) )
77 62 76 syldan ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ◡ 𝑓 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) ≤ ( deg ‘ 𝑓 ) ) )
78 77 simpld ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ◡ 𝑓 “ { 0 } ) ∈ Fin )
79 78 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → ( ◡ 𝑓 “ { 0 } ) ∈ Fin )
80 44 63 coeid2 ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ ) → ( 𝑓 ‘ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) )
81 70 80 syldan ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 𝑓 ‘ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) )
82 53 oveq2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 0 ... 1 ) = ( 0 ... ( deg ‘ 𝑓 ) ) )
83 82 sumeq1d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... ( deg ‘ 𝑓 ) ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) )
84 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
85 1e0p1 ⊢ 1 = ( 0 + 1 )
86 fveq2 ⊢ ( 𝑘 = 1 → ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) = ( ( coeff ‘ 𝑓 ) ‘ 1 ) )
87 oveq2 ⊢ ( 𝑘 = 1 → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) = ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) )
88 86 87 oveq12d ⊢ ( 𝑘 = 1 → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) ) )
89 46 ffvelrnda ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) ∈ ℂ )
90 expcl ⊢ ( ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ∈ ℂ )
91 70 90 sylan ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ∈ ℂ )
92 89 91 mulcld ⊢ ( ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) ∈ ℂ )
93 0z ⊢ 0 ∈ ℤ
94 70 exp0d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) = 1 )
95 94 oveq2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · 1 ) )
96 49 mulid1d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · 1 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
97 95 96 eqtrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
98 97 49 eqeltrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) ∈ ℂ )
99 fveq2 ⊢ ( 𝑘 = 0 → ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
100 oveq2 ⊢ ( 𝑘 = 0 → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) = ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) )
101 99 100 oveq12d ⊢ ( 𝑘 = 0 → ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) )
102 101 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) )
103 93 98 102 sylancr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 0 ) ) )
104 103 97 eqtrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
105 104 47 jctil ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 0 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) ) )
106 70 exp1d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) = - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) )
107 106 oveq2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) )
108 52 69 mulneg2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = - ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) )
109 49 52 68 divcan2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
110 109 negeqd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → - ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = - ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
111 107 108 110 3eqtrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) ) = - ( ( coeff ‘ 𝑓 ) ‘ 0 ) )
112 111 oveq2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) + ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) + - ( ( coeff ‘ 𝑓 ) ‘ 0 ) ) )
113 49 negidd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) + - ( ( coeff ‘ 𝑓 ) ‘ 0 ) ) = 0 )
114 112 113 eqtrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) + ( ( ( coeff ‘ 𝑓 ) ‘ 1 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 1 ) ) ) = 0 )
115 84 85 88 92 105 114 fsump1i ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 1 ∈ ℕ0 ∧ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = 0 ) )
116 115 simprd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( ( coeff ‘ 𝑓 ) ‘ 𝑘 ) · ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ↑ 𝑘 ) ) = 0 )
117 81 83 116 3eqtr2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 𝑓 ‘ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = 0 )
118 plyf ⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → 𝑓 : ℂ ⟶ ℂ )
119 118 ffnd ⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → 𝑓 Fn ℂ )
120 119 adantr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → 𝑓 Fn ℂ )
121 fniniseg ⊢ ( 𝑓 Fn ℂ → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ( ◡ 𝑓 “ { 0 } ) ↔ ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ ∧ ( 𝑓 ‘ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = 0 ) ) )
122 120 121 syl ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ( ◡ 𝑓 “ { 0 } ) ↔ ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ ∧ ( 𝑓 ‘ - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ) = 0 ) ) )
123 70 117 122 mpbir2and ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ( ◡ 𝑓 “ { 0 } ) )
124 123 snssd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ⊆ ( ◡ 𝑓 “ { 0 } ) )
125 124 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ⊆ ( ◡ 𝑓 “ { 0 } ) )
126 hashsng ⊢ ( - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) ∈ ℂ → ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = 1 )
127 70 126 syl ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = 1 )
128 127 53 eqtrd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = ( deg ‘ 𝑓 ) )
129 128 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = ( deg ‘ 𝑓 ) )
130 simprr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) )
131 129 130 eqtr4d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) )
132 snfi ⊢ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ∈ Fin
133 hashen ⊢ ( ( { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ∈ Fin ∧ ( ◡ 𝑓 “ { 0 } ) ∈ Fin ) → ( ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) ↔ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ≈ ( ◡ 𝑓 “ { 0 } ) ) )
134 132 78 133 sylancr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) ↔ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ≈ ( ◡ 𝑓 “ { 0 } ) ) )
135 134 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → ( ( ♯ ‘ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ) = ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) ↔ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ≈ ( ◡ 𝑓 “ { 0 } ) ) )
136 131 135 mpbid ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ≈ ( ◡ 𝑓 “ { 0 } ) )
137 fisseneq ⊢ ( ( ( ◡ 𝑓 “ { 0 } ) ∈ Fin ∧ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ⊆ ( ◡ 𝑓 “ { 0 } ) ∧ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } ≈ ( ◡ 𝑓 “ { 0 } ) ) → { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } = ( ◡ 𝑓 “ { 0 } ) )
138 79 125 136 137 syl3anc ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } = ( ◡ 𝑓 “ { 0 } ) )
139 138 sumeq1d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → Σ 𝑥 ∈ { - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) } 𝑥 = Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 )
140 1m1e0 ⊢ ( 1 − 1 ) = 0
141 53 oveq1d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( 1 − 1 ) = ( ( deg ‘ 𝑓 ) − 1 ) )
142 140 141 eqtr3id ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → 0 = ( ( deg ‘ 𝑓 ) − 1 ) )
143 142 fveq2d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( coeff ‘ 𝑓 ) ‘ 0 ) = ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) )
144 143 54 oveq12d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
145 144 negeqd ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ 1 = ( deg ‘ 𝑓 ) ) → - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
146 145 adantrr ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → - ( ( ( coeff ‘ 𝑓 ) ‘ 0 ) / ( ( coeff ‘ 𝑓 ) ‘ 1 ) ) = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
147 74 139 146 3eqtr3d ⊢ ( ( 𝑓 ∈ ( Poly ‘ ℂ ) ∧ ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
148 147 ex ⊢ ( 𝑓 ∈ ( Poly ‘ ℂ ) → ( ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
149 148 rgen ⊢ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 1 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
150 id ⊢ ( 𝑦 = 𝑥 → 𝑦 = 𝑥 )
151 150 cbvsumv ⊢ Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥
152 151 eqeq1i ⊢ ( Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ↔ Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
153 152 imbi2i ⊢ ( ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
154 153 ralbii ⊢ ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
155 eqid ⊢ ( coeff ‘ 𝑔 ) = ( coeff ‘ 𝑔 )
156 eqid ⊢ ( deg ‘ 𝑔 ) = ( deg ‘ 𝑔 )
157 eqid ⊢ ( ◡ 𝑔 “ { 0 } ) = ( ◡ 𝑔 “ { 0 } )
158 simp1r ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ∧ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) ) → 𝑔 ∈ ( Poly ‘ ℂ ) )
159 simp3r ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ∧ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) ) → ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) )
160 simp1l ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ∧ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) ) → 𝑑 ∈ ℕ )
161 simp3l ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ∧ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) ) → ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) )
162 simp2 ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( 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 162 154 sylib ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( 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 ‘ 𝑓 ) ) ) ) )
164 eqid ⊢ ( 𝑔 quot ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = ( 𝑔 quot ( Xp ∘f − ( ℂ × { 𝑧 } ) ) )
165 155 156 157 158 159 160 161 163 164 vieta1lem2 ⊢ ( ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) ∧ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ∧ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) ) → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) )
166 165 3exp ⊢ ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑦 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑦 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) → ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) ) ) )
167 154 166 syl5bir ⊢ ( ( 𝑑 ∈ ℕ ∧ 𝑔 ∈ ( Poly ‘ ℂ ) ) → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) → ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) ) ) )
168 167 ralrimdva ⊢ ( 𝑑 ∈ ℕ → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) → ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) ) ) )
169 fveq2 ⊢ ( 𝑔 = 𝑓 → ( deg ‘ 𝑔 ) = ( deg ‘ 𝑓 ) )
170 169 eqeq2d ⊢ ( 𝑔 = 𝑓 → ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ↔ ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ) )
171 cnveq ⊢ ( 𝑔 = 𝑓 → ◡ 𝑔 = ◡ 𝑓 )
172 171 imaeq1d ⊢ ( 𝑔 = 𝑓 → ( ◡ 𝑔 “ { 0 } ) = ( ◡ 𝑓 “ { 0 } ) )
173 172 fveq2d ⊢ ( 𝑔 = 𝑓 → ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) )
174 173 169 eqeq12d ⊢ ( 𝑔 = 𝑓 → ( ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ↔ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) )
175 170 174 anbi12d ⊢ ( 𝑔 = 𝑓 → ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) ↔ ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ) )
176 172 sumeq1d ⊢ ( 𝑔 = 𝑓 → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 )
177 fveq2 ⊢ ( 𝑔 = 𝑓 → ( coeff ‘ 𝑔 ) = ( coeff ‘ 𝑓 ) )
178 169 oveq1d ⊢ ( 𝑔 = 𝑓 → ( ( deg ‘ 𝑔 ) − 1 ) = ( ( deg ‘ 𝑓 ) − 1 ) )
179 177 178 fveq12d ⊢ ( 𝑔 = 𝑓 → ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) = ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) )
180 177 169 fveq12d ⊢ ( 𝑔 = 𝑓 → ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) = ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) )
181 179 180 oveq12d ⊢ ( 𝑔 = 𝑓 → ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) = ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
182 181 negeqd ⊢ ( 𝑔 = 𝑓 → - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) )
183 176 182 eqeq12d ⊢ ( 𝑔 = 𝑓 → ( Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) ↔ Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
184 175 183 imbi12d ⊢ ( 𝑔 = 𝑓 → ( ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) ) ↔ ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
185 184 cbvralvw ⊢ ( ∀ 𝑔 ∈ ( Poly ‘ ℂ ) ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑔 ) ∧ ( ♯ ‘ ( ◡ 𝑔 “ { 0 } ) ) = ( deg ‘ 𝑔 ) ) → Σ 𝑥 ∈ ( ◡ 𝑔 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑔 ) ‘ ( ( deg ‘ 𝑔 ) − 1 ) ) / ( ( coeff ‘ 𝑔 ) ‘ ( deg ‘ 𝑔 ) ) ) ) ↔ ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
186 168 185 syl6ib ⊢ ( 𝑑 ∈ ℕ → ( ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑑 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( ( 𝑑 + 1 ) = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ) )
187 31 35 39 43 149 186 nnind ⊢ ( 𝑁 ∈ ℕ → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
188 6 187 syl ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝑁 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
189 plyssc ⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
190 189 4 sselid ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ ℂ ) )
191 27 188 190 rspcdva ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) = 𝑁 → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) )
192 5 191 mpd ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )