Metamath Proof Explorer

Theorem vieta1lem1

Description: Lemma for vieta1 . (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses vieta1.1 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
vieta1.2 ⊢ 𝑁 = ( deg ‘ 𝐹 )
vieta1.3 ⊢ 𝑅 = ( ◡ 𝐹 “ { 0 } )
vieta1.4 ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
vieta1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) = 𝑁 )
vieta1lem.6 ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
vieta1lem.7 ⊢ ( 𝜑 → ( 𝐷 + 1 ) = 𝑁 )
vieta1lem.8 ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝐷 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
vieta1lem.9 ⊢ 𝑄 = ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝑧 } ) ) )
Assertion vieta1lem1 ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑄 ∈ ( Poly ‘ ℂ ) ∧ 𝐷 = ( deg ‘ 𝑄 ) ) )

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