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