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

Theorem vieta1lem2 24913
Description: Lemma for vieta1 24914: 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 11651 . . . . . . 7 (𝜑 → (𝐷 + 1) ∈ ℕ)
52, 4eqeltrrd 2917 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnne0d 11684 . . . . 5 (𝜑𝑁 ≠ 0)
71, 6eqnetrd 3081 . . . 4 (𝜑 → (♯‘𝑅) ≠ 0)
8 vieta1.4 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘𝑆))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (deg‘𝐹)
109, 6eqnetrrid 3089 . . . . . . . . 9 (𝜑 → (deg‘𝐹) ≠ 0)
11 fveq2 6661 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 24865 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12syl6eq 2875 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
1413necon3i 3046 . . . . . . . . 9 ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
1510, 14syl 17 . . . . . . . 8 (𝜑𝐹 ≠ 0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
1716fta1 24910 . . . . . . . 8 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
188, 15, 17syl2anc 587 . . . . . . 7 (𝜑 → (𝑅 ∈ Fin ∧ (♯‘𝑅) ≤ (deg‘𝐹)))
1918simpld 498 . . . . . 6 (𝜑𝑅 ∈ Fin)
20 hasheq0 13729 . . . . . 6 (𝑅 ∈ Fin → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
2119, 20syl 17 . . . . 5 (𝜑 → ((♯‘𝑅) = 0 ↔ 𝑅 = ∅))
2221necon3bid 3058 . . . 4 (𝜑 → ((♯‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
237, 22mpbid 235 . . 3 (𝜑𝑅 ≠ ∅)
24 n0 4293 . . 3 (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧𝑅)
2523, 24sylib 221 . 2 (𝜑 → ∃𝑧 𝑧𝑅)
26 incom 4163 . . . . 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 24912 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
3130simprd 499 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐷 = (deg‘𝑄))
3230simpld 498 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝑄 ∈ (Poly‘ℂ))
33 dgrcl 24836 . . . . . . . . . . 11 (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
3432, 33syl 17 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℕ0)
3534nn0red 11953 . . . . . . . . 9 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℝ)
3631, 35eqeltrd 2916 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 ∈ ℝ)
3736ltp1d 11568 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 < (𝐷 + 1))
3836, 37gtned 10773 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 + 1) ≠ 𝐷)
39 snssi 4725 . . . . . . . . . . 11 (𝑧 ∈ (𝑄 “ {0}) → {𝑧} ⊆ (𝑄 “ {0}))
40 ssequn1 4142 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑄 “ {0}) ↔ ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4139, 40sylib 221 . . . . . . . . . 10 (𝑧 ∈ (𝑄 “ {0}) → ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4241fveq2d 6665 . . . . . . . . 9 (𝑧 ∈ (𝑄 “ {0}) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (♯‘(𝑄 “ {0})))
438adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘𝑆))
44 cnvimass 5936 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 “ {0}) ⊆ dom 𝐹
4516, 44eqsstri 3987 . . . . . . . . . . . . . . . . . . . 20 𝑅 ⊆ dom 𝐹
46 plyf 24801 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47 fdm 6511 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝐹 = ℂ)
4945, 48sseqtrid 4005 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑅 ⊆ ℂ)
5049sselda 3953 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝑧 ∈ ℂ)
5116eleq2i 2907 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑅𝑧 ∈ (𝐹 “ {0}))
52 ffn 6503 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53 fniniseg 6821 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℂ → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5551, 54syl5bb 286 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5655simplbda 503 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝐹𝑧) = 0)
57 eqid 2824 . . . . . . . . . . . . . . . . . . 19 (Xpf − (ℂ × {𝑧})) = (Xpf − (ℂ × {𝑧}))
5857facth 24908 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧})))))
5943, 50, 56, 58syl3anc 1368 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧})))))
6029oveq2i 7160 . . . . . . . . . . . . . . . . 17 ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = ((Xpf − (ℂ × {𝑧})) ∘f · (𝐹 quot (Xpf − (ℂ × {𝑧}))))
6159, 60syl6eqr 2877 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))
6261cnveqd 5733 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐹 = ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))
6362imaeq1d 5915 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝐹 “ {0}) = (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
6416, 63syl5eq 2871 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 𝑅 = (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}))
65 cnex 10616 . . . . . . . . . . . . . 14 ℂ ∈ V
6657plyremlem 24906 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℂ → ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xpf − (ℂ × {𝑧}))) = 1 ∧ ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6750, 66syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xpf − (ℂ × {𝑧}))) = 1 ∧ ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6867simp1d 1139 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
69 plyf 24801 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ)
71 plyf 24801 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
7232, 71syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄:ℂ⟶ℂ)
73 ofmulrt 24884 . . . . . . . . . . . . . 14 ((ℂ ∈ V ∧ (Xpf − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7465, 70, 72, 73mp3an2i 1463 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) “ {0}) = (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7567simp3d 1141 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) “ {0}) = {𝑧})
7675uneq1d 4124 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})) = ({𝑧} ∪ (𝑄 “ {0})))
7764, 74, 763eqtrd 2863 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → 𝑅 = ({𝑧} ∪ (𝑄 “ {0})))
7877fveq2d 6665 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘𝑅) = (♯‘({𝑧} ∪ (𝑄 “ {0}))))
791, 2eqtr4d 2862 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑅) = (𝐷 + 1))
8079adantr 484 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘𝑅) = (𝐷 + 1))
8178, 80eqtr3d 2861 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (𝐷 + 1))
8215adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ≠ 0𝑝)
8361, 82eqnetrrd 3082 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝)
84 plymul0or 24883 . . . . . . . . . . . . . . . . . . 19 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8568, 32, 84syl2anc 587 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) = 0𝑝 ↔ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8685necon3abid 3050 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (((Xpf − (ℂ × {𝑧})) ∘f · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8783, 86mpbid 235 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
88 neanior 3106 . . . . . . . . . . . . . . . 16 (((Xpf − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝) ↔ ¬ ((Xpf − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
8987, 88sylibr 237 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((Xpf − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝))
9089simprd 499 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄 ≠ 0𝑝)
91 eqid 2824 . . . . . . . . . . . . . . 15 (𝑄 “ {0}) = (𝑄 “ {0})
9291fta1 24910 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((𝑄 “ {0}) ∈ Fin ∧ (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9332, 90, 92syl2anc 587 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∈ Fin ∧ (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9493simprd 499 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ≤ (deg‘𝑄))
9594, 31breqtrrd 5080 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ≤ 𝐷)
96 snfi 8590 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9793simpld 498 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝑄 “ {0}) ∈ Fin)
98 hashun2 13749 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (𝑄 “ {0}) ∈ Fin) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))))
9996, 97, 98sylancr 590 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))))
100 ax-1cn 10593 . . . . . . . . . . . . . . 15 1 ∈ ℂ
1013nncnd 11650 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
102101adantr 484 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐷 ∈ ℂ)
103 addcom 10824 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
104100, 102, 103sylancr 590 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (1 + 𝐷) = (𝐷 + 1))
10581, 104eqtr4d 2862 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘({𝑧} ∪ (𝑄 “ {0}))) = (1 + 𝐷))
106 hashsng 13735 . . . . . . . . . . . . . . 15 (𝑧𝑅 → (♯‘{𝑧}) = 1)
107106adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (♯‘{𝑧}) = 1)
108107oveq1d 7164 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((♯‘{𝑧}) + (♯‘(𝑄 “ {0}))) = (1 + (♯‘(𝑄 “ {0}))))
10999, 105, 1083brtr3d 5083 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (1 + 𝐷) ≤ (1 + (♯‘(𝑄 “ {0}))))
110 hashcl 13722 . . . . . . . . . . . . . . 15 ((𝑄 “ {0}) ∈ Fin → (♯‘(𝑄 “ {0})) ∈ ℕ0)
11197, 110syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ∈ ℕ0)
112111nn0red 11953 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) ∈ ℝ)
113 1red 10640 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 1 ∈ ℝ)
11436, 112, 113leadd2d 11233 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (𝐷 ≤ (♯‘(𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (♯‘(𝑄 “ {0})))))
115109, 114mpbird 260 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝐷 ≤ (♯‘(𝑄 “ {0})))
116112, 36letri3d 10780 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((♯‘(𝑄 “ {0})) = 𝐷 ↔ ((♯‘(𝑄 “ {0})) ≤ 𝐷𝐷 ≤ (♯‘(𝑄 “ {0})))))
11795, 115, 116mpbir2and 712 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) = 𝐷)
11881, 117eqeq12d 2840 . . . . . . . . 9 ((𝜑𝑧𝑅) → ((♯‘({𝑧} ∪ (𝑄 “ {0}))) = (♯‘(𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
11942, 118syl5ib 247 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝑧 ∈ (𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
120119necon3ad 3027 . . . . . . 7 ((𝜑𝑧𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (𝑄 “ {0})))
12138, 120mpd 15 . . . . . 6 ((𝜑𝑧𝑅) → ¬ 𝑧 ∈ (𝑄 “ {0}))
122 disjsn 4632 . . . . . 6 (((𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑄 “ {0}))
123121, 122sylibr 237 . . . . 5 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∩ {𝑧}) = ∅)
12426, 123syl5eq 2871 . . . 4 ((𝜑𝑧𝑅) → ({𝑧} ∩ (𝑄 “ {0})) = ∅)
12519adantr 484 . . . 4 ((𝜑𝑧𝑅) → 𝑅 ∈ Fin)
12649adantr 484 . . . . 5 ((𝜑𝑧𝑅) → 𝑅 ⊆ ℂ)
127126sselda 3953 . . . 4 (((𝜑𝑧𝑅) ∧ 𝑥𝑅) → 𝑥 ∈ ℂ)
128124, 77, 125, 127fsumsplit 15097 . . 3 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥))
129 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
130129sumsn 15101 . . . . . 6 ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13150, 50, 130syl2anc 587 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13250negnegd 10986 . . . . 5 ((𝜑𝑧𝑅) → --𝑧 = 𝑧)
133131, 132eqtr4d 2862 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
134117, 31eqtrd 2859 . . . . . 6 ((𝜑𝑧𝑅) → (♯‘(𝑄 “ {0})) = (deg‘𝑄))
135 fveq2 6661 . . . . . . . . . 10 (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
136135eqeq2d 2835 . . . . . . . . 9 (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
137 cnveq 5731 . . . . . . . . . . . 12 (𝑓 = 𝑄𝑓 = 𝑄)
138137imaeq1d 5915 . . . . . . . . . . 11 (𝑓 = 𝑄 → (𝑓 “ {0}) = (𝑄 “ {0}))
139138fveq2d 6665 . . . . . . . . . 10 (𝑓 = 𝑄 → (♯‘(𝑓 “ {0})) = (♯‘(𝑄 “ {0})))
140139, 135eqeq12d 2840 . . . . . . . . 9 (𝑓 = 𝑄 → ((♯‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (♯‘(𝑄 “ {0})) = (deg‘𝑄)))
141136, 140anbi12d 633 . . . . . . . 8 (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄))))
142138sumeq1d 15058 . . . . . . . . 9 (𝑓 = 𝑄 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥 ∈ (𝑄 “ {0})𝑥)
143 fveq2 6661 . . . . . . . . . . . 12 (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
144135oveq1d 7164 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
145143, 144fveq12d 6668 . . . . . . . . . . 11 (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
146143, 135fveq12d 6668 . . . . . . . . . . 11 (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
147145, 146oveq12d 7167 . . . . . . . . . 10 (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
148147negeqd 10878 . . . . . . . . 9 (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
149142, 148eqeq12d 2840 . . . . . . . 8 (𝑓 = 𝑄 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
150141, 149imbi12d 348 . . . . . . 7 (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
15128adantr 484 . . . . . . 7 ((𝜑𝑧𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (♯‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
152150, 151, 32rspcdva 3611 . . . . . 6 ((𝜑𝑧𝑅) → ((𝐷 = (deg‘𝑄) ∧ (♯‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
15331, 134, 152mp2and 698 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
15431fvoveq1d 7171 . . . . . . 7 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
15561fveq2d 6665 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (coeff‘𝐹) = (coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15627, 155syl5eq 2871 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐴 = (coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15761fveq2d 6665 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘𝐹) = (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)))
15867simp2d 1140 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (deg‘(Xpf − (ℂ × {𝑧}))) = 1)
159 ax-1ne0 10604 . . . . . . . . . . . . . . 15 1 ≠ 0
160159a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 1 ≠ 0)
161158, 160eqnetrd 3081 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (deg‘(Xpf − (ℂ × {𝑧}))) ≠ 0)
162 fveq2 6661 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xpf − (ℂ × {𝑧}))) = (deg‘0𝑝))
163162, 12syl6eq 2875 . . . . . . . . . . . . . 14 ((Xpf − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xpf − (ℂ × {𝑧}))) = 0)
164163necon3i 3046 . . . . . . . . . . . . 13 ((deg‘(Xpf − (ℂ × {𝑧}))) ≠ 0 → (Xpf − (ℂ × {𝑧})) ≠ 0𝑝)
165161, 164syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (Xpf − (ℂ × {𝑧})) ≠ 0𝑝)
166 eqid 2824 . . . . . . . . . . . . 13 (deg‘(Xpf − (ℂ × {𝑧}))) = (deg‘(Xpf − (ℂ × {𝑧})))
167 eqid 2824 . . . . . . . . . . . . 13 (deg‘𝑄) = (deg‘𝑄)
168166, 167dgrmul 24873 . . . . . . . . . . . 12 ((((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xpf − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
16968, 165, 32, 90, 168syl22anc 837 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄)) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
170157, 169eqtrd 2859 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝐹) = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
1719, 170syl5eq 2871 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝑁 = ((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄)))
172156, 171fveq12d 6668 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))))
173 eqid 2824 . . . . . . . . . 10 (coeff‘(Xpf − (ℂ × {𝑧}))) = (coeff‘(Xpf − (ℂ × {𝑧})))
174 eqid 2824 . . . . . . . . . 10 (coeff‘𝑄) = (coeff‘𝑄)
175173, 174, 166, 167coemulhi 24857 . . . . . . . . 9 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
17668, 32, 175syl2anc 587 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘((deg‘(Xpf − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
177158fveq2d 6665 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘1))
178 ssid 3975 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
179 plyid 24812 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
180178, 100, 179mp2an 691 . . . . . . . . . . . . . 14 Xp ∈ (Poly‘ℂ)
181 plyconst 24809 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
182178, 50, 181sylancr 590 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
183 eqid 2824 . . . . . . . . . . . . . . 15 (coeff‘Xp) = (coeff‘Xp)
184 eqid 2824 . . . . . . . . . . . . . . 15 (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
185183, 184coesub 24860 . . . . . . . . . . . . . 14 ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xpf − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
186180, 182, 185sylancr 590 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (coeff‘(Xpf − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧}))))
187186fveq1d 6663 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1))
188 1nn0 11910 . . . . . . . . . . . . . 14 1 ∈ ℕ0
189183coef3 24835 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
190 ffn 6503 . . . . . . . . . . . . . . . . 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 24835 . . . . . . . . . . . . . . . 16 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
194 ffn 6503 . . . . . . . . . . . . . . . 16 ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
195182, 193, 1943syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
196 nn0ex 11900 . . . . . . . . . . . . . . . 16 0 ∈ V
197196a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ℕ0 ∈ V)
198 inidm 4180 . . . . . . . . . . . . . . 15 (ℕ0 ∩ ℕ0) = ℕ0
199 coeidp 24866 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
200199adantl 485 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
201 eqid 2824 . . . . . . . . . . . . . . . . 17 1 = 1
202201iftruei 4457 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
203200, 202syl6eq 2875 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
204 0lt1 11160 . . . . . . . . . . . . . . . . . 18 0 < 1
205 0re 10641 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
206 1re 10639 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
207205, 206ltnlei 10759 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ ¬ 1 ≤ 0)
208204, 207mpbi 233 . . . . . . . . . . . . . . . . 17 ¬ 1 ≤ 0
20950adantr 484 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
210 0dgr 24848 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
212211breq2d 5064 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
213208, 212mtbiri 330 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
214 eqid 2824 . . . . . . . . . . . . . . . . . . . 20 (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
215184, 214dgrub 24837 . . . . . . . . . . . . . . . . . . 19 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
2162153expia 1118 . . . . . . . . . . . . . . . . . 18 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
217182, 216sylan 583 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
218217necon1bd 3032 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
219213, 218mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
220192, 195, 197, 197, 198, 203, 219ofval 7412 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
221188, 220mpan2 690 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
222 1m0e1 11755 . . . . . . . . . . . . 13 (1 − 0) = 1
223221, 222syl6eq 2875 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘1) = 1)
224187, 223eqtrd 2859 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘1) = 1)
225177, 224eqtrd 2859 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) = 1)
226225oveq1d 7164 . . . . . . . . 9 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
227174coef3 24835 . . . . . . . . . . . 12 (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
22832, 227syl 17 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
229228, 34ffvelrnd 6843 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
230229mulid2d 10657 . . . . . . . . 9 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
231226, 230eqtrd 2859 . . . . . . . 8 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘(deg‘(Xpf − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
232172, 176, 2313eqtrd 2863 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
233154, 232oveq12d 7167 . . . . . 6 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
234233negeqd 10878 . . . . 5 ((𝜑𝑧𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
235153, 234eqtr4d 2862 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)))
236133, 235oveq12d 7167 . . 3 ((𝜑𝑧𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
23750negcld 10982 . . . . 5 ((𝜑𝑧𝑅) → -𝑧 ∈ ℂ)
238 nnm1nn0 11935 . . . . . . . . 9 (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
2393, 238syl 17 . . . . . . . 8 (𝜑 → (𝐷 − 1) ∈ ℕ0)
240239adantr 484 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 − 1) ∈ ℕ0)
241228, 240ffvelrnd 6843 . . . . . 6 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
242232, 229eqeltrd 2916 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ∈ ℂ)
2439, 27dgreq0 24868 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
24443, 243syl 17 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
245244necon3bid 3058 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴𝑁) ≠ 0))
24682, 245mpbid 235 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ≠ 0)
247241, 242, 246divcld 11414 . . . . 5 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) ∈ ℂ)
248237, 247negdid 11008 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
249237, 242mulcld 10659 . . . . . . 7 ((𝜑𝑧𝑅) → (-𝑧 · (𝐴𝑁)) ∈ ℂ)
250249, 241, 242, 246divdird 11452 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
251 nnm1nn0 11935 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
2525, 251syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
253252adantr 484 . . . . . . . . 9 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ0)
254173, 174coemul 24855 . . . . . . . . 9 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
25568, 32, 253, 254syl3anc 1368 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
256156fveq1d 6663 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xpf − (ℂ × {𝑧})) ∘f · 𝑄))‘(𝑁 − 1)))
257 1e0p1 12137 . . . . . . . . . . . 12 1 = (0 + 1)
258257oveq2i 7160 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
259258sumeq1i 15055 . . . . . . . . . 10 Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
260 0nn0 11909 . . . . . . . . . . . . 13 0 ∈ ℕ0
261 nn0uz 12277 . . . . . . . . . . . . 13 0 = (ℤ‘0)
262260, 261eleqtri 2914 . . . . . . . . . . . 12 0 ∈ (ℤ‘0)
263262a1i 11 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 0 ∈ (ℤ‘0))
264258eleq2i 2907 . . . . . . . . . . . 12 (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
265173coef3 24835 . . . . . . . . . . . . . . 15 ((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ)
26668, 265syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ)
267 elfznn0 13004 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
268 ffvelrn 6840 . . . . . . . . . . . . . 14 (((coeff‘(Xpf − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
269266, 267, 268syl2an 598 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
2702oveq1d 7164 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
271 pncan 10890 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
272101, 100, 271sylancl 589 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
273270, 272eqtr3d 2861 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) = 𝐷)
274273adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝑁 − 1) = 𝐷)
2753adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐷 ∈ ℕ)
276274, 275eqeltrd 2916 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ)
277 nnuz 12278 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
278276, 277eleqtrdi 2926 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ (ℤ‘1))
279 fzss2 12951 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ (ℤ‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
280278, 279syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
281280sselda 3953 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
282 fznn0sub 12943 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
283 ffvelrn 6840 . . . . . . . . . . . . . . 15 (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
284228, 282, 283syl2an 598 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
285281, 284syldan 594 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
286269, 285mulcld 10659 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
287264, 286sylan2br 597 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
288 id 22 . . . . . . . . . . . . . 14 (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
289288, 257syl6eqr 2877 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → 𝑘 = 1)
290289fveq2d 6665 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘1))
291289oveq2d 7165 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
292291fveq2d 6665 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
293290, 292oveq12d 7167 . . . . . . . . . . 11 (𝑘 = (0 + 1) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
294263, 287, 293fsump1 15111 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
295259, 294syl5eq 2871 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
296 eldifn 4090 . . . . . . . . . . . . . 14 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
297296adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
298 eldifi 4089 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
299 elfznn0 13004 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
300298, 299syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
301173, 166dgrub 24837 . . . . . . . . . . . . . . . . 17 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))))
3023013expia 1118 . . . . . . . . . . . . . . . 16 (((Xpf − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
30368, 300, 302syl2an 598 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
304 elfzuz 12907 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ‘0))
305298, 304syl 17 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ‘0))
306305adantl 485 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ‘0))
307 1z 12009 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
308 elfz5 12903 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
309306, 307, 308sylancl 589 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
310158breq2d 5064 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
311310adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
312309, 311bitr4d 285 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xpf − (ℂ × {𝑧})))))
313303, 312sylibrd 262 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
314313necon1bd 3032 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = 0))
315297, 314mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = 0)
316315oveq1d 7164 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
317298, 284sylan2 595 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
318317mul02d 10836 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
319316, 318eqtrd 2859 . . . . . . . . . 10 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
320 fzfid 13345 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (0...(𝑁 − 1)) ∈ Fin)
321280, 286, 319, 320fsumss 15082 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
322 0z 11989 . . . . . . . . . . . 12 0 ∈ ℤ
323186fveq1d 6663 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0))
324 coeidp 24866 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
325159nesymi 3071 . . . . . . . . . . . . . . . . . . . . 21 ¬ 0 = 1
326325iffalsei 4460 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
327324, 326syl6eq 2875 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
328327adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
329 0cn 10631 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℂ
330 vex 3483 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
331330fvconst2 6957 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
332329, 331ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℂ × {𝑧})‘0) = 𝑧
333184coefv0 24851 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
334182, 333syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
335332, 334syl5reqr 2874 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
336335adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
337192, 195, 197, 197, 198, 328, 336ofval 7412 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
338260, 337mpan2 690 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
339 df-neg 10871 . . . . . . . . . . . . . . . 16 -𝑧 = (0 − 𝑧)
340338, 339syl6eqr 2877 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘f − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
341323, 340eqtrd 2859 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘(Xpf − (ℂ × {𝑧})))‘0) = -𝑧)
342274oveq1d 7164 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
343102subid1d 10984 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝐷 − 0) = 𝐷)
344342, 343, 313eqtrd 2863 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
345344fveq2d 6665 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
346345, 232eqtr4d 2862 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴𝑁))
347341, 346oveq12d 7167 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴𝑁)))
348347, 249eqeltrd 2916 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
349 fveq2 6661 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xpf − (ℂ × {𝑧})))‘0))
350 oveq2 7157 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
351350fveq2d 6665 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
352349, 351oveq12d 7167 . . . . . . . . . . . . 13 (𝑘 = 0 → (((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
353352fsum1 15102 . . . . . . . . . . . 12 ((0 ∈ ℤ ∧ (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
354322, 348, 353sylancr 590 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xpf − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
355354, 347eqtrd 2859 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴𝑁)))
356274fvoveq1d 7171 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
357224, 356oveq12d 7167 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
358241mulid2d 10657 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
359357, 358eqtrd 2859 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
360355, 359oveq12d 7167 . . . . . . . . 9 ((𝜑𝑧𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xpf − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
361295, 321, 3603eqtr3rd 2868 . . . . . . . 8 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xpf − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
362255, 256, 3613eqtr4rd 2870 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
363362oveq1d 7164 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
364237, 242, 246divcan4d 11420 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) = -𝑧)
365364oveq1d 7164 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
366250, 363, 3653eqtr3rd 2868 . . . . 5 ((𝜑𝑧𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
367366negeqd 10878 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
368248, 367eqtr3d 2861 . . 3 ((𝜑𝑧𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
369128, 236, 3683eqtrd 2863 . 2 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
37025, 369exlimddv 1937 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wex 1781  wcel 2115  wne 3014  wral 3133  Vcvv 3480  cdif 3916  cun 3917  cin 3918  wss 3919  c0 4276  ifcif 4450  {csn 4550   class class class wbr 5052   × cxp 5540  ccnv 5541  dom cdm 5542  cima 5545   Fn wfn 6338  wf 6339  cfv 6343  (class class class)co 7149  f cof 7401  Fincfn 8505  cc 10533  cr 10534  0cc0 10535  1c1 10536   + caddc 10538   · cmul 10540   < clt 10673  cle 10674  cmin 10868  -cneg 10869   / cdiv 11295  cn 11634  0cn0 11894  cz 11978  cuz 12240  ...cfz 12894  chash 13695  Σcsu 15042  0𝑝c0p 24279  Polycply 24787  Xpcidp 24788  coeffccoe 24789  degcdgr 24790   quot cquot 24892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613  ax-addf 10614
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-of 7403  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8285  df-map 8404  df-pm 8405  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-sup 8903  df-inf 8904  df-oi 8971  df-dju 9327  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-n0 11895  df-xnn0 11965  df-z 11979  df-uz 12241  df-rp 12387  df-fz 12895  df-fzo 13038  df-fl 13166  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-rlim 14846  df-sum 15043  df-0p 24280  df-ply 24791  df-idp 24792  df-coe 24793  df-dgr 24794  df-quot 24893
This theorem is referenced by:  vieta1  24914
  Copyright terms: Public domain W3C validator