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

Theorem vieta1lem2 26353
Description: Lemma for vieta1 26354: 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 12283 . . . . . . 7 (𝜑 → (𝐷 + 1) ∈ ℕ)
52, 4eqeltrrd 2842 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnne0d 12316 . . . . 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 6906 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 26302 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12eqtrdi 2793 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
1413necon3i 2973 . . . . . . . . 9 ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
1510, 14syl 17 . . . . . . . 8 (𝜑𝐹 ≠ 0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
1716fta1 26350 . . . . . . . 8 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
188, 15, 17syl2anc 584 . . . . . . 7 (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
1918simpld 494 . . . . . 6 (𝜑𝑅 ∈ Fin)
20 hasheq0 14402 . . . . . 6 (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
2119, 20syl 17 . . . . 5 (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
2221necon3bid 2985 . . . 4 (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
237, 22mpbid 232 . . 3 (𝜑𝑅 ≠ ∅)
24 n0 4353 . . 3 (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧𝑅)
2523, 24sylib 218 . 2 (𝜑 → ∃𝑧 𝑧𝑅)
26 incom 4209 . . . . 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 26352 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
3130simprd 495 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐷 = (deg‘𝑄))
3230simpld 494 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝑄 ∈ (Poly‘ℂ))
33 dgrcl 26272 . . . . . . . . . . 11 (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
3432, 33syl 17 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℕ0)
3534nn0red 12588 . . . . . . . . 9 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℝ)
3631, 35eqeltrd 2841 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 ∈ ℝ)
3736ltp1d 12198 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 < (𝐷 + 1))
3836, 37gtned 11396 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 + 1) ≠ 𝐷)
39 snssi 4808 . . . . . . . . . . 11 (𝑧 ∈ (𝑄 “ {0}) → {𝑧} ⊆ (𝑄 “ {0}))
40 ssequn1 4186 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑄 “ {0}) ↔ ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4139, 40sylib 218 . . . . . . . . . 10 (𝑧 ∈ (𝑄 “ {0}) → ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4241fveq2d 6910 . . . . . . . . 9 (𝑧 ∈ (𝑄 “ {0}) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (♯‘(𝑄 “ {0})))
438adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘𝑆))
44 cnvimass 6100 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 “ {0}) ⊆ dom 𝐹
4516, 44eqsstri 4030 . . . . . . . . . . . . . . . . . . . 20 𝑅 ⊆ dom 𝐹
46 plyf 26237 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47 fdm 6745 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝐹 = ℂ)
4945, 48sseqtrid 4026 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑅 ⊆ ℂ)
5049sselda 3983 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝑧 ∈ ℂ)
5116eleq2i 2833 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑅𝑧 ∈ (𝐹 “ {0}))
52 ffn 6736 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53 fniniseg 7080 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℂ → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5551, 54bitrid 283 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5655simplbda 499 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝐹𝑧) = 0)
57 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (Xpf − (ℂ × {𝑧})) = (Xpf − (ℂ × {𝑧}))
5857facth 26348 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧})))))
5943, 50, 56, 58syl3anc 1373 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧})))))
6029oveq2i 7442 . . . . . . . . . . . . . . . . 17 ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧}))))
6159, 60eqtr4di 2795 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))
6261cnveqd 5886 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))
6362imaeq1d 6077 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝐹 “ {0}) = (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
6416, 63eqtrid 2789 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 𝑅 = (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65 cnex 11236 . . . . . . . . . . . . . 14 ℂ ∈ V
6657plyremlem 26346 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℂ → ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xpf − (ℂ × {𝑧}))) = 1 ∧ ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6750, 66syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xpf − (ℂ × {𝑧}))) = 1 ∧ ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6867simp1d 1143 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69 plyf 26237 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ)
71 plyf 26237 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
7232, 71syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄:ℂ⟶ℂ)
73 ofmulrt 26323 . . . . . . . . . . . . . 14 ((ℂ ∈ V ∧ (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7465, 70, 72, 73mp3an2i 1468 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7567simp3d 1145 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧})
7675uneq1d 4167 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})) = ({𝑧} ∪ (𝑄 “ {0})))
7764, 74, 763eqtrd 2781 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → 𝑅 = ({𝑧} ∪ (𝑄 “ {0})))
7877fveq2d 6910 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (𝑄 “ {0}))))
791, 2eqtr4d 2780 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑅) = (𝐷 + 1))
8079adantr 480 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘𝑅) = (𝐷 + 1))
8178, 80eqtr3d 2779 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (𝐷 + 1))
8215adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ≠ 0𝑝)
8361, 82eqnetrrd 3009 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84 plymul0or 26322 . . . . . . . . . . . . . . . . . . 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 232 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
88 neanior 3035 . . . . . . . . . . . . . . . 16 (((Xpf − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝) ↔ ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
8987, 88sylibr 234 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝))
9089simprd 495 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄 ≠ 0𝑝)
91 eqid 2737 . . . . . . . . . . . . . . 15 (𝑄 “ {0}) = (𝑄 “ {0})
9291fta1 26350 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((𝑄 “ {0}) ∈ Fin ∧ (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9332, 90, 92syl2anc 584 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∈ Fin ∧ (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9493simprd 495 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄))
9594, 31breqtrrd 5171 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ≤ 𝐷)
96 snfi 9083 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9793simpld 494 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝑄 “ {0}) ∈ Fin)
98 hashun2 14422 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))))
9996, 97, 98sylancr 587 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))))
100 ax-1cn 11213 . . . . . . . . . . . . . . 15 1 ∈ ℂ
1013nncnd 12282 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
102101adantr 480 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐷 ∈ ℂ)
103 addcom 11447 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104100, 102, 103sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (1 + 𝐷) = (𝐷 + 1))
10581, 104eqtr4d 2780 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (1 + 𝐷))
106 hashsng 14408 . . . . . . . . . . . . . . 15 (𝑧𝑅 → (♯‘{𝑧}) = 1)
107106adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (♯‘{𝑧}) = 1)
108107oveq1d 7446 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))) = (1 + (♯‘(𝑄 “ {0}))))
10999, 105, 1083brtr3d 5174 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(𝑄 “ {0}))))
110 hashcl 14395 . . . . . . . . . . . . . . 15 ((𝑄 “ {0}) ∈ Fin → (♯‘(𝑄 “ {0})) ∈ ℕ0)
11197, 110syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ∈ ℕ0)
112111nn0red 12588 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ∈ ℝ)
113 1red 11262 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 1 ∈ ℝ)
11436, 112, 113leadd2d 11858 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (𝐷 ≤ (♯‘(𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(𝑄 “ {0})))))
115109, 114mpbird 257 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝐷 ≤ (♯‘(𝑄 “ {0})))
116112, 36letri3d 11403 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((♯‘(𝑄 “ {0})) = 𝐷 ↔ ((♯‘(𝑄 “ {0})) ≤ 𝐷𝐷 ≤ (♯‘(𝑄 “ {0})))))
11795, 115, 116mpbir2and 713 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) = 𝐷)
11881, 117eqeq12d 2753 . . . . . . . . 9 ((𝜑𝑧𝑅) → ((♯‘({𝑧} ∪ (𝑄 “ {0}))) = (♯‘(𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
11942, 118imbitrid 244 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝑧 ∈ (𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120119necon3ad 2953 . . . . . . 7 ((𝜑𝑧𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (𝑄 “ {0})))
12138, 120mpd 15 . . . . . 6 ((𝜑𝑧𝑅) → ¬ 𝑧 ∈ (𝑄 “ {0}))
122 disjsn 4711 . . . . . 6 (((𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑄 “ {0}))
123121, 122sylibr 234 . . . . 5 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∩ {𝑧}) = ∅)
12426, 123eqtrid 2789 . . . 4 ((𝜑𝑧𝑅) → ({𝑧} ∩ (𝑄 “ {0})) = ∅)
12519adantr 480 . . . 4 ((𝜑𝑧𝑅) → 𝑅 ∈ Fin)
12649adantr 480 . . . . 5 ((𝜑𝑧𝑅) → 𝑅 ⊆ ℂ)
127126sselda 3983 . . . 4 (((𝜑𝑧𝑅) ∧ 𝑥𝑅) → 𝑥 ∈ ℂ)
128124, 77, 125, 127fsumsplit 15777 . . 3 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥))
129 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
130129sumsn 15782 . . . . . 6 ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13150, 50, 130syl2anc 584 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13250negnegd 11611 . . . . 5 ((𝜑𝑧𝑅) → --𝑧 = 𝑧)
133131, 132eqtr4d 2780 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134117, 31eqtrd 2777 . . . . . 6 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) = (deg‘𝑄))
135 fveq2 6906 . . . . . . . . . 10 (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136135eqeq2d 2748 . . . . . . . . 9 (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137 cnveq 5884 . . . . . . . . . . . 12 (𝑓 = 𝑄𝑓 = 𝑄)
138137imaeq1d 6077 . . . . . . . . . . 11 (𝑓 = 𝑄 → (𝑓 “ {0}) = (𝑄 “ {0}))
139138fveq2d 6910 . . . . . . . . . 10 (𝑓 = 𝑄 → (♯‘(𝑓 “ {0})) = (♯‘(𝑄 “ {0})))
140139, 135eqeq12d 2753 . . . . . . . . 9 (𝑓 = 𝑄 → ((♯‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(𝑄 “ {0})) = (deg‘𝑄)))
141136, 140anbi12d 632 . . . . . . . 8 (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄))))
142138sumeq1d 15736 . . . . . . . . 9 (𝑓 = 𝑄 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥 ∈ (𝑄 “ {0})𝑥)
143 fveq2 6906 . . . . . . . . . . . 12 (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144135oveq1d 7446 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145143, 144fveq12d 6913 . . . . . . . . . . 11 (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146143, 135fveq12d 6913 . . . . . . . . . . 11 (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147145, 146oveq12d 7449 . . . . . . . . . 10 (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148147negeqd 11502 . . . . . . . . 9 (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149142, 148eqeq12d 2753 . . . . . . . 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 480 . . . . . . 7 ((𝜑𝑧𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
152150, 151, 32rspcdva 3623 . . . . . 6 ((𝜑𝑧𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
15331, 134, 152mp2and 699 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
15431fvoveq1d 7453 . . . . . . 7 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
15561fveq2d 6910 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (coeff‘𝐹) = (coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15627, 155eqtrid 2789 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐴 = (coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15761fveq2d 6910 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘𝐹) = (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15867simp2d 1144 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (deg‘(Xpf − (ℂ × {𝑧}))) = 1)
159 ax-1ne0 11224 . . . . . . . . . . . . . . 15 1 ≠ 0
160159a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 1 ≠ 0)
161158, 160eqnetrd 3008 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (deg‘(Xpf − (ℂ × {𝑧}))) ≠ 0)
162 fveq2 6906 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xpf − (ℂ × {𝑧}))) = (deg‘0𝑝))
163162, 12eqtrdi 2793 . . . . . . . . . . . . . 14 ((Xpf − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xpf − (ℂ × {𝑧}))) = 0)
164163necon3i 2973 . . . . . . . . . . . . 13 ((deg‘(Xpf − (ℂ × {𝑧}))) ≠ 0 → (Xpf − (ℂ × {𝑧})) ≠ 0𝑝)
165161, 164syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})) ≠ 0𝑝)
166 eqid 2737 . . . . . . . . . . . . 13 (deg‘(Xpf − (ℂ × {𝑧}))) = (deg‘(Xpf − (ℂ × {𝑧})))
167 eqid 2737 . . . . . . . . . . . . 13 (deg‘𝑄) = (deg‘𝑄)
168166, 167dgrmul 26310 . . . . . . . . . . . 12 ((((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xpf − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
16968, 165, 32, 90, 168syl22anc 839 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
170157, 169eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝐹) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
1719, 170eqtrid 2789 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝑁 = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
172156, 171fveq12d 6913 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))))
173 eqid 2737 . . . . . . . . . 10 (coeff‘(Xpf − (ℂ × {𝑧}))) = (coeff‘(Xpf − (ℂ × {𝑧})))
174 eqid 2737 . . . . . . . . . 10 (coeff‘𝑄) = (coeff‘𝑄)
175173, 174, 166, 167coemulhi 26293 . . . . . . . . 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 6910 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘1))
178 ssid 4006 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
179 plyid 26248 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180178, 100, 179mp2an 692 . . . . . . . . . . . . . 14 Xp ∈ (Poly‘ℂ)
181 plyconst 26245 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182178, 50, 181sylancr 587 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183 eqid 2737 . . . . . . . . . . . . . . 15 (coeff‘Xp) = (coeff‘Xp)
184 eqid 2737 . . . . . . . . . . . . . . 15 (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185183, 184coesub 26296 . . . . . . . . . . . . . 14 ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xpf − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
186180, 182, 185sylancr 587 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (coeff‘(Xpf − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
187186fveq1d 6908 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188 1nn0 12542 . . . . . . . . . . . . . 14 1 ∈ ℕ0
189183coef3 26271 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190 ffn 6736 . . . . . . . . . . . . . . . . 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 26271 . . . . . . . . . . . . . . . 16 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194 ffn 6736 . . . . . . . . . . . . . . . 16 ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195182, 193, 1943syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196 nn0ex 12532 . . . . . . . . . . . . . . . 16 0 ∈ V
197196a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ℕ0 ∈ V)
198 inidm 4227 . . . . . . . . . . . . . . 15 (ℕ0 ∩ ℕ0) = ℕ0
199 coeidp 26303 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
200199adantl 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
201 eqid 2737 . . . . . . . . . . . . . . . . 17 1 = 1
202201iftruei 4532 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
203200, 202eqtrdi 2793 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204 0lt1 11785 . . . . . . . . . . . . . . . . . 18 0 < 1
205 0re 11263 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
206 1re 11261 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
207205, 206ltnlei 11382 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ ¬ 1 ≤ 0)
208204, 207mpbi 230 . . . . . . . . . . . . . . . . 17 ¬ 1 ≤ 0
20950adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210 0dgr 26284 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212211breq2d 5155 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213208, 212mtbiri 327 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215184, 214dgrub 26273 . . . . . . . . . . . . . . . . . . 19 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
2162153expia 1122 . . . . . . . . . . . . . . . . . 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 7708 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
221188, 220mpan2 691 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222 1m0e1 12387 . . . . . . . . . . . . 13 (1 − 0) = 1
223221, 222eqtrdi 2793 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224187, 223eqtrd 2777 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘1) = 1)
225177, 224eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) = 1)
226225oveq1d 7446 . . . . . . . . 9 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227174coef3 26271 . . . . . . . . . . . 12 (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
22832, 227syl 17 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229228, 34ffvelcdmd 7105 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230229mullidd 11279 . . . . . . . . 9 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231226, 230eqtrd 2777 . . . . . . . 8 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232172, 176, 2313eqtrd 2781 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233154, 232oveq12d 7449 . . . . . 6 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234233negeqd 11502 . . . . 5 ((𝜑𝑧𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235153, 234eqtr4d 2780 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)))
236133, 235oveq12d 7449 . . 3 ((𝜑𝑧𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
23750negcld 11607 . . . . 5 ((𝜑𝑧𝑅) → -𝑧 ∈ ℂ)
238 nnm1nn0 12567 . . . . . . . . 9 (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
2393, 238syl 17 . . . . . . . 8 (𝜑 → (𝐷 − 1) ∈ ℕ0)
240239adantr 480 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 − 1) ∈ ℕ0)
241228, 240ffvelcdmd 7105 . . . . . 6 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242232, 229eqeltrd 2841 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ∈ ℂ)
2439, 27dgreq0 26305 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
24443, 243syl 17 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
245244necon3bid 2985 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴𝑁) ≠ 0))
24682, 245mpbid 232 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ≠ 0)
247241, 242, 246divcld 12043 . . . . 5 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) ∈ ℂ)
248237, 247negdid 11633 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
249237, 242mulcld 11281 . . . . . . 7 ((𝜑𝑧𝑅) → (-𝑧 · (𝐴𝑁)) ∈ ℂ)
250249, 241, 242, 246divdird 12081 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
251 nnm1nn0 12567 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
2525, 251syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
253252adantr 480 . . . . . . . . 9 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ0)
254173, 174coemul 26291 . . . . . . . . 9 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
25568, 32, 253, 254syl3anc 1373 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256156fveq1d 6908 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257 1e0p1 12775 . . . . . . . . . . . 12 1 = (0 + 1)
258257oveq2i 7442 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
259258sumeq1i 15733 . . . . . . . . . 10 Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260 0nn0 12541 . . . . . . . . . . . . 13 0 ∈ ℕ0
261 nn0uz 12920 . . . . . . . . . . . . 13 0 = (ℤ‘0)
262260, 261eleqtri 2839 . . . . . . . . . . . 12 0 ∈ (ℤ‘0)
263262a1i 11 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 0 ∈ (ℤ‘0))
264258eleq2i 2833 . . . . . . . . . . . 12 (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265173coef3 26271 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ)
26668, 265syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267 elfznn0 13660 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268 ffvelcdm 7101 . . . . . . . . . . . . . 14 (((coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269266, 267, 268syl2an 596 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
2702oveq1d 7446 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271 pncan 11514 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272101, 100, 271sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273270, 272eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) = 𝐷)
274273adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝑁 − 1) = 𝐷)
2753adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐷 ∈ ℕ)
276274, 275eqeltrd 2841 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ)
277 nnuz 12921 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
278276, 277eleqtrdi 2851 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ (ℤ‘1))
279 fzss2 13604 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ (ℤ‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280278, 279syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281280sselda 3983 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282 fznn0sub 13596 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283 ffvelcdm 7101 . . . . . . . . . . . . . . 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 11281 . . . . . . . . . . . 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 2795 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → 𝑘 = 1)
290289fveq2d 6910 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘1))
291289oveq2d 7447 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292291fveq2d 6910 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293290, 292oveq12d 7449 . . . . . . . . . . 11 (𝑘 = (0 + 1) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294263, 287, 293fsump1 15792 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
295259, 294eqtrid 2789 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296 eldifn 4132 . . . . . . . . . . . . . 14 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297296adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298 eldifi 4131 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299 elfznn0 13660 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300298, 299syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301173, 166dgrub 26273 . . . . . . . . . . . . . . . . 17 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))))
3023013expia 1122 . . . . . . . . . . . . . . . 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 13560 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ‘0))
305298, 304syl 17 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ‘0))
306305adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ‘0))
307 1z 12647 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
308 elfz5 13556 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309306, 307, 308sylancl 586 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310158breq2d 5155 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
311310adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
312309, 311bitr4d 282 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
313303, 312sylibrd 259 . . . . . . . . . . . . . 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 7446 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
317298, 284sylan2 593 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
318317mul02d 11459 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319316, 318eqtrd 2777 . . . . . . . . . 10 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320 fzfid 14014 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321280, 286, 319, 320fsumss 15761 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322 0z 12624 . . . . . . . . . . . 12 0 ∈ ℤ
323186fveq1d 6908 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324 coeidp 26303 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325159nesymi 2998 . . . . . . . . . . . . . . . . . . . . 21 ¬ 0 = 1
326325iffalsei 4535 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
327324, 326eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328327adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329184coefv0 26287 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
330182, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
331 0cn 11253 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℂ
332 vex 3484 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
333332fvconst2 7224 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
334331, 333ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℂ × {𝑧})‘0) = 𝑧
335330, 334eqtr3di 2792 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336335adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337192, 195, 197, 197, 198, 328, 336ofval 7708 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338260, 337mpan2 691 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339 df-neg 11495 . . . . . . . . . . . . . . . 16 -𝑧 = (0 − 𝑧)
340338, 339eqtr4di 2795 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341323, 340eqtrd 2777 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘0) = -𝑧)
342274oveq1d 7446 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343102subid1d 11609 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝐷 − 0) = 𝐷)
344342, 343, 313eqtrd 2781 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345344fveq2d 6910 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346345, 232eqtr4d 2780 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴𝑁))
347341, 346oveq12d 7449 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴𝑁)))
348347, 249eqeltrd 2841 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349 fveq2 6906 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘0))
350 oveq2 7439 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351350fveq2d 6910 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352349, 351oveq12d 7449 . . . . . . . . . . . . 13 (𝑘 = 0 → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353352fsum1 15783 . . . . . . . . . . . 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 2777 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴𝑁)))
356274fvoveq1d 7453 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357224, 356oveq12d 7449 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358241mullidd 11279 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359357, 358eqtrd 2777 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360355, 359oveq12d 7449 . . . . . . . . 9 ((𝜑𝑧𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361295, 321, 3603eqtr3rd 2786 . . . . . . . 8 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362255, 256, 3613eqtr4rd 2788 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363362oveq1d 7446 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
364237, 242, 246divcan4d 12049 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) = -𝑧)
365364oveq1d 7446 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
366250, 363, 3653eqtr3rd 2786 . . . . 5 ((𝜑𝑧𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
367366negeqd 11502 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
368248, 367eqtr3d 2779 . . 3 ((𝜑𝑧𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
369128, 236, 3683eqtrd 2781 . 2 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
37025, 369exlimddv 1935 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wex 1779  wcel 2108  wne 2940  wral 3061  Vcvv 3480  cdif 3948  cun 3949  cin 3950  wss 3951  c0 4333  ifcif 4525  {csn 4626   class class class wbr 5143   × cxp 5683  ccnv 5684  dom cdm 5685  cima 5688   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  f cof 7695  Fincfn 8985  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160   < clt 11295  cle 11296  cmin 11492  -cneg 11493   / cdiv 11920  cn 12266  0cn0 12526  cz 12613  cuz 12878  ...cfz 13547  chash 14369  Σcsu 15722  0𝑝c0p 25704  Polycply 26223  Xpcidp 26224  coeffccoe 26225  degcdgr 26226   quot cquot 26332
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-map 8868  df-pm 8869  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-rp 13035  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-rlim 15525  df-sum 15723  df-0p 25705  df-ply 26227  df-idp 26228  df-coe 26229  df-dgr 26230  df-quot 26333
This theorem is referenced by:  vieta1  26354
  Copyright terms: Public domain W3C validator