Metamath Proof Explorer

Theorem vieta1lem1

Description: Lemma for vieta1 . (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
vieta1lem.6 ⊢ φ → D ∈ ℕ
vieta1lem.7 ⊢ φ → D + 1 = N
vieta1lem.8 ⊢ φ → ∀ f ∈ Poly ⁡ ℂ D = deg ⁡ f ∧ f -1 0 = deg ⁡ f → ∑ x ∈ f -1 0 x = − coeff ⁡ f ⁡ deg ⁡ f − 1 coeff ⁡ f ⁡ deg ⁡ f
vieta1lem.9 ⊢ Q = F quot X p − f ℂ × z
Assertion vieta1lem1 ⊢ φ ∧ z ∈ R → Q ∈ Poly ⁡ ℂ ∧ D = deg ⁡ Q

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 vieta1lem.6 ⊢ φ → D ∈ ℕ
7 vieta1lem.7 ⊢ φ → D + 1 = N
8 vieta1lem.8 ⊢ φ → ∀ f ∈ Poly ⁡ ℂ D = deg ⁡ f ∧ f -1 0 = deg ⁡ f → ∑ x ∈ f -1 0 x = − coeff ⁡ f ⁡ deg ⁡ f − 1 coeff ⁡ f ⁡ deg ⁡ f
9 vieta1lem.9 ⊢ Q = F quot X p − f ℂ × z
10 plyssc ⊢ Poly ⁡ S ⊆ Poly ⁡ ℂ
11 4 adantr ⊢ φ ∧ z ∈ R → F ∈ Poly ⁡ S
12 10 11 sseldi ⊢ φ ∧ z ∈ R → F ∈ Poly ⁡ ℂ
13 cnvimass ⊢ F -1 0 ⊆ dom ⁡ F
14 3 13 eqsstri ⊢ R ⊆ dom ⁡ F
15 plyf ⊢ F ∈ Poly ⁡ S → F : ℂ ⟶ ℂ
16 4 15 syl ⊢ φ → F : ℂ ⟶ ℂ
17 14 16 fssdm ⊢ φ → R ⊆ ℂ
18 17 sselda ⊢ φ ∧ z ∈ R → z ∈ ℂ
19 eqid ⊢ X p − f ℂ × z = X p − f ℂ × z
20 19 plyremlem ⊢ z ∈ ℂ → X p − f ℂ × z ∈ Poly ⁡ ℂ ∧ deg ⁡ X p − f ℂ × z = 1 ∧ X p − f ℂ × z -1 0 = z
21 18 20 syl ⊢ φ ∧ z ∈ R → X p − f ℂ × z ∈ Poly ⁡ ℂ ∧ deg ⁡ X p − f ℂ × z = 1 ∧ X p − f ℂ × z -1 0 = z
22 21 simp1d ⊢ φ ∧ z ∈ R → X p − f ℂ × z ∈ Poly ⁡ ℂ
23 21 simp2d ⊢ φ ∧ z ∈ R → deg ⁡ X p − f ℂ × z = 1
24 ax-1ne0 ⊢ 1 ≠ 0
25 24 a1i ⊢ φ ∧ z ∈ R → 1 ≠ 0
26 23 25 eqnetrd ⊢ φ ∧ z ∈ R → deg ⁡ X p − f ℂ × z ≠ 0
27 fveq2 ⊢ X p − f ℂ × z = 0 𝑝 → deg ⁡ X p − f ℂ × z = deg ⁡ 0 𝑝
28 dgr0 ⊢ deg ⁡ 0 𝑝 = 0
29 27 28 eqtrdi ⊢ X p − f ℂ × z = 0 𝑝 → deg ⁡ X p − f ℂ × z = 0
30 29 necon3i ⊢ deg ⁡ X p − f ℂ × z ≠ 0 → X p − f ℂ × z ≠ 0 𝑝
31 26 30 syl ⊢ φ ∧ z ∈ R → X p − f ℂ × z ≠ 0 𝑝
32 quotcl2 ⊢ F ∈ Poly ⁡ ℂ ∧ X p − f ℂ × z ∈ Poly ⁡ ℂ ∧ X p − f ℂ × z ≠ 0 𝑝 → F quot X p − f ℂ × z ∈ Poly ⁡ ℂ
33 12 22 31 32 syl3anc ⊢ φ ∧ z ∈ R → F quot X p − f ℂ × z ∈ Poly ⁡ ℂ
34 9 33 eqeltrid ⊢ φ ∧ z ∈ R → Q ∈ Poly ⁡ ℂ
35 1cnd ⊢ φ ∧ z ∈ R → 1 ∈ ℂ
36 6 nncnd ⊢ φ → D ∈ ℂ
37 36 adantr ⊢ φ ∧ z ∈ R → D ∈ ℂ
38 dgrcl ⊢ Q ∈ Poly ⁡ ℂ → deg ⁡ Q ∈ ℕ 0
39 34 38 syl ⊢ φ ∧ z ∈ R → deg ⁡ Q ∈ ℕ 0
40 39 nn0cnd ⊢ φ ∧ z ∈ R → deg ⁡ Q ∈ ℂ
41 ax-1cn ⊢ 1 ∈ ℂ
42 addcom ⊢ 1 ∈ ℂ ∧ D ∈ ℂ → 1 + D = D + 1
43 41 37 42 sylancr ⊢ φ ∧ z ∈ R → 1 + D = D + 1
44 7 2 eqtrdi ⊢ φ → D + 1 = deg ⁡ F
45 44 adantr ⊢ φ ∧ z ∈ R → D + 1 = deg ⁡ F
46 3 eleq2i ⊢ z ∈ R ↔ z ∈ F -1 0
47 16 ffnd ⊢ φ → F Fn ℂ
48 fniniseg ⊢ F Fn ℂ → z ∈ F -1 0 ↔ z ∈ ℂ ∧ F ⁡ z = 0
49 47 48 syl ⊢ φ → z ∈ F -1 0 ↔ z ∈ ℂ ∧ F ⁡ z = 0
50 46 49 syl5bb ⊢ φ → z ∈ R ↔ z ∈ ℂ ∧ F ⁡ z = 0
51 50 simplbda ⊢ φ ∧ z ∈ R → F ⁡ z = 0
52 19 facth ⊢ F ∈ Poly ⁡ S ∧ z ∈ ℂ ∧ F ⁡ z = 0 → F = X p − f ℂ × z × f F quot X p − f ℂ × z
53 11 18 51 52 syl3anc ⊢ φ ∧ z ∈ R → F = X p − f ℂ × z × f F quot X p − f ℂ × z
54 9 oveq2i ⊢ X p − f ℂ × z × f Q = X p − f ℂ × z × f F quot X p − f ℂ × z
55 53 54 eqtr4di ⊢ φ ∧ z ∈ R → F = X p − f ℂ × z × f Q
56 55 fveq2d ⊢ φ ∧ z ∈ R → deg ⁡ F = deg ⁡ X p − f ℂ × z × f Q
57 6 peano2nnd ⊢ φ → D + 1 ∈ ℕ
58 7 57 eqeltrrd ⊢ φ → N ∈ ℕ
59 58 nnne0d ⊢ φ → N ≠ 0
60 2 59 eqnetrrid ⊢ φ → deg ⁡ F ≠ 0
61 fveq2 ⊢ F = 0 𝑝 → deg ⁡ F = deg ⁡ 0 𝑝
62 61 28 eqtrdi ⊢ F = 0 𝑝 → deg ⁡ F = 0
63 62 necon3i ⊢ deg ⁡ F ≠ 0 → F ≠ 0 𝑝
64 60 63 syl ⊢ φ → F ≠ 0 𝑝
65 64 adantr ⊢ φ ∧ z ∈ R → F ≠ 0 𝑝
66 55 65 eqnetrrd ⊢ φ ∧ z ∈ R → X p − f ℂ × z × f Q ≠ 0 𝑝
67 plymul0or ⊢ X p − f ℂ × z ∈ Poly ⁡ ℂ ∧ Q ∈ Poly ⁡ ℂ → X p − f ℂ × z × f Q = 0 𝑝 ↔ X p − f ℂ × z = 0 𝑝 ∨ Q = 0 𝑝
68 22 34 67 syl2anc ⊢ φ ∧ z ∈ R → X p − f ℂ × z × f Q = 0 𝑝 ↔ X p − f ℂ × z = 0 𝑝 ∨ Q = 0 𝑝
69 68 necon3abid ⊢ φ ∧ z ∈ R → X p − f ℂ × z × f Q ≠ 0 𝑝 ↔ ¬ X p − f ℂ × z = 0 𝑝 ∨ Q = 0 𝑝
70 66 69 mpbid ⊢ φ ∧ z ∈ R → ¬ X p − f ℂ × z = 0 𝑝 ∨ Q = 0 𝑝
71 neanior ⊢ X p − f ℂ × z ≠ 0 𝑝 ∧ Q ≠ 0 𝑝 ↔ ¬ X p − f ℂ × z = 0 𝑝 ∨ Q = 0 𝑝
72 70 71 sylibr ⊢ φ ∧ z ∈ R → X p − f ℂ × z ≠ 0 𝑝 ∧ Q ≠ 0 𝑝
73 72 simprd ⊢ φ ∧ z ∈ R → Q ≠ 0 𝑝
74 eqid ⊢ deg ⁡ X p − f ℂ × z = deg ⁡ X p − f ℂ × z
75 eqid ⊢ deg ⁡ Q = deg ⁡ Q
76 74 75 dgrmul ⊢ X p − f ℂ × z ∈ Poly ⁡ ℂ ∧ X p − f ℂ × z ≠ 0 𝑝 ∧ Q ∈ Poly ⁡ ℂ ∧ Q ≠ 0 𝑝 → deg ⁡ X p − f ℂ × z × f Q = deg ⁡ X p − f ℂ × z + deg ⁡ Q
77 22 31 34 73 76 syl22anc ⊢ φ ∧ z ∈ R → deg ⁡ X p − f ℂ × z × f Q = deg ⁡ X p − f ℂ × z + deg ⁡ Q
78 45 56 77 3eqtrd ⊢ φ ∧ z ∈ R → D + 1 = deg ⁡ X p − f ℂ × z + deg ⁡ Q
79 23 oveq1d ⊢ φ ∧ z ∈ R → deg ⁡ X p − f ℂ × z + deg ⁡ Q = 1 + deg ⁡ Q
80 43 78 79 3eqtrd ⊢ φ ∧ z ∈ R → 1 + D = 1 + deg ⁡ Q
81 35 37 40 80 addcanad ⊢ φ ∧ z ∈ R → D = deg ⁡ Q
82 34 81 jca ⊢ φ ∧ z ∈ R → Q ∈ Poly ⁡ ℂ ∧ D = deg ⁡ Q