MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vieta1lem2 Structured version   Visualization version   GIF version

Theorem vieta1lem2 25551
Description: Lemma for vieta1 25552: inductive step. Let 𝑧 be a root of 𝐹. Then 𝐹 = (Xp𝑧) · 𝑄 for some 𝑄 by the factor theorem, and 𝑄 is a degree- 𝐷 polynomial, so by the induction hypothesis Σ𝑥 ∈ (𝑄 “ 0)𝑥 = -(coeff‘𝑄)‘(𝐷 − 1) / (coeff‘𝑄)‘𝐷, so Σ𝑥𝑅𝑥 = 𝑧 − (coeff‘𝑄)‘ (𝐷 − 1) / (coeff‘𝑄)‘𝐷. Now the coefficients of 𝐹 are 𝐴‘(𝐷 + 1) = (coeff‘𝑄)‘𝐷 and 𝐴𝐷 = Σ𝑘 ∈ (0...𝐷)(coeff‘Xp𝑧)‘𝑘 · (coeff‘𝑄) ‘(𝐷𝑘), which works out to -𝑧 · (coeff‘𝑄)‘𝐷 + (coeff‘𝑄)‘(𝐷 − 1), so putting it all together we have Σ𝑥𝑅𝑥 = -𝐴𝐷 / 𝐴‘(𝐷 + 1) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014.)
Hypotheses
Ref Expression
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 (Xpf − (ℂ × {𝑧})))
Assertion
Ref Expression
vieta1lem2 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Distinct variable groups:   𝐷,𝑓   𝑓,𝐹   𝑧,𝑓,𝑁   𝑥,𝑓,𝑄   𝑅,𝑓   𝑥,𝑧,𝑅   𝐴,𝑓,𝑧   𝜑,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑓)   𝐴(𝑥)   𝐷(𝑥,𝑧)   𝑄(𝑧)   𝑆(𝑥,𝑧,𝑓)   𝐹(𝑥,𝑧)   𝑁(𝑥)

