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 ⊢ A = coeff ⁡ F
vieta1.2 ⊢ N = deg ⁡ F
vieta1.3 ⊢ R = F -1 0
vieta1.4 ⊢ φ → F ∈ Poly ⁡ S
vieta1.5 ⊢ φ → R = N
vieta1.6 ⊢ φ → N ∈ ℕ
Assertion vieta1 ⊢ φ → ∑ x ∈ R x = − A ⁡ N − 1 A ⁡ N

Proof

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