Metamath Proof Explorer

Theorem vieta1lem2

Description: Lemma for vieta1 : inductive step. Let z be a root of F . Then F = ( Xp - z ) x. Q for some Q by the factor theorem, and Q is a degree- D polynomial, so by the induction hypothesis sum_ x e. (`' Q " 0 ) x = -u ( coeff `Q )( D - 1 ) / ( coeffQ )D , so sum_ x e. R x = z - ( coeffQ )` ` ( D - 1 ) / ( coeffQ )D . Now the coefficients of F are A( D + 1 ) = ( coeffQ )D and AD = sum_ k e. ( 0 ... D ) ( coeffXp - z )k x. ( coeffQ ) ` `( D - k ) , which works out to -u z x. ( coeffQ )D + ( coeffQ )( D - 1 ) , so putting it all together we have sum_ x e. R x = -u AD / A( D + 1 ) as we wanted to show. (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 vieta1lem2 ( 𝜑 → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 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 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 6 peano2nnd ⊢ ( 𝜑 → ( 𝐷 + 1 ) ∈ ℕ )
11 7 10 eqeltrrd ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
12 11 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
13 5 12 eqnetrd ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) ≠ 0 )
14 2 12 eqnetrrid ⊢ ( 𝜑 → ( deg ‘ 𝐹 ) ≠ 0 )
15 fveq2 ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
16 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
17 15 16 eqtrdi ⊢ ( 𝐹 = 0𝑝 → ( deg ‘ 𝐹 ) = 0 )
18 17 necon3i ⊢ ( ( deg ‘ 𝐹 ) ≠ 0 → 𝐹 ≠ 0𝑝 )
19 14 18 syl ⊢ ( 𝜑 → 𝐹 ≠ 0𝑝 )
20 3 fta1 ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐹 ≠ 0𝑝 ) → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )
21 4 19 20 syl2anc ⊢ ( 𝜑 → ( 𝑅 ∈ Fin ∧ ( ♯ ‘ 𝑅 ) ≤ ( deg ‘ 𝐹 ) ) )
22 21 simpld ⊢ ( 𝜑 → 𝑅 ∈ Fin )
23 hasheq0 ⊢ ( 𝑅 ∈ Fin → ( ( ♯ ‘ 𝑅 ) = 0 ↔ 𝑅 = ∅ ) )
24 22 23 syl ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) = 0 ↔ 𝑅 = ∅ ) )
25 24 necon3bid ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑅 ) ≠ 0 ↔ 𝑅 ≠ ∅ ) )
26 13 25 mpbid ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
27 n0 ⊢ ( 𝑅 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝑅 )
28 26 27 sylib ⊢ ( 𝜑 → ∃ 𝑧 𝑧 ∈ 𝑅 )
29 incom ⊢ ( { 𝑧 } ∩ ( ◡ 𝑄 “ { 0 } ) ) = ( ( ◡ 𝑄 “ { 0 } ) ∩ { 𝑧 } )
30 1 2 3 4 5 6 7 8 9 vieta1lem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑄 ∈ ( Poly ‘ ℂ ) ∧ 𝐷 = ( deg ‘ 𝑄 ) ) )
31 30 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐷 = ( deg ‘ 𝑄 ) )
32 30 simpld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑄 ∈ ( Poly ‘ ℂ ) )
33 dgrcl ⊢ ( 𝑄 ∈ ( Poly ‘ ℂ ) → ( deg ‘ 𝑄 ) ∈ ℕ0 )
34 32 33 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ 𝑄 ) ∈ ℕ0 )
35 34 nn0red ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ 𝑄 ) ∈ ℝ )
36 31 35 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐷 ∈ ℝ )
37 36 ltp1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐷 < ( 𝐷 + 1 ) )
38 36 37 gtned ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐷 + 1 ) ≠ 𝐷 )
39 snssi ⊢ ( 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) → { 𝑧 } ⊆ ( ◡ 𝑄 “ { 0 } ) )
40 ssequn1 ⊢ ( { 𝑧 } ⊆ ( ◡ 𝑄 “ { 0 } ) ↔ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) = ( ◡ 𝑄 “ { 0 } ) )
41 39 40 sylib ⊢ ( 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) → ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) = ( ◡ 𝑄 “ { 0 } ) )
42 41 fveq2d ⊢ ( 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) → ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) = ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) )
43 4 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
44 cnvimass ⊢ ( ◡ 𝐹 “ { 0 } ) ⊆ dom 𝐹
45 3 44 eqsstri ⊢ 𝑅 ⊆ dom 𝐹
46 plyf ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
47 fdm ⊢ ( 𝐹 : ℂ ⟶ ℂ → dom 𝐹 = ℂ )
48 4 46 47 3syl ⊢ ( 𝜑 → dom 𝐹 = ℂ )
49 45 48 sseqtrid ⊢ ( 𝜑 → 𝑅 ⊆ ℂ )
50 49 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑧 ∈ ℂ )
51 3 eleq2i ⊢ ( 𝑧 ∈ 𝑅 ↔ 𝑧 ∈ ( ◡ 𝐹 “ { 0 } ) )
52 ffn ⊢ ( 𝐹 : ℂ ⟶ ℂ → 𝐹 Fn ℂ )
53 fniniseg ⊢ ( 𝐹 Fn ℂ → ( 𝑧 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) ) )
54 4 46 52 53 4syl ⊢ ( 𝜑 → ( 𝑧 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) ) )
55 51 54 bitrid ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑅 ↔ ( 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) ) )
56 55 simplbda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑧 ) = 0 )
57 eqid ⊢ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = ( Xp ∘f − ( ℂ × { 𝑧 } ) )
58 57 facth ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑧 ∈ ℂ ∧ ( 𝐹 ‘ 𝑧 ) = 0 ) → 𝐹 = ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) )
59 43 50 56 58 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐹 = ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) )
60 9 oveq2i ⊢ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) = ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · ( 𝐹 quot ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) )
61 59 60 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐹 = ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) )
62 61 cnveqd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ◡ 𝐹 = ◡ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) )
63 62 imaeq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ◡ 𝐹 “ { 0 } ) = ( ◡ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) “ { 0 } ) )
64 3 63 eqtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑅 = ( ◡ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) “ { 0 } ) )
65 cnex ⊢ ℂ ∈ V
66 57 plyremlem ⊢ ( 𝑧 ∈ ℂ → ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) “ { 0 } ) = { 𝑧 } ) )
67 50 66 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = 1 ∧ ( ◡ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) “ { 0 } ) = { 𝑧 } ) )
68 67 simp1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) )
69 plyf ⊢ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) → ( Xp ∘f − ( ℂ × { 𝑧 } ) ) : ℂ ⟶ ℂ )
70 68 69 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( Xp ∘f − ( ℂ × { 𝑧 } ) ) : ℂ ⟶ ℂ )
71 plyf ⊢ ( 𝑄 ∈ ( Poly ‘ ℂ ) → 𝑄 : ℂ ⟶ ℂ )
72 32 71 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑄 : ℂ ⟶ ℂ )
73 ofmulrt ⊢ ( ( ℂ ∈ V ∧ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) : ℂ ⟶ ℂ ∧ 𝑄 : ℂ ⟶ ℂ ) → ( ◡ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) “ { 0 } ) = ( ( ◡ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) “ { 0 } ) ∪ ( ◡ 𝑄 “ { 0 } ) ) )
74 65 70 72 73 mp3an2i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ◡ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) “ { 0 } ) = ( ( ◡ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) “ { 0 } ) ∪ ( ◡ 𝑄 “ { 0 } ) ) )
75 67 simp3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ◡ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) “ { 0 } ) = { 𝑧 } )
76 75 uneq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ◡ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) “ { 0 } ) ∪ ( ◡ 𝑄 “ { 0 } ) ) = ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) )
77 64 74 76 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑅 = ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) )
78 77 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ 𝑅 ) = ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) )
79 5 7 eqtr4d ⊢ ( 𝜑 → ( ♯ ‘ 𝑅 ) = ( 𝐷 + 1 ) )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ 𝑅 ) = ( 𝐷 + 1 ) )
81 78 80 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) = ( 𝐷 + 1 ) )
82 19 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐹 ≠ 0𝑝 )
83 61 82 eqnetrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ≠ 0𝑝 )
84 plymul0or ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ 𝑄 ∈ ( Poly ‘ ℂ ) ) → ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) = 0𝑝 ↔ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 ∨ 𝑄 = 0𝑝 ) ) )
85 68 32 84 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) = 0𝑝 ↔ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 ∨ 𝑄 = 0𝑝 ) ) )
86 85 necon3abid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ≠ 0𝑝 ↔ ¬ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 ∨ 𝑄 = 0𝑝 ) ) )
87 83 86 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ¬ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 ∨ 𝑄 = 0𝑝 ) )
88 neanior ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝 ) ↔ ¬ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 ∨ 𝑄 = 0𝑝 ) )
89 87 88 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ≠ 0𝑝 ∧ 𝑄 ≠ 0𝑝 ) )
90 89 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑄 ≠ 0𝑝 )
91 eqid ⊢ ( ◡ 𝑄 “ { 0 } ) = ( ◡ 𝑄 “ { 0 } )
92 91 fta1 ⊢ ( ( 𝑄 ∈ ( Poly ‘ ℂ ) ∧ 𝑄 ≠ 0𝑝 ) → ( ( ◡ 𝑄 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ≤ ( deg ‘ 𝑄 ) ) )
93 32 90 92 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ◡ 𝑄 “ { 0 } ) ∈ Fin ∧ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ≤ ( deg ‘ 𝑄 ) ) )
94 93 simprd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ≤ ( deg ‘ 𝑄 ) )
95 94 31 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ≤ 𝐷 )
96 snfi ⊢ { 𝑧 } ∈ Fin
97 93 simpld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ◡ 𝑄 “ { 0 } ) ∈ Fin )
98 hashun2 ⊢ ( ( { 𝑧 } ∈ Fin ∧ ( ◡ 𝑄 “ { 0 } ) ∈ Fin ) → ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) ≤ ( ( ♯ ‘ { 𝑧 } ) + ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) )
99 96 97 98 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) ≤ ( ( ♯ ‘ { 𝑧 } ) + ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) )
100 ax-1cn ⊢ 1 ∈ ℂ
101 6 nncnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐷 ∈ ℂ )
103 addcom ⊢ ( ( 1 ∈ ℂ ∧ 𝐷 ∈ ℂ ) → ( 1 + 𝐷 ) = ( 𝐷 + 1 ) )
104 100 102 103 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 1 + 𝐷 ) = ( 𝐷 + 1 ) )
105 81 104 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) = ( 1 + 𝐷 ) )
106 hashsng ⊢ ( 𝑧 ∈ 𝑅 → ( ♯ ‘ { 𝑧 } ) = 1 )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ { 𝑧 } ) = 1 )
108 107 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ♯ ‘ { 𝑧 } ) + ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) = ( 1 + ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) )
109 99 105 108 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 1 + 𝐷 ) ≤ ( 1 + ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) )
110 hashcl ⊢ ( ( ◡ 𝑄 “ { 0 } ) ∈ Fin → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ∈ ℕ0 )
111 97 110 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ∈ ℕ0 )
112 111 nn0red ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ∈ ℝ )
113 1red ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 1 ∈ ℝ )
114 36 112 113 leadd2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐷 ≤ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ↔ ( 1 + 𝐷 ) ≤ ( 1 + ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) ) )
115 109 114 mpbird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐷 ≤ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) )
116 112 36 letri3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = 𝐷 ↔ ( ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ≤ 𝐷 ∧ 𝐷 ≤ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ) ) )
117 95 115 116 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = 𝐷 )
118 81 117 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ♯ ‘ ( { 𝑧 } ∪ ( ◡ 𝑄 “ { 0 } ) ) ) = ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) ↔ ( 𝐷 + 1 ) = 𝐷 ) )
119 42 118 imbitrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) → ( 𝐷 + 1 ) = 𝐷 ) )
120 119 necon3ad ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( 𝐷 + 1 ) ≠ 𝐷 → ¬ 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) ) )
121 38 120 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ¬ 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) )
122 disjsn ⊢ ( ( ( ◡ 𝑄 “ { 0 } ) ∩ { 𝑧 } ) = ∅ ↔ ¬ 𝑧 ∈ ( ◡ 𝑄 “ { 0 } ) )
123 121 122 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ◡ 𝑄 “ { 0 } ) ∩ { 𝑧 } ) = ∅ )
124 29 123 eqtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( { 𝑧 } ∩ ( ◡ 𝑄 “ { 0 } ) ) = ∅ )
125 22 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑅 ∈ Fin )
126 49 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑅 ⊆ ℂ )
127 126 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑥 ∈ 𝑅 ) → 𝑥 ∈ ℂ )
128 124 77 125 127 fsumsplit ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑥 ∈ 𝑅 𝑥 = ( Σ 𝑥 ∈ { 𝑧 } 𝑥 + Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 ) )
129 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
130 129 sumsn ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → Σ 𝑥 ∈ { 𝑧 } 𝑥 = 𝑧 )
131 50 50 130 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑥 ∈ { 𝑧 } 𝑥 = 𝑧 )
132 50 negnegd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → - - 𝑧 = 𝑧 )
133 131 132 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑥 ∈ { 𝑧 } 𝑥 = - - 𝑧 )
134 117 31 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = ( deg ‘ 𝑄 ) )
135 fveq2 ⊢ ( 𝑓 = 𝑄 → ( deg ‘ 𝑓 ) = ( deg ‘ 𝑄 ) )
136 135 eqeq2d ⊢ ( 𝑓 = 𝑄 → ( 𝐷 = ( deg ‘ 𝑓 ) ↔ 𝐷 = ( deg ‘ 𝑄 ) ) )
137 cnveq ⊢ ( 𝑓 = 𝑄 → ◡ 𝑓 = ◡ 𝑄 )
138 137 imaeq1d ⊢ ( 𝑓 = 𝑄 → ( ◡ 𝑓 “ { 0 } ) = ( ◡ 𝑄 “ { 0 } ) )
139 138 fveq2d ⊢ ( 𝑓 = 𝑄 → ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) )
140 139 135 eqeq12d ⊢ ( 𝑓 = 𝑄 → ( ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ↔ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = ( deg ‘ 𝑄 ) ) )
141 136 140 anbi12d ⊢ ( 𝑓 = 𝑄 → ( ( 𝐷 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) ↔ ( 𝐷 = ( deg ‘ 𝑄 ) ∧ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = ( deg ‘ 𝑄 ) ) ) )
142 138 sumeq1d ⊢ ( 𝑓 = 𝑄 → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 )
143 fveq2 ⊢ ( 𝑓 = 𝑄 → ( coeff ‘ 𝑓 ) = ( coeff ‘ 𝑄 ) )
144 135 oveq1d ⊢ ( 𝑓 = 𝑄 → ( ( deg ‘ 𝑓 ) − 1 ) = ( ( deg ‘ 𝑄 ) − 1 ) )
145 143 144 fveq12d ⊢ ( 𝑓 = 𝑄 → ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) )
146 143 135 fveq12d ⊢ ( 𝑓 = 𝑄 → ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) )
147 145 146 oveq12d ⊢ ( 𝑓 = 𝑄 → ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) = ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
148 147 negeqd ⊢ ( 𝑓 = 𝑄 → - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) = - ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
149 142 148 eqeq12d ⊢ ( 𝑓 = 𝑄 → ( Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ↔ Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) ) )
150 141 149 imbi12d ⊢ ( 𝑓 = 𝑄 → ( ( ( 𝐷 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) ↔ ( ( 𝐷 = ( deg ‘ 𝑄 ) ∧ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = ( deg ‘ 𝑄 ) ) → Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) ) ) )
151 8 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ∀ 𝑓 ∈ ( Poly ‘ ℂ ) ( ( 𝐷 = ( deg ‘ 𝑓 ) ∧ ( ♯ ‘ ( ◡ 𝑓 “ { 0 } ) ) = ( deg ‘ 𝑓 ) ) → Σ 𝑥 ∈ ( ◡ 𝑓 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑓 ) ‘ ( ( deg ‘ 𝑓 ) − 1 ) ) / ( ( coeff ‘ 𝑓 ) ‘ ( deg ‘ 𝑓 ) ) ) ) )
152 150 151 32 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( 𝐷 = ( deg ‘ 𝑄 ) ∧ ( ♯ ‘ ( ◡ 𝑄 “ { 0 } ) ) = ( deg ‘ 𝑄 ) ) → Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) ) )
153 31 134 152 mp2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
154 31 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) )
155 61 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( coeff ‘ 𝐹 ) = ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) )
156 1 155 eqtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐴 = ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) )
157 61 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ 𝐹 ) = ( deg ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) )
158 67 simp2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = 1 )
159 ax-1ne0 ⊢ 1 ≠ 0
160 159 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 1 ≠ 0 )
161 158 160 eqnetrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ≠ 0 )
162 fveq2 ⊢ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = ( deg ‘ 0𝑝 ) )
163 162 16 eqtrdi ⊢ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) = 0𝑝 → ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = 0 )
164 163 necon3i ⊢ ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ≠ 0 → ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ≠ 0𝑝 )
165 161 164 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ≠ 0𝑝 )
166 eqid ⊢ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) )
167 eqid ⊢ ( deg ‘ 𝑄 ) = ( deg ‘ 𝑄 )
168 166 167 dgrmul ⊢ ( ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ≠ 0𝑝 ) ∧ ( 𝑄 ∈ ( Poly ‘ ℂ ) ∧ 𝑄 ≠ 0𝑝 ) ) → ( deg ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) )
169 68 165 32 90 168 syl22anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) )
170 157 169 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( deg ‘ 𝐹 ) = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) )
171 2 170 eqtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝑁 = ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) )
172 156 171 fveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐴 ‘ 𝑁 ) = ( ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) ‘ ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) ) )
173 eqid ⊢ ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) )
174 eqid ⊢ ( coeff ‘ 𝑄 ) = ( coeff ‘ 𝑄 )
175 173 174 166 167 coemulhi ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ 𝑄 ∈ ( Poly ‘ ℂ ) ) → ( ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) ‘ ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) ) = ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) · ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
176 68 32 175 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) ‘ ( ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) + ( deg ‘ 𝑄 ) ) ) = ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) · ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
177 158 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) = ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) )
178 ssid ⊢ ℂ ⊆ ℂ
179 plyid ⊢ ( ( ℂ ⊆ ℂ ∧ 1 ∈ ℂ ) → Xp ∈ ( Poly ‘ ℂ ) )
180 178 100 179 mp2an ⊢ Xp ∈ ( Poly ‘ ℂ )
181 plyconst ⊢ ( ( ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ ) → ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) )
182 178 50 181 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) )
183 eqid ⊢ ( coeff ‘ Xp ) = ( coeff ‘ Xp )
184 eqid ⊢ ( coeff ‘ ( ℂ × { 𝑧 } ) ) = ( coeff ‘ ( ℂ × { 𝑧 } ) )
185 183 184 coesub ⊢ ( ( Xp ∈ ( Poly ‘ ℂ ) ∧ ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) ) → ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) )
186 180 182 185 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) = ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) )
187 186 fveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) = ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) )
188 1nn0 ⊢ 1 ∈ ℕ0
189 183 coef3 ⊢ ( Xp ∈ ( Poly ‘ ℂ ) → ( coeff ‘ Xp ) : ℕ0 ⟶ ℂ )
190 ffn ⊢ ( ( coeff ‘ Xp ) : ℕ0 ⟶ ℂ → ( coeff ‘ Xp ) Fn ℕ0 )
191 180 189 190 mp2b ⊢ ( coeff ‘ Xp ) Fn ℕ0
192 191 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( coeff ‘ Xp ) Fn ℕ0 )
193 184 coef3 ⊢ ( ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) → ( coeff ‘ ( ℂ × { 𝑧 } ) ) : ℕ0 ⟶ ℂ )
194 ffn ⊢ ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) : ℕ0 ⟶ ℂ → ( coeff ‘ ( ℂ × { 𝑧 } ) ) Fn ℕ0 )
195 182 193 194 3syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( coeff ‘ ( ℂ × { 𝑧 } ) ) Fn ℕ0 )
196 nn0ex ⊢ ℕ0 ∈ V
197 196 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ℕ0 ∈ V )
198 inidm ⊢ ( ℕ0 ∩ ℕ0 ) = ℕ0
199 coeidp ⊢ ( 1 ∈ ℕ0 → ( ( coeff ‘ Xp ) ‘ 1 ) = if ( 1 = 1 , 1 , 0 ) )
200 199 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( ( coeff ‘ Xp ) ‘ 1 ) = if ( 1 = 1 , 1 , 0 ) )
201 eqid ⊢ 1 = 1
202 201 iftruei ⊢ if ( 1 = 1 , 1 , 0 ) = 1
203 200 202 eqtrdi ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( ( coeff ‘ Xp ) ‘ 1 ) = 1 )
204 0lt1 ⊢ 0 < 1
205 0re ⊢ 0 ∈ ℝ
206 1re ⊢ 1 ∈ ℝ
207 205 206 ltnlei ⊢ ( 0 < 1 ↔ ¬ 1 ≤ 0 )
208 204 207 mpbi ⊢ ¬ 1 ≤ 0
209 50 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → 𝑧 ∈ ℂ )
210 0dgr ⊢ ( 𝑧 ∈ ℂ → ( deg ‘ ( ℂ × { 𝑧 } ) ) = 0 )
211 209 210 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( deg ‘ ( ℂ × { 𝑧 } ) ) = 0 )
212 211 breq2d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( 1 ≤ ( deg ‘ ( ℂ × { 𝑧 } ) ) ↔ 1 ≤ 0 ) )
213 208 212 mtbiri ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ¬ 1 ≤ ( deg ‘ ( ℂ × { 𝑧 } ) ) )
214 eqid ⊢ ( deg ‘ ( ℂ × { 𝑧 } ) ) = ( deg ‘ ( ℂ × { 𝑧 } ) )
215 184 214 dgrub ⊢ ( ( ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) ∧ 1 ∈ ℕ0 ∧ ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 1 ) ≠ 0 ) → 1 ≤ ( deg ‘ ( ℂ × { 𝑧 } ) ) )
216 215 3expia ⊢ ( ( ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) ∧ 1 ∈ ℕ0 ) → ( ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 1 ) ≠ 0 → 1 ≤ ( deg ‘ ( ℂ × { 𝑧 } ) ) ) )
217 182 216 sylan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 1 ) ≠ 0 → 1 ≤ ( deg ‘ ( ℂ × { 𝑧 } ) ) ) )
218 217 necon1bd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( ¬ 1 ≤ ( deg ‘ ( ℂ × { 𝑧 } ) ) → ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 1 ) = 0 ) )
219 213 218 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 1 ) = 0 )
220 192 195 197 197 198 203 219 ofval ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 1 ∈ ℕ0 ) → ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) = ( 1 − 0 ) )
221 188 220 mpan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) = ( 1 − 0 ) )
222 1m0e1 ⊢ ( 1 − 0 ) = 1
223 221 222 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) = 1 )
224 187 223 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) = 1 )
225 177 224 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) = 1 )
226 225 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) · ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) = ( 1 · ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
227 174 coef3 ⊢ ( 𝑄 ∈ ( Poly ‘ ℂ ) → ( coeff ‘ 𝑄 ) : ℕ0 ⟶ ℂ )
228 32 227 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( coeff ‘ 𝑄 ) : ℕ0 ⟶ ℂ )
229 228 34 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ∈ ℂ )
230 229 mullidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 1 · ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) )
231 226 230 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) · ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) )
232 172 176 231 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐴 ‘ 𝑁 ) = ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) )
233 154 232 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) = ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
234 233 negeqd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → - ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) = - ( ( ( coeff ‘ 𝑄 ) ‘ ( ( deg ‘ 𝑄 ) − 1 ) ) / ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) ) )
235 153 234 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 = - ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
236 133 235 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( Σ 𝑥 ∈ { 𝑧 } 𝑥 + Σ 𝑥 ∈ ( ◡ 𝑄 “ { 0 } ) 𝑥 ) = ( - - 𝑧 + - ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) )
237 50 negcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → - 𝑧 ∈ ℂ )
238 nnm1nn0 ⊢ ( 𝐷 ∈ ℕ → ( 𝐷 − 1 ) ∈ ℕ0 )
239 6 238 syl ⊢ ( 𝜑 → ( 𝐷 − 1 ) ∈ ℕ0 )
240 239 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐷 − 1 ) ∈ ℕ0 )
241 228 240 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ∈ ℂ )
242 232 229 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐴 ‘ 𝑁 ) ∈ ℂ )
243 2 1 dgreq0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
244 43 243 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
245 244 necon3bid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐹 ≠ 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) ≠ 0 ) )
246 82 245 mpbid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐴 ‘ 𝑁 ) ≠ 0 )
247 241 242 246 divcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ∈ ℂ )
248 237 247 negdid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → - ( - 𝑧 + ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) = ( - - 𝑧 + - ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) )
249 237 242 mulcld ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) ∈ ℂ )
250 249 241 242 246 divdird ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) + ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) / ( 𝐴 ‘ 𝑁 ) ) = ( ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) / ( 𝐴 ‘ 𝑁 ) ) + ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) )
251 nnm1nn0 ⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
252 11 251 syl ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
253 252 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑁 − 1 ) ∈ ℕ0 )
254 173 174 coemul ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ 𝑄 ∈ ( Poly ‘ ℂ ) ∧ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) ‘ ( 𝑁 − 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
255 68 32 253 254 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) ‘ ( 𝑁 − 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
256 156 fveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐴 ‘ ( 𝑁 − 1 ) ) = ( ( coeff ‘ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∘f · 𝑄 ) ) ‘ ( 𝑁 − 1 ) ) )
257 1e0p1 ⊢ 1 = ( 0 + 1 )
258 257 oveq2i ⊢ ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
259 258 sumeq1i ⊢ Σ 𝑘 ∈ ( 0 ... 1 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) )
260 0nn0 ⊢ 0 ∈ ℕ0
261 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
262 260 261 eleqtri ⊢ 0 ∈ ( ℤ≥ ‘ 0 )
263 262 a1i ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 0 ∈ ( ℤ≥ ‘ 0 ) )
264 258 eleq2i ⊢ ( 𝑘 ∈ ( 0 ... 1 ) ↔ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) )
265 173 coef3 ⊢ ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) → ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) : ℕ0 ⟶ ℂ )
266 68 265 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) : ℕ0 ⟶ ℂ )
267 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 1 ) → 𝑘 ∈ ℕ0 )
268 ffvelcdm ⊢ ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) : ℕ0 ⟶ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) ∈ ℂ )
269 266 267 268 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( 0 ... 1 ) ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) ∈ ℂ )
270 7 oveq1d ⊢ ( 𝜑 → ( ( 𝐷 + 1 ) − 1 ) = ( 𝑁 − 1 ) )
271 pncan ⊢ ( ( 𝐷 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐷 + 1 ) − 1 ) = 𝐷 )
272 101 100 271 sylancl ⊢ ( 𝜑 → ( ( 𝐷 + 1 ) − 1 ) = 𝐷 )
273 270 272 eqtr3d ⊢ ( 𝜑 → ( 𝑁 − 1 ) = 𝐷 )
274 273 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑁 − 1 ) = 𝐷 )
275 6 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → 𝐷 ∈ ℕ )
276 274 275 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑁 − 1 ) ∈ ℕ )
277 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
278 276 277 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) )
279 fzss2 ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 1 ) → ( 0 ... 1 ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) )
280 278 279 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 0 ... 1 ) ⊆ ( 0 ... ( 𝑁 − 1 ) ) )
281 280 sselda ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( 0 ... 1 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
282 fznn0sub ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 )
283 ffvelcdm ⊢ ( ( ( coeff ‘ 𝑄 ) : ℕ0 ⟶ ℂ ∧ ( ( 𝑁 − 1 ) − 𝑘 ) ∈ ℕ0 ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℂ )
284 228 282 283 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℂ )
285 281 284 syldan ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( 0 ... 1 ) ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℂ )
286 269 285 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( 0 ... 1 ) ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℂ )
287 264 286 sylan2br ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) ∈ ℂ )
288 id ⊢ ( 𝑘 = ( 0 + 1 ) → 𝑘 = ( 0 + 1 ) )
289 288 257 eqtr4di ⊢ ( 𝑘 = ( 0 + 1 ) → 𝑘 = 1 )
290 289 fveq2d ⊢ ( 𝑘 = ( 0 + 1 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) = ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) )
291 289 oveq2d ⊢ ( 𝑘 = ( 0 + 1 ) → ( ( 𝑁 − 1 ) − 𝑘 ) = ( ( 𝑁 − 1 ) − 1 ) )
292 291 fveq2d ⊢ ( 𝑘 = ( 0 + 1 ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) )
293 290 292 oveq12d ⊢ ( 𝑘 = ( 0 + 1 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) ) )
294 263 287 293 fsump1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑘 ∈ ( 0 ... ( 0 + 1 ) ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) ) ) )
295 259 294 eqtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) ) ) )
296 eldifn ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) → ¬ 𝑘 ∈ ( 0 ... 1 ) )
297 296 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ¬ 𝑘 ∈ ( 0 ... 1 ) )
298 eldifi ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) )
299 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ℕ0 )
300 298 299 syl ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) → 𝑘 ∈ ℕ0 )
301 173 166 dgrub ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ 𝑘 ∈ ℕ0 ∧ ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) ≠ 0 ) → 𝑘 ≤ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) )
302 301 3expia ⊢ ( ( ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ∈ ( Poly ‘ ℂ ) ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) )
303 68 300 302 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ≤ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) )
304 elfzuz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
305 298 304 syl ⊢ ( 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
306 305 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → 𝑘 ∈ ( ℤ≥ ‘ 0 ) )
307 1z ⊢ 1 ∈ ℤ
308 elfz5 ⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 0 ) ∧ 1 ∈ ℤ ) → ( 𝑘 ∈ ( 0 ... 1 ) ↔ 𝑘 ≤ 1 ) )
309 306 307 308 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( 𝑘 ∈ ( 0 ... 1 ) ↔ 𝑘 ≤ 1 ) )
310 158 breq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝑘 ≤ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ↔ 𝑘 ≤ 1 ) )
311 310 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( 𝑘 ≤ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ↔ 𝑘 ≤ 1 ) )
312 309 311 bitr4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( 𝑘 ∈ ( 0 ... 1 ) ↔ 𝑘 ≤ ( deg ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ) )
313 303 312 sylibrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) ≠ 0 → 𝑘 ∈ ( 0 ... 1 ) ) )
314 313 necon1bd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ¬ 𝑘 ∈ ( 0 ... 1 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) = 0 ) )
315 297 314 mpd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) = 0 )
316 315 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( 0 · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
317 298 284 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ∈ ℂ )
318 317 mul02d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( 0 · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = 0 )
319 316 318 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 𝑘 ∈ ( ( 0 ... ( 𝑁 − 1 ) ) ∖ ( 0 ... 1 ) ) ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = 0 )
320 fzfid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 0 ... ( 𝑁 − 1 ) ) ∈ Fin )
321 280 286 319 320 fsumss ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑘 ∈ ( 0 ... 1 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
322 0z ⊢ 0 ∈ ℤ
323 186 fveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) = ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) )
324 coeidp ⊢ ( 0 ∈ ℕ0 → ( ( coeff ‘ Xp ) ‘ 0 ) = if ( 0 = 1 , 1 , 0 ) )
325 159 nesymi ⊢ ¬ 0 = 1
326 325 iffalsei ⊢ if ( 0 = 1 , 1 , 0 ) = 0
327 324 326 eqtrdi ⊢ ( 0 ∈ ℕ0 → ( ( coeff ‘ Xp ) ‘ 0 ) = 0 )
328 327 adantl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 0 ∈ ℕ0 ) → ( ( coeff ‘ Xp ) ‘ 0 ) = 0 )
329 184 coefv0 ⊢ ( ( ℂ × { 𝑧 } ) ∈ ( Poly ‘ ℂ ) → ( ( ℂ × { 𝑧 } ) ‘ 0 ) = ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 0 ) )
330 182 329 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ℂ × { 𝑧 } ) ‘ 0 ) = ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 0 ) )
331 0cn ⊢ 0 ∈ ℂ
332 vex ⊢ 𝑧 ∈ V
333 332 fvconst2 ⊢ ( 0 ∈ ℂ → ( ( ℂ × { 𝑧 } ) ‘ 0 ) = 𝑧 )
334 331 333 ax-mp ⊢ ( ( ℂ × { 𝑧 } ) ‘ 0 ) = 𝑧
335 330 334 eqtr3di ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 0 ) = 𝑧 )
336 335 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 0 ∈ ℕ0 ) → ( ( coeff ‘ ( ℂ × { 𝑧 } ) ) ‘ 0 ) = 𝑧 )
337 192 195 197 197 198 328 336 ofval ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) ∧ 0 ∈ ℕ0 ) → ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) = ( 0 − 𝑧 ) )
338 260 337 mpan2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) = ( 0 − 𝑧 ) )
339 df-neg ⊢ - 𝑧 = ( 0 − 𝑧 )
340 338 339 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ Xp ) ∘f − ( coeff ‘ ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) = - 𝑧 )
341 323 340 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) = - 𝑧 )
342 274 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( 𝑁 − 1 ) − 0 ) = ( 𝐷 − 0 ) )
343 102 subid1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 𝐷 − 0 ) = 𝐷 )
344 342 343 31 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( 𝑁 − 1 ) − 0 ) = ( deg ‘ 𝑄 ) )
345 344 fveq2d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( deg ‘ 𝑄 ) ) )
346 345 232 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) = ( 𝐴 ‘ 𝑁 ) )
347 341 346 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) ) = ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) )
348 347 249 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) ) ∈ ℂ )
349 fveq2 ⊢ ( 𝑘 = 0 → ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) = ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) )
350 oveq2 ⊢ ( 𝑘 = 0 → ( ( 𝑁 − 1 ) − 𝑘 ) = ( ( 𝑁 − 1 ) − 0 ) )
351 350 fveq2d ⊢ ( 𝑘 = 0 → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) )
352 349 351 oveq12d ⊢ ( 𝑘 = 0 → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) ) )
353 352 fsum1 ⊢ ( ( 0 ∈ ℤ ∧ ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) ) )
354 322 348 353 sylancr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 0 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 0 ) ) ) )
355 354 347 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) = ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) )
356 274 fvoveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) )
357 224 356 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) ) = ( 1 · ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) )
358 241 mullidd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( 1 · ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) )
359 357 358 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) ) = ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) )
360 355 359 oveq12d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( Σ 𝑘 ∈ ( 0 ... 0 ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) + ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 1 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 1 ) ) ) ) = ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) + ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) )
361 295 321 360 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) + ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 − 1 ) ) ( ( ( coeff ‘ ( Xp ∘f − ( ℂ × { 𝑧 } ) ) ) ‘ 𝑘 ) · ( ( coeff ‘ 𝑄 ) ‘ ( ( 𝑁 − 1 ) − 𝑘 ) ) ) )
362 255 256 361 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) + ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) = ( 𝐴 ‘ ( 𝑁 − 1 ) ) )
363 362 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) + ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) ) / ( 𝐴 ‘ 𝑁 ) ) = ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
364 237 242 246 divcan4d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) / ( 𝐴 ‘ 𝑁 ) ) = - 𝑧 )
365 364 oveq1d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( ( ( - 𝑧 · ( 𝐴 ‘ 𝑁 ) ) / ( 𝐴 ‘ 𝑁 ) ) + ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) = ( - 𝑧 + ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) )
366 250 363 365 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( - 𝑧 + ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) = ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
367 366 negeqd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → - ( - 𝑧 + ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
368 248 367 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → ( - - 𝑧 + - ( ( ( coeff ‘ 𝑄 ) ‘ ( 𝐷 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) ) = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
369 128 236 368 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑅 ) → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )
370 28 369 exlimddv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝑅 𝑥 = - ( ( 𝐴 ‘ ( 𝑁 − 1 ) ) / ( 𝐴 ‘ 𝑁 ) ) )