Proof of Theorem vieta1lem2
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 vieta1.5 . . . . 5 (𝜑 → (♯‘𝑅) = 𝑁)
2 vieta1lem.7 . . . . . . 7 (𝜑 → (𝐷 + 1) = 𝑁)
3 vieta1lem.6 . . . . . . . 8 (𝜑𝐷 ∈ ℕ)
43peano2nnd 12069 . . . . . . 7 (𝜑 → (𝐷 + 1) ∈ ℕ)
52, 4eqeltrrd 2838 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnne0d 12102 . . . . 5 (𝜑𝑁 ≠ 0)
71, 6eqnetrd 3008 . . . 4 (𝜑 → (♯‘𝑅) ≠ 0)
8 vieta1.4 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘𝑆))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (deg‘𝐹)
109, 6eqnetrrid 3016 . . . . . . . . 9 (𝜑 → (deg‘𝐹) ≠ 0)
11 fveq2 6811 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 25503 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12eqtrdi 2792 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
1413necon3i 2973 . . . . . . . . 9 ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
1510, 14syl 17 . . . . . . . 8 (𝜑𝐹 ≠ 0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
1716fta1 25548 . . . . . . . 8 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
188, 15, 17syl2anc 584 . . . . . . 7 (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
1918simpld 495 . . . . . 6 (𝜑𝑅 ∈ Fin)
20 hasheq0 14156 . . . . . 6 (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
2119, 20syl 17 . . . . 5 (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
2221necon3bid 2985 . . . 4 (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
237, 22mpbid 231 . . 3 (𝜑𝑅 ≠ ∅)
24 n0 4290 . . 3 (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧𝑅)
2523, 24sylib 217 . 2 (𝜑 → ∃𝑧 𝑧𝑅)
26 incom 4145 . . . . 5 ({𝑧} ∩ (𝑄 “ {0})) = ((𝑄 “ {0}) ∩ {𝑧})
27 vieta1.1 . . . . . . . . . . 11 𝐴 = (coeff‘𝐹)
28 vieta1lem.8 . . . . . . . . . . 11 (𝜑 → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
29 vieta1lem.9 . . . . . . . . . . 11 𝑄 = (𝐹 quot (Xpf − (ℂ × {𝑧})))
3027, 9, 16, 8, 1, 3, 2, 28, 29vieta1lem1 25550 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
3130simprd 496 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐷 = (deg‘𝑄))
3230simpld 495 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝑄 ∈ (Poly‘ℂ))
33 dgrcl 25474 . . . . . . . . . . 11 (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
3432, 33syl 17 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℕ0)
3534nn0red 12373 . . . . . . . . 9 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℝ)
3631, 35eqeltrd 2837 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 ∈ ℝ)
3736ltp1d 11984 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 < (𝐷 + 1))
3836, 37gtned 11189 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 + 1) ≠ 𝐷)
39 snssi 4752 . . . . . . . . . . 11 (𝑧 ∈ (𝑄 “ {0}) → {𝑧} ⊆ (𝑄 “ {0}))
40 ssequn1 4124 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑄 “ {0}) ↔ ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4139, 40sylib 217 . . . . . . . . . 10 (𝑧 ∈ (𝑄 “ {0}) → ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4241fveq2d 6815 . . . . . . . . 9 (𝑧 ∈ (𝑄 “ {0}) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (♯‘(𝑄 “ {0})))
438adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘𝑆))
44 cnvimass 6006 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 “ {0}) ⊆ dom 𝐹
4516, 44eqsstri 3964 . . . . . . . . . . . . . . . . . . . 20 𝑅 ⊆ dom 𝐹
46 plyf 25439 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47 fdm 6646 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝐹 = ℂ)
4945, 48sseqtrid 3982 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑅 ⊆ ℂ)
5049sselda 3930 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝑧 ∈ ℂ)
5116eleq2i 2828 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑅𝑧 ∈ (𝐹 “ {0}))
52 ffn 6637 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53 fniniseg 6976 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℂ → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5551, 54bitrid 282 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5655simplbda 500 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝐹𝑧) = 0)
57 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (Xpf − (ℂ × {𝑧})) = (Xpf − (ℂ × {𝑧}))
5857facth 25546 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧})))))
5943, 50, 56, 58syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧})))))
6029oveq2i 7327 . . . . . . . . . . . . . . . . 17 ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧}))))
6159, 60eqtr4di 2794 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))
6261cnveqd 5804 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))
6362imaeq1d 5985 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝐹 “ {0}) = (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
6416, 63eqtrid 2788 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 𝑅 = (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65 cnex 11031 . . . . . . . . . . . . . 14 ℂ ∈ V
6657plyremlem 25544 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℂ → ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xpf − (ℂ × {𝑧}))) = 1 ∧ ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6750, 66syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xpf − (ℂ × {𝑧}))) = 1 ∧ ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6867simp1d 1141 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69 plyf 25439 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ)
71 plyf 25439 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
7232, 71syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄:ℂ⟶ℂ)
73 ofmulrt 25522 . . . . . . . . . . . . . 14 ((ℂ ∈ V ∧ (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7465, 70, 72, 73mp3an2i 1465 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7567simp3d 1143 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧})
7675uneq1d 4106 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})) = ({𝑧} ∪ (𝑄 “ {0})))
7764, 74, 763eqtrd 2780 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → 𝑅 = ({𝑧} ∪ (𝑄 “ {0})))
7877fveq2d 6815 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (𝑄 “ {0}))))
791, 2eqtr4d 2779 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑅) = (𝐷 + 1))
8079adantr 481 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘𝑅) = (𝐷 + 1))
8178, 80eqtr3d 2778 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (𝐷 + 1))
8215adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ≠ 0𝑝)
8361, 82eqnetrrd 3009 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84 plymul0or 25521 . . . . . . . . . . . . . . . . . . 19 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8568, 32, 84syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8685necon3abid 2977 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8783, 86mpbid 231 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
88 neanior 3034 . . . . . . . . . . . . . . . 16 (((Xpf − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝) ↔ ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
8987, 88sylibr 233 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝))
9089simprd 496 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄 ≠ 0𝑝)
91 eqid 2736 . . . . . . . . . . . . . . 15 (𝑄 “ {0}) = (𝑄 “ {0})
9291fta1 25548 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((𝑄 “ {0}) ∈ Fin ∧ (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9332, 90, 92syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∈ Fin ∧ (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9493simprd 496 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄))
9594, 31breqtrrd 5114 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ≤ 𝐷)
96 snfi 8887 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9793simpld 495 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝑄 “ {0}) ∈ Fin)
98 hashun2 14176 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))))
9996, 97, 98sylancr 587 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))))
100 ax-1cn 11008 . . . . . . . . . . . . . . 15 1 ∈ ℂ
1013nncnd 12068 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
102101adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐷 ∈ ℂ)
103 addcom 11240 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104100, 102, 103sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (1 + 𝐷) = (𝐷 + 1))
10581, 104eqtr4d 2779 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (1 + 𝐷))
106 hashsng 14162 . . . . . . . . . . . . . . 15 (𝑧𝑅 → (♯‘{𝑧}) = 1)
107106adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (♯‘{𝑧}) = 1)
108107oveq1d 7331 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))) = (1 + (♯‘(𝑄 “ {0}))))
10999, 105, 1083brtr3d 5117 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(𝑄 “ {0}))))
110 hashcl 14149 . . . . . . . . . . . . . . 15 ((𝑄 “ {0}) ∈ Fin → (♯‘(𝑄 “ {0})) ∈ ℕ0)
11197, 110syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ∈ ℕ0)
112111nn0red 12373 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ∈ ℝ)
113 1red 11055 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 1 ∈ ℝ)
11436, 112, 113leadd2d 11649 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (𝐷 ≤ (♯‘(𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(𝑄 “ {0})))))
115109, 114mpbird 256 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝐷 ≤ (♯‘(𝑄 “ {0})))
116112, 36letri3d 11196 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((♯‘(𝑄 “ {0})) = 𝐷 ↔ ((♯‘(𝑄 “ {0})) ≤ 𝐷𝐷 ≤ (♯‘(𝑄 “ {0})))))
11795, 115, 116mpbir2and 710 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) = 𝐷)
11881, 117eqeq12d 2752 . . . . . . . . 9 ((𝜑𝑧𝑅) → ((♯‘({𝑧} ∪ (𝑄 “ {0}))) = (♯‘(𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
11942, 118syl5ib 243 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝑧 ∈ (𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120119necon3ad 2953 . . . . . . 7 ((𝜑𝑧𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (𝑄 “ {0})))
12138, 120mpd 15 . . . . . 6 ((𝜑𝑧𝑅) → ¬ 𝑧 ∈ (𝑄 “ {0}))
122 disjsn 4656 . . . . . 6 (((𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑄 “ {0}))
123121, 122sylibr 233 . . . . 5 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∩ {𝑧}) = ∅)
12426, 123eqtrid 2788 . . . 4 ((𝜑𝑧𝑅) → ({𝑧} ∩ (𝑄 “ {0})) = ∅)
12519adantr 481 . . . 4 ((𝜑𝑧𝑅) → 𝑅 ∈ Fin)
12649adantr 481 . . . . 5 ((𝜑𝑧𝑅) → 𝑅 ⊆ ℂ)
127126sselda 3930 . . . 4 (((𝜑𝑧𝑅) ∧ 𝑥𝑅) → 𝑥 ∈ ℂ)
128124, 77, 125, 127fsumsplit 15529 . . 3 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥))
129 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
130129sumsn 15534 . . . . . 6 ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13150, 50, 130syl2anc 584 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13250negnegd 11402 . . . . 5 ((𝜑𝑧𝑅) → --𝑧 = 𝑧)
133131, 132eqtr4d 2779 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134117, 31eqtrd 2776 . . . . . 6 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) = (deg‘𝑄))
135 fveq2 6811 . . . . . . . . . 10 (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136135eqeq2d 2747 . . . . . . . . 9 (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137 cnveq 5802 . . . . . . . . . . . 12 (𝑓 = 𝑄𝑓 = 𝑄)
138137imaeq1d 5985 . . . . . . . . . . 11 (𝑓 = 𝑄 → (𝑓 “ {0}) = (𝑄 “ {0}))
139138fveq2d 6815 . . . . . . . . . 10 (𝑓 = 𝑄 → (♯‘(𝑓 “ {0})) = (♯‘(𝑄 “ {0})))
140139, 135eqeq12d 2752 . . . . . . . . 9 (𝑓 = 𝑄 → ((♯‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(𝑄 “ {0})) = (deg‘𝑄)))
141136, 140anbi12d 631 . . . . . . . 8 (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄))))
142138sumeq1d 15489 . . . . . . . . 9 (𝑓 = 𝑄 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥 ∈ (𝑄 “ {0})𝑥)
143 fveq2 6811 . . . . . . . . . . . 12 (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144135oveq1d 7331 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145143, 144fveq12d 6818 . . . . . . . . . . 11 (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146143, 135fveq12d 6818 . . . . . . . . . . 11 (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147145, 146oveq12d 7334 . . . . . . . . . 10 (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148147negeqd 11294 . . . . . . . . 9 (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149142, 148eqeq12d 2752 . . . . . . . 8 (𝑓 = 𝑄 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
150141, 149imbi12d 344 . . . . . . 7 (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
15128adantr 481 . . . . . . 7 ((𝜑𝑧𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
152150, 151, 32rspcdva 3570 . . . . . 6 ((𝜑𝑧𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
15331, 134, 152mp2and 696 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
15431fvoveq1d 7338 . . . . . . 7 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
15561fveq2d 6815 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (coeff‘𝐹) = (coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15627, 155eqtrid 2788 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐴 = (coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15761fveq2d 6815 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘𝐹) = (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15867simp2d 1142 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (deg‘(Xpf − (ℂ × {𝑧}))) = 1)
159 ax-1ne0 11019 . . . . . . . . . . . . . . 15 1 ≠ 0
160159a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 1 ≠ 0)
161158, 160eqnetrd 3008 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (deg‘(Xpf − (ℂ × {𝑧}))) ≠ 0)
162 fveq2 6811 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xpf − (ℂ × {𝑧}))) = (deg‘0𝑝))
163162, 12eqtrdi 2792 . . . . . . . . . . . . . 14 ((Xpf − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xpf − (ℂ × {𝑧}))) = 0)
164163necon3i 2973 . . . . . . . . . . . . 13 ((deg‘(Xpf − (ℂ × {𝑧}))) ≠ 0 → (Xpf − (ℂ × {𝑧})) ≠ 0𝑝)
165161, 164syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})) ≠ 0𝑝)
166 eqid 2736 . . . . . . . . . . . . 13 (deg‘(Xpf − (ℂ × {𝑧}))) = (deg‘(Xpf − (ℂ × {𝑧})))
167 eqid 2736 . . . . . . . . . . . . 13 (deg‘𝑄) = (deg‘𝑄)
168166, 167dgrmul 25511 . . . . . . . . . . . 12 ((((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xpf − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
16968, 165, 32, 90, 168syl22anc 836 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
170157, 169eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝐹) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
1719, 170eqtrid 2788 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝑁 = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
172156, 171fveq12d 6818 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))))
173 eqid 2736 . . . . . . . . . 10 (coeff‘(Xpf − (ℂ × {𝑧}))) = (coeff‘(Xpf − (ℂ × {𝑧})))
174 eqid 2736 . . . . . . . . . 10 (coeff‘𝑄) = (coeff‘𝑄)
175173, 174, 166, 167coemulhi 25495 . . . . . . . . 9 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
17668, 32, 175syl2anc 584 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
177158fveq2d 6815 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘1))
178 ssid 3952 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
179 plyid 25450 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180178, 100, 179mp2an 689 . . . . . . . . . . . . . 14 Xp ∈ (Poly‘ℂ)
181 plyconst 25447 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182178, 50, 181sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183 eqid 2736 . . . . . . . . . . . . . . 15 (coeff‘Xp) = (coeff‘Xp)
184 eqid 2736 . . . . . . . . . . . . . . 15 (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185183, 184coesub 25498 . . . . . . . . . . . . . 14 ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xpf − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
186180, 182, 185sylancr 587 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (coeff‘(Xpf − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
187186fveq1d 6813 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188 1nn0 12328 . . . . . . . . . . . . . 14 1 ∈ ℕ0
189183coef3 25473 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190 ffn 6637 . . . . . . . . . . . . . . . . 17 ((coeff‘Xp):ℕ0⟶ℂ → (coeff‘Xp) Fn ℕ0)
191180, 189, 190mp2b 10 . . . . . . . . . . . . . . . 16 (coeff‘Xp) Fn ℕ0
192191a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘Xp) Fn ℕ0)
193184coef3 25473 . . . . . . . . . . . . . . . 16 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194 ffn 6637 . . . . . . . . . . . . . . . 16 ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195182, 193, 1943syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196 nn0ex 12318 . . . . . . . . . . . . . . . 16 0 ∈ V
197196a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ℕ0 ∈ V)
198 inidm 4162 . . . . . . . . . . . . . . 15 (ℕ0 ∩ ℕ0) = ℕ0
199 coeidp 25504 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
200199adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
201 eqid 2736 . . . . . . . . . . . . . . . . 17 1 = 1
202201iftruei 4477 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
203200, 202eqtrdi 2792 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204 0lt1 11576 . . . . . . . . . . . . . . . . . 18 0 < 1
205 0re 11056 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
206 1re 11054 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
207205, 206ltnlei 11175 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ ¬ 1 ≤ 0)
208204, 207mpbi 229 . . . . . . . . . . . . . . . . 17 ¬ 1 ≤ 0
20950adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210 0dgr 25486 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212211breq2d 5098 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213208, 212mtbiri 326 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214 eqid 2736 . . . . . . . . . . . . . . . . . . . 20 (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215184, 214dgrub 25475 . . . . . . . . . . . . . . . . . . 19 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
2162153expia 1120 . . . . . . . . . . . . . . . . . 18 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
217182, 216sylan 580 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
218217necon1bd 2958 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
219213, 218mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
220192, 195, 197, 197, 198, 203, 219ofval 7585 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
221188, 220mpan2 688 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222 1m0e1 12173 . . . . . . . . . . . . 13 (1 − 0) = 1
223221, 222eqtrdi 2792 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224187, 223eqtrd 2776 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘1) = 1)
225177, 224eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) = 1)
226225oveq1d 7331 . . . . . . . . 9 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227174coef3 25473 . . . . . . . . . . . 12 (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
22832, 227syl 17 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229228, 34ffvelcdmd 7001 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230229mulid2d 11072 . . . . . . . . 9 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231226, 230eqtrd 2776 . . . . . . . 8 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232172, 176, 2313eqtrd 2780 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233154, 232oveq12d 7334 . . . . . 6 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234233negeqd 11294 . . . . 5 ((𝜑𝑧𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235153, 234eqtr4d 2779 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)))
236133, 235oveq12d 7334 . . 3 ((𝜑𝑧𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
23750negcld 11398 . . . . 5 ((𝜑𝑧𝑅) → -𝑧 ∈ ℂ)
238 nnm1nn0 12353 . . . . . . . . 9 (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
2393, 238syl 17 . . . . . . . 8 (𝜑 → (𝐷 − 1) ∈ ℕ0)
240239adantr 481 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 − 1) ∈ ℕ0)
241228, 240ffvelcdmd 7001 . . . . . 6 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242232, 229eqeltrd 2837 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ∈ ℂ)
2439, 27dgreq0 25506 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
24443, 243syl 17 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
245244necon3bid 2985 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴𝑁) ≠ 0))
24682, 245mpbid 231 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ≠ 0)
247241, 242, 246divcld 11830 . . . . 5 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) ∈ ℂ)
248237, 247negdid 11424 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
249237, 242mulcld 11074 . . . . . . 7 ((𝜑𝑧𝑅) → (-𝑧 · (𝐴𝑁)) ∈ ℂ)
250249, 241, 242, 246divdird 11868 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
251 nnm1nn0 12353 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
2525, 251syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
253252adantr 481 . . . . . . . . 9 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ0)
254173, 174coemul 25493 . . . . . . . . 9 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
25568, 32, 253, 254syl3anc 1370 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256156fveq1d 6813 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257 1e0p1 12558 . . . . . . . . . . . 12 1 = (0 + 1)
258257oveq2i 7327 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
259258sumeq1i 15486 . . . . . . . . . 10 Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260 0nn0 12327 . . . . . . . . . . . . 13 0 ∈ ℕ0
261 nn0uz 12699 . . . . . . . . . . . . 13 0 = (ℤ‘0)
262260, 261eleqtri 2835 . . . . . . . . . . . 12 0 ∈ (ℤ‘0)
263262a1i 11 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 0 ∈ (ℤ‘0))
264258eleq2i 2828 . . . . . . . . . . . 12 (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265173coef3 25473 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ)
26668, 265syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267 elfznn0 13428 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268 ffvelcdm 6998 . . . . . . . . . . . . . 14 (((coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269266, 267, 268syl2an 596 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
2702oveq1d 7331 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271 pncan 11306 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272101, 100, 271sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273270, 272eqtr3d 2778 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) = 𝐷)
274273adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝑁 − 1) = 𝐷)
2753adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐷 ∈ ℕ)
276274, 275eqeltrd 2837 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ)
277 nnuz 12700 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
278276, 277eleqtrdi 2847 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ (ℤ‘1))
279 fzss2 13375 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ (ℤ‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280278, 279syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281280sselda 3930 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282 fznn0sub 13367 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283 ffvelcdm 6998 . . . . . . . . . . . . . . 15 (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
284228, 282, 283syl2an 596 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
285281, 284syldan 591 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
286269, 285mulcld 11074 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
287264, 286sylan2br 595 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
288 id 22 . . . . . . . . . . . . . 14 (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
289288, 257eqtr4di 2794 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → 𝑘 = 1)
290289fveq2d 6815 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘1))
291289oveq2d 7332 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292291fveq2d 6815 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293290, 292oveq12d 7334 . . . . . . . . . . 11 (𝑘 = (0 + 1) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294263, 287, 293fsump1 15544 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
295259, 294eqtrid 2788 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296 eldifn 4072 . . . . . . . . . . . . . 14 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297296adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298 eldifi 4071 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299 elfznn0 13428 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300298, 299syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301173, 166dgrub 25475 . . . . . . . . . . . . . . . . 17 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))))
3023013expia 1120 . . . . . . . . . . . . . . . 16 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
30368, 300, 302syl2an 596 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
304 elfzuz 13331 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ‘0))
305298, 304syl 17 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ‘0))
306305adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ‘0))
307 1z 12429 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
308 elfz5 13327 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309306, 307, 308sylancl 586 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310158breq2d 5098 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
311310adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
312309, 311bitr4d 281 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
313303, 312sylibrd 258 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
314313necon1bd 2958 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = 0))
315297, 314mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = 0)
316315oveq1d 7331 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
317298, 284sylan2 593 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
318317mul02d 11252 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319316, 318eqtrd 2776 . . . . . . . . . 10 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320 fzfid 13772 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321280, 286, 319, 320fsumss 15513 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322 0z 12409 . . . . . . . . . . . 12 0 ∈ ℤ
323186fveq1d 6813 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324 coeidp 25504 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325159nesymi 2998 . . . . . . . . . . . . . . . . . . . . 21 ¬ 0 = 1
326325iffalsei 4480 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
327324, 326eqtrdi 2792 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328327adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329184coefv0 25489 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
330182, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
331 0cn 11046 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℂ
332 vex 3444 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
333332fvconst2 7118 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
334331, 333ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℂ × {𝑧})‘0) = 𝑧
335330, 334eqtr3di 2791 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336335adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337192, 195, 197, 197, 198, 328, 336ofval 7585 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338260, 337mpan2 688 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339 df-neg 11287 . . . . . . . . . . . . . . . 16 -𝑧 = (0 − 𝑧)
340338, 339eqtr4di 2794 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341323, 340eqtrd 2776 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘0) = -𝑧)
342274oveq1d 7331 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343102subid1d 11400 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝐷 − 0) = 𝐷)
344342, 343, 313eqtrd 2780 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345344fveq2d 6815 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346345, 232eqtr4d 2779 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴𝑁))
347341, 346oveq12d 7334 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴𝑁)))
348347, 249eqeltrd 2837 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349 fveq2 6811 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘0))
350 oveq2 7324 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351350fveq2d 6815 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352349, 351oveq12d 7334 . . . . . . . . . . . . 13 (𝑘 = 0 → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353352fsum1 15535 . . . . . . . . . . . 12 ((0 ∈ ℤ ∧ (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
354322, 348, 353sylancr 587 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
355354, 347eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴𝑁)))
356274fvoveq1d 7338 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357224, 356oveq12d 7334 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358241mulid2d 11072 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359357, 358eqtrd 2776 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360355, 359oveq12d 7334 . . . . . . . . 9 ((𝜑𝑧𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361295, 321, 3603eqtr3rd 2785 . . . . . . . 8 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362255, 256, 3613eqtr4rd 2787 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363362oveq1d 7331 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
364237, 242, 246divcan4d 11836 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) = -𝑧)
365364oveq1d 7331 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
366250, 363, 3653eqtr3rd 2785 . . . . 5 ((𝜑𝑧𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
367366negeqd 11294 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
368248, 367eqtr3d 2778 . . 3 ((𝜑𝑧𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
369128, 236, 3683eqtrd 2780 . 2 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
37025, 369exlimddv 1937 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3a 1086   = wceq 1540  wex 1780  wcel 2105  wne 2940  wral 3061  Vcvv 3440  cdif 3893  cun 3894  cin 3895  wss 3896  c0 4266  ifcif 4470  {csn 4570   class class class wbr 5086   × cxp 5605  ccnv 5606  dom cdm 5607  cima 5610   Fn wfn 6460  wf 6461  cfv 6465  (class class class)co 7316  f cof 7572  Fincfn 8782  cc 10948  cr 10949  0cc0 10950  1c1 10951   + caddc 10953   · cmul 10955   < clt 11088  cle 11089  cmin 11284  -cneg 11285   / cdiv 11711  cn 12052  0cn0 12312  cz 12398  cuz 12661  ...cfz 13318  chash 14123  Σcsu 15473  0𝑝c0p 24913  Polycply 25425  Xpcidp 25426  coeffccoe 25427  degcdgr 25428   quot cquot 25530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-inf2 9476  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027  ax-pre-sup 11028
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-int 4892  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-se 5563  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-isom 6474  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-of 7574  df-om 7759  df-1st 7877  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-1o 8345  df-oadd 8349  df-er 8547  df-map 8666  df-pm 8667  df-en 8783  df-dom 8784  df-sdom 8785  df-fin 8786  df-sup 9277  df-inf 9278  df-oi 9345  df-dju 9736  df-card 9774  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-div 11712  df-nn 12053  df-2 12115  df-3 12116  df-n0 12313  df-xnn0 12385  df-z 12399  df-uz 12662  df-rp 12810  df-fz 13319  df-fzo 13462  df-fl 13591  df-seq 13801  df-exp 13862  df-hash 14124  df-cj 14886  df-re 14887  df-im 14888  df-sqrt 15022  df-abs 15023  df-clim 15273  df-rlim 15274  df-sum 15474  df-0p 24914  df-ply 25429  df-idp 25430  df-coe 25431  df-dgr 25432  df-quot 25531
This theorem is referenced by:  vieta1  25552
  Copyright terms: Public domain W3C validator