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

Theorem vieta1lem2 23784
Description: Lemma for vieta1 23785: 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 (Xp𝑓 − (ℂ × {𝑧})))
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 10881 . . . . . . 7 (𝜑 → (𝐷 + 1) ∈ ℕ)
52, 4eqeltrrd 2685 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnne0d 10909 . . . . 5 (𝜑𝑁 ≠ 0)
71, 6eqnetrd 2845 . . . 4 (𝜑 → (#‘𝑅) ≠ 0)
8 vieta1.4 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘𝑆))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (deg‘𝐹)
109, 6syl5eqner 2853 . . . . . . . . 9 (𝜑 → (deg‘𝐹) ≠ 0)
11 fveq2 6085 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 23736 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12syl6eq 2656 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
1413necon3i 2810 . . . . . . . . 9 ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
1510, 14syl 17 . . . . . . . 8 (𝜑𝐹 ≠ 0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
1716fta1 23781 . . . . . . . 8 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
188, 15, 17syl2anc 690 . . . . . . 7 (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
1918simpld 473 . . . . . 6 (𝜑𝑅 ∈ Fin)
20 hasheq0 12964 . . . . . 6 (𝑅 ∈ Fin → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
2119, 20syl 17 . . . . 5 (𝜑 → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
2221necon3bid 2822 . . . 4 (𝜑 → ((#‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
237, 22mpbid 220 . . 3 (𝜑𝑅 ≠ ∅)
24 n0 3886 . . 3 (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧𝑅)
2523, 24sylib 206 . 2 (𝜑 → ∃𝑧 𝑧𝑅)
26 incom 3763 . . . . 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 (Xp𝑓 − (ℂ × {𝑧})))
3027, 9, 16, 8, 1, 3, 2, 28, 29vieta1lem1 23783 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
3130simprd 477 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐷 = (deg‘𝑄))
3230simpld 473 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝑄 ∈ (Poly‘ℂ))
33 dgrcl 23707 . . . . . . . . . . 11 (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
3432, 33syl 17 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℕ0)
3534nn0red 11196 . . . . . . . . 9 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℝ)
3631, 35eqeltrd 2684 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 ∈ ℝ)
3736ltp1d 10800 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 < (𝐷 + 1))
3836, 37gtned 10020 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 + 1) ≠ 𝐷)
39 snssi 4276 . . . . . . . . . . 11 (𝑧 ∈ (𝑄 “ {0}) → {𝑧} ⊆ (𝑄 “ {0}))
40 ssequn1 3741 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑄 “ {0}) ↔ ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4139, 40sylib 206 . . . . . . . . . 10 (𝑧 ∈ (𝑄 “ {0}) → ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4241fveq2d 6089 . . . . . . . . 9 (𝑧 ∈ (𝑄 “ {0}) → (#‘({𝑧} ∪ (𝑄 “ {0}))) = (#‘(𝑄 “ {0})))
438adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘𝑆))
44 cnvimass 5388 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 “ {0}) ⊆ dom 𝐹
4516, 44eqsstri 3594 . . . . . . . . . . . . . . . . . . . 20 𝑅 ⊆ dom 𝐹
46 plyf 23672 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47 fdm 5947 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝐹 = ℂ)
4945, 48syl5sseq 3612 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑅 ⊆ ℂ)
5049sselda 3564 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝑧 ∈ ℂ)
5116eleq2i 2676 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑅𝑧 ∈ (𝐹 “ {0}))
52 ffn 5941 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53 fniniseg 6228 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℂ → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5551, 54syl5bb 270 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5655simplbda 651 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝐹𝑧) = 0)
57 eqid 2606 . . . . . . . . . . . . . . . . . . 19 (Xp𝑓 − (ℂ × {𝑧})) = (Xp𝑓 − (ℂ × {𝑧}))
5857facth 23779 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))))
5943, 50, 56, 58syl3anc 1317 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))))
6029oveq2i 6535 . . . . . . . . . . . . . . . . 17 ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧}))))
6159, 60syl6eqr 2658 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))
6261cnveqd 5205 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))
6362imaeq1d 5368 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝐹 “ {0}) = (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}))
6416, 63syl5eq 2652 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 𝑅 = (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}))
65 cnex 9870 . . . . . . . . . . . . . . 15 ℂ ∈ V
6665a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ℂ ∈ V)
6757plyremlem 23777 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℂ → ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6850, 67syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6968simp1d 1065 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
70 plyf 23672 . . . . . . . . . . . . . . 15 ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
7169, 70syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
72 plyf 23672 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
7332, 72syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄:ℂ⟶ℂ)
74 ofmulrt 23755 . . . . . . . . . . . . . 14 ((ℂ ∈ V ∧ (Xp𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}) = (((Xp𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7566, 71, 73, 74syl3anc 1317 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}) = (((Xp𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7668simp3d 1067 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})
7776uneq1d 3724 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})) = ({𝑧} ∪ (𝑄 “ {0})))
7864, 75, 773eqtrd 2644 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → 𝑅 = ({𝑧} ∪ (𝑄 “ {0})))
7978fveq2d 6089 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (#‘𝑅) = (#‘({𝑧} ∪ (𝑄 “ {0}))))
801, 2eqtr4d 2643 . . . . . . . . . . . 12 (𝜑 → (#‘𝑅) = (𝐷 + 1))
8180adantr 479 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (#‘𝑅) = (𝐷 + 1))
8279, 81eqtr3d 2642 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (#‘({𝑧} ∪ (𝑄 “ {0}))) = (𝐷 + 1))
8315adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ≠ 0𝑝)
8461, 83eqnetrrd 2846 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) ≠ 0𝑝)
85 plymul0or 23754 . . . . . . . . . . . . . . . . . . 19 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = 0𝑝 ↔ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8669, 32, 85syl2anc 690 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = 0𝑝 ↔ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8786necon3abid 2814 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8884, 87mpbid 220 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
89 neanior 2870 . . . . . . . . . . . . . . . 16 (((Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝) ↔ ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
9088, 89sylibr 222 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝))
9190simprd 477 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄 ≠ 0𝑝)
92 eqid 2606 . . . . . . . . . . . . . . 15 (𝑄 “ {0}) = (𝑄 “ {0})
9392fta1 23781 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((𝑄 “ {0}) ∈ Fin ∧ (#‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9432, 91, 93syl2anc 690 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∈ Fin ∧ (#‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9594simprd 477 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ≤ (deg‘𝑄))
9695, 31breqtrrd 4602 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ≤ 𝐷)
97 snfi 7897 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9894simpld 473 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝑄 “ {0}) ∈ Fin)
99 hashun2 12982 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (𝑄 “ {0}) ∈ Fin) → (#‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(𝑄 “ {0}))))
10097, 98, 99sylancr 693 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (#‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(𝑄 “ {0}))))
101 ax-1cn 9847 . . . . . . . . . . . . . . 15 1 ∈ ℂ
1023nncnd 10880 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
103102adantr 479 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐷 ∈ ℂ)
104 addcom 10070 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
105101, 103, 104sylancr 693 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (1 + 𝐷) = (𝐷 + 1))
10682, 105eqtr4d 2643 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (#‘({𝑧} ∪ (𝑄 “ {0}))) = (1 + 𝐷))
107 hashsng 12969 . . . . . . . . . . . . . . 15 (𝑧𝑅 → (#‘{𝑧}) = 1)
108107adantl 480 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (#‘{𝑧}) = 1)
109108oveq1d 6539 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((#‘{𝑧}) + (#‘(𝑄 “ {0}))) = (1 + (#‘(𝑄 “ {0}))))
110100, 106, 1093brtr3d 4605 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (1 + 𝐷) ≤ (1 + (#‘(𝑄 “ {0}))))
111 hashcl 12958 . . . . . . . . . . . . . . 15 ((𝑄 “ {0}) ∈ Fin → (#‘(𝑄 “ {0})) ∈ ℕ0)
11298, 111syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ∈ ℕ0)
113112nn0red 11196 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ∈ ℝ)
114 1red 9908 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 1 ∈ ℝ)
11536, 113, 114leadd2d 10468 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (𝐷 ≤ (#‘(𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (#‘(𝑄 “ {0})))))
116110, 115mpbird 245 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝐷 ≤ (#‘(𝑄 “ {0})))
117113, 36letri3d 10027 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((#‘(𝑄 “ {0})) = 𝐷 ↔ ((#‘(𝑄 “ {0})) ≤ 𝐷𝐷 ≤ (#‘(𝑄 “ {0})))))
11896, 116, 117mpbir2and 958 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) = 𝐷)
11982, 118eqeq12d 2621 . . . . . . . . 9 ((𝜑𝑧𝑅) → ((#‘({𝑧} ∪ (𝑄 “ {0}))) = (#‘(𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
12042, 119syl5ib 232 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝑧 ∈ (𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
121120necon3ad 2791 . . . . . . 7 ((𝜑𝑧𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (𝑄 “ {0})))
12238, 121mpd 15 . . . . . 6 ((𝜑𝑧𝑅) → ¬ 𝑧 ∈ (𝑄 “ {0}))
123 disjsn 4188 . . . . . 6 (((𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑄 “ {0}))
124122, 123sylibr 222 . . . . 5 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∩ {𝑧}) = ∅)
12526, 124syl5eq 2652 . . . 4 ((𝜑𝑧𝑅) → ({𝑧} ∩ (𝑄 “ {0})) = ∅)
12619adantr 479 . . . 4 ((𝜑𝑧𝑅) → 𝑅 ∈ Fin)
12749adantr 479 . . . . 5 ((𝜑𝑧𝑅) → 𝑅 ⊆ ℂ)
128127sselda 3564 . . . 4 (((𝜑𝑧𝑅) ∧ 𝑥𝑅) → 𝑥 ∈ ℂ)
129125, 78, 126, 128fsumsplit 14261 . . 3 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥))
130 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
131130sumsn 14262 . . . . . 6 ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13250, 50, 131syl2anc 690 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13350negnegd 10231 . . . . 5 ((𝜑𝑧𝑅) → --𝑧 = 𝑧)
134132, 133eqtr4d 2643 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
135118, 31eqtrd 2640 . . . . . 6 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) = (deg‘𝑄))
13628adantr 479 . . . . . . 7 ((𝜑𝑧𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
137 fveq2 6085 . . . . . . . . . . 11 (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
138137eqeq2d 2616 . . . . . . . . . 10 (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
139 cnveq 5203 . . . . . . . . . . . . 13 (𝑓 = 𝑄𝑓 = 𝑄)
140139imaeq1d 5368 . . . . . . . . . . . 12 (𝑓 = 𝑄 → (𝑓 “ {0}) = (𝑄 “ {0}))
141140fveq2d 6089 . . . . . . . . . . 11 (𝑓 = 𝑄 → (#‘(𝑓 “ {0})) = (#‘(𝑄 “ {0})))
142141, 137eqeq12d 2621 . . . . . . . . . 10 (𝑓 = 𝑄 → ((#‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (#‘(𝑄 “ {0})) = (deg‘𝑄)))
143138, 142anbi12d 742 . . . . . . . . 9 (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄))))
144140sumeq1d 14222 . . . . . . . . . 10 (𝑓 = 𝑄 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥 ∈ (𝑄 “ {0})𝑥)
145 fveq2 6085 . . . . . . . . . . . . 13 (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
146137oveq1d 6539 . . . . . . . . . . . . 13 (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
147145, 146fveq12d 6091 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
148145, 137fveq12d 6091 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
149147, 148oveq12d 6542 . . . . . . . . . . 11 (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
150149negeqd 10123 . . . . . . . . . 10 (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
151144, 150eqeq12d 2621 . . . . . . . . 9 (𝑓 = 𝑄 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
152143, 151imbi12d 332 . . . . . . . 8 (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
153152rspcv 3274 . . . . . . 7 (𝑄 ∈ (Poly‘ℂ) → (∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ((𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
15432, 136, 153sylc 62 . . . . . 6 ((𝜑𝑧𝑅) → ((𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
15531, 135, 154mp2and 710 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
15631oveq1d 6539 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐷 − 1) = ((deg‘𝑄) − 1))
157156fveq2d 6089 . . . . . . 7 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
15861fveq2d 6089 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (coeff‘𝐹) = (coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
15927, 158syl5eq 2652 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐴 = (coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
16061fveq2d 6089 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘𝐹) = (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
16168simp2d 1066 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1)
162 ax-1ne0 9858 . . . . . . . . . . . . . . 15 1 ≠ 0
163162a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 1 ≠ 0)
164161, 163eqnetrd 2845 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ≠ 0)
165 fveq2 6085 . . . . . . . . . . . . . . 15 ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = (deg‘0𝑝))
166165, 12syl6eq 2656 . . . . . . . . . . . . . 14 ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 0)
167166necon3i 2810 . . . . . . . . . . . . 13 ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) ≠ 0 → (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝)
168164, 167syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝)
169 eqid 2606 . . . . . . . . . . . . 13 (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = (deg‘(Xp𝑓 − (ℂ × {𝑧})))
170 eqid 2606 . . . . . . . . . . . . 13 (deg‘𝑄) = (deg‘𝑄)
171169, 170dgrmul 23744 . . . . . . . . . . . 12 ((((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
17269, 168, 32, 91, 171syl22anc 1318 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
173160, 172eqtrd 2640 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝐹) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
1749, 173syl5eq 2652 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝑁 = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
175159, 174fveq12d 6091 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))))
176 eqid 2606 . . . . . . . . . 10 (coeff‘(Xp𝑓 − (ℂ × {𝑧}))) = (coeff‘(Xp𝑓 − (ℂ × {𝑧})))
177 eqid 2606 . . . . . . . . . 10 (coeff‘𝑄) = (coeff‘𝑄)
178176, 177, 169, 170coemulhi 23728 . . . . . . . . 9 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
17969, 32, 178syl2anc 690 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
180161fveq2d 6089 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) = ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1))
181 ssid 3583 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
182 plyid 23683 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
183181, 101, 182mp2an 703 . . . . . . . . . . . . . 14 Xp ∈ (Poly‘ℂ)
184 plyconst 23680 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
185181, 50, 184sylancr 693 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
186 eqid 2606 . . . . . . . . . . . . . . 15 (coeff‘Xp) = (coeff‘Xp)
187 eqid 2606 . . . . . . . . . . . . . . 15 (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
188186, 187coesub 23731 . . . . . . . . . . . . . 14 ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧}))))
189183, 185, 188sylancr 693 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧}))))
190189fveq1d 6087 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1))
191 1nn0 11152 . . . . . . . . . . . . . 14 1 ∈ ℕ0
192186coef3 23706 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
193 ffn 5941 . . . . . . . . . . . . . . . . 17 ((coeff‘Xp):ℕ0⟶ℂ → (coeff‘Xp) Fn ℕ0)
194183, 192, 193mp2b 10 . . . . . . . . . . . . . . . 16 (coeff‘Xp) Fn ℕ0
195194a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘Xp) Fn ℕ0)
196187coef3 23706 . . . . . . . . . . . . . . . 16 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
197 ffn 5941 . . . . . . . . . . . . . . . 16 ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
198185, 196, 1973syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
199 nn0ex 11142 . . . . . . . . . . . . . . . 16 0 ∈ V
200199a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ℕ0 ∈ V)
201 inidm 3780 . . . . . . . . . . . . . . 15 (ℕ0 ∩ ℕ0) = ℕ0
202 coeidp 23737 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
203202adantl 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
204 eqid 2606 . . . . . . . . . . . . . . . . 17 1 = 1
205204iftruei 4039 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
206203, 205syl6eq 2656 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
207 0lt1 10396 . . . . . . . . . . . . . . . . . 18 0 < 1
208 0re 9893 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
209 1re 9892 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
210208, 209ltnlei 10006 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ ¬ 1 ≤ 0)
211207, 210mpbi 218 . . . . . . . . . . . . . . . . 17 ¬ 1 ≤ 0
21250adantr 479 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
213 0dgr 23719 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
214212, 213syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
215214breq2d 4586 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
216211, 215mtbiri 315 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
217 eqid 2606 . . . . . . . . . . . . . . . . . . . 20 (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
218187, 217dgrub 23708 . . . . . . . . . . . . . . . . . . 19 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
2192183expia 1258 . . . . . . . . . . . . . . . . . 18 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
220185, 219sylan 486 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
221220necon1bd 2796 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
222216, 221mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
223195, 198, 200, 200, 201, 206, 222ofval 6778 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
224191, 223mpan2 702 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
225 1m0e1 10975 . . . . . . . . . . . . 13 (1 − 0) = 1
226224, 225syl6eq 2656 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = 1)
227190, 226eqtrd 2640 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) = 1)
228180, 227eqtrd 2640 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) = 1)
229228oveq1d 6539 . . . . . . . . 9 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
230177coef3 23706 . . . . . . . . . . . 12 (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
23132, 230syl 17 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
232231, 34ffvelrnd 6250 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
233232mulid2d 9911 . . . . . . . . 9 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
234229, 233eqtrd 2640 . . . . . . . 8 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
235175, 179, 2343eqtrd 2644 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
236157, 235oveq12d 6542 . . . . . 6 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
237236negeqd 10123 . . . . 5 ((𝜑𝑧𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
238155, 237eqtr4d 2643 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)))
239134, 238oveq12d 6542 . . 3 ((𝜑𝑧𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
24050negcld 10227 . . . . 5 ((𝜑𝑧𝑅) → -𝑧 ∈ ℂ)
241 nnm1nn0 11178 . . . . . . . . 9 (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
2423, 241syl 17 . . . . . . . 8 (𝜑 → (𝐷 − 1) ∈ ℕ0)
243242adantr 479 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 − 1) ∈ ℕ0)
244231, 243ffvelrnd 6250 . . . . . 6 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
245235, 232eqeltrd 2684 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ∈ ℂ)
2469, 27dgreq0 23739 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
24743, 246syl 17 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
248247necon3bid 2822 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴𝑁) ≠ 0))
24983, 248mpbid 220 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ≠ 0)
250244, 245, 249divcld 10647 . . . . 5 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) ∈ ℂ)
251240, 250negdid 10253 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
252240, 245mulcld 9913 . . . . . . 7 ((𝜑𝑧𝑅) → (-𝑧 · (𝐴𝑁)) ∈ ℂ)
253252, 244, 245, 249divdird 10685 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
254 nnm1nn0 11178 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
2555, 254syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
256255adantr 479 . . . . . . . . 9 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ0)
257176, 177coemul 23726 . . . . . . . . 9 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
25869, 32, 256, 257syl3anc 1317 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
259159fveq1d 6087 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘(𝑁 − 1)))
260 1e0p1 11381 . . . . . . . . . . . 12 1 = (0 + 1)
261260oveq2i 6535 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
262261sumeq1i 14219 . . . . . . . . . 10 Σ𝑘 ∈ (0...1)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
263 0nn0 11151 . . . . . . . . . . . . 13 0 ∈ ℕ0
264 nn0uz 11551 . . . . . . . . . . . . 13 0 = (ℤ‘0)
265263, 264eleqtri 2682 . . . . . . . . . . . 12 0 ∈ (ℤ‘0)
266265a1i 11 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 0 ∈ (ℤ‘0))
267261eleq2i 2676 . . . . . . . . . . . 12 (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
268176coef3 23706 . . . . . . . . . . . . . . 15 ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))):ℕ0⟶ℂ)
26969, 268syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))):ℕ0⟶ℂ)
270 elfznn0 12254 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
271 ffvelrn 6247 . . . . . . . . . . . . . 14 (((coeff‘(Xp𝑓 − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
272269, 270, 271syl2an 492 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
2732oveq1d 6539 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
274 pncan 10135 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
275102, 101, 274sylancl 692 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
276273, 275eqtr3d 2642 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) = 𝐷)
277276adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝑁 − 1) = 𝐷)
2783adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐷 ∈ ℕ)
279277, 278eqeltrd 2684 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ)
280 nnuz 11552 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
281279, 280syl6eleq 2694 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ (ℤ‘1))
282 fzss2 12204 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ (ℤ‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
283281, 282syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
284283sselda 3564 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
285 fznn0sub 12196 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
286 ffvelrn 6247 . . . . . . . . . . . . . . 15 (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
287231, 285, 286syl2an 492 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
288284, 287syldan 485 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
289272, 288mulcld 9913 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
290267, 289sylan2br 491 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
291 id 22 . . . . . . . . . . . . . 14 (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
292291, 260syl6eqr 2658 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → 𝑘 = 1)
293292fveq2d 6089 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1))
294292oveq2d 6540 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
295294fveq2d 6089 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
296293, 295oveq12d 6542 . . . . . . . . . . 11 (𝑘 = (0 + 1) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
297266, 290, 296fsump1 14272 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
298262, 297syl5eq 2652 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
299 eldifn 3691 . . . . . . . . . . . . . 14 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
300299adantl 480 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
301 eldifi 3690 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
302 elfznn0 12254 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
303301, 302syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
304176, 169dgrub 23708 . . . . . . . . . . . . . . . . 17 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧}))))
3053043expia 1258 . . . . . . . . . . . . . . . 16 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧})))))
30669, 303, 305syl2an 492 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧})))))
307 elfzuz 12161 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ‘0))
308301, 307syl 17 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ‘0))
309308adantl 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ‘0))
310 1z 11237 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
311 elfz5 12157 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
312309, 310, 311sylancl 692 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
313161breq2d 4586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
314313adantr 479 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
315312, 314bitr4d 269 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧})))))
316306, 315sylibrd 247 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
317316necon1bd 2796 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = 0))
318300, 317mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = 0)
319318oveq1d 6539 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
320301, 287sylan2 489 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
321320mul02d 10082 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
322319, 321eqtrd 2640 . . . . . . . . . 10 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
323 fzfid 12586 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (0...(𝑁 − 1)) ∈ Fin)
324283, 289, 322, 323fsumss 14246 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
325 0z 11218 . . . . . . . . . . . 12 0 ∈ ℤ
326189fveq1d 6087 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0))
327 coeidp 23737 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
328162nesymi 2835 . . . . . . . . . . . . . . . . . . . . 21 ¬ 0 = 1
329328iffalsei 4042 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
330327, 329syl6eq 2656 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
331330adantl 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
332 0cn 9885 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℂ
333 vex 3172 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
334333fvconst2 6349 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
335332, 334ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℂ × {𝑧})‘0) = 𝑧
336187coefv0 23722 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
337185, 336syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
338335, 337syl5reqr 2655 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
339338adantr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
340195, 198, 200, 200, 201, 331, 339ofval 6778 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
341263, 340mpan2 702 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
342 df-neg 10117 . . . . . . . . . . . . . . . 16 -𝑧 = (0 − 𝑧)
343341, 342syl6eqr 2658 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
344326, 343eqtrd 2640 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) = -𝑧)
345277oveq1d 6539 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
346103subid1d 10229 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝐷 − 0) = 𝐷)
347345, 346, 313eqtrd 2644 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
348347fveq2d 6089 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
349348, 235eqtr4d 2643 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴𝑁))
350344, 349oveq12d 6542 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴𝑁)))
351350, 252eqeltrd 2684 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
352 fveq2 6085 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0))
353 oveq2 6532 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
354353fveq2d 6089 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
355352, 354oveq12d 6542 . . . . . . . . . . . . 13 (𝑘 = 0 → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
356355fsum1 14263 . . . . . . . . . . . 12 ((0 ∈ ℤ ∧ (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
357325, 351, 356sylancr 693 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
358357, 350eqtrd 2640 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴𝑁)))
359277oveq1d 6539 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 1) = (𝐷 − 1))
360359fveq2d 6089 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
361227, 360oveq12d 6542 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
362244mulid2d 9911 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
363361, 362eqtrd 2640 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
364358, 363oveq12d 6542 . . . . . . . . 9 ((𝜑𝑧𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
365298, 324, 3643eqtr3rd 2649 . . . . . . . 8 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
366258, 259, 3653eqtr4rd 2651 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
367366oveq1d 6539 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
368240, 245, 249divcan4d 10653 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) = -𝑧)
369368oveq1d 6539 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
370253, 367, 3693eqtr3rd 2649 . . . . 5 ((𝜑𝑧𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
371370negeqd 10123 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
372251, 371eqtr3d 2642 . . 3 ((𝜑𝑧𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
373129, 239, 3723eqtrd 2644 . 2 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
37425, 373exlimddv 1849 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wo 381  wa 382  w3a 1030   = wceq 1474  wex 1694  wcel 1976  wne 2776  wral 2892  Vcvv 3169  cdif 3533  cun 3534  cin 3535  wss 3536  c0 3870  ifcif 4032  {csn 4121   class class class wbr 4574   × cxp 5023  ccnv 5024  dom cdm 5025  cima 5028   Fn wfn 5782  wf 5783  cfv 5787  (class class class)co 6524  𝑓 cof 6767  Fincfn 7815  cc 9787  cr 9788  0cc0 9789  1c1 9790   + caddc 9792   · cmul 9794   < clt 9927  cle 9928  cmin 10114  -cneg 10115   / cdiv 10530  cn 10864  0cn0 11136  cz 11207  cuz 11516  ...cfz 12149  #chash 12931  Σcsu 14207  0𝑝c0p 23156  Polycply 23658  Xpcidp 23659  coeffccoe 23660  degcdgr 23661   quot cquot 23763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-n0 11137  df-z 11208  df-uz 11517  df-rp 11662  df-fz 12150  df-fzo 12287  df-fl 12407  df-seq 12616  df-exp 12675  df-hash 12932  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-clim 14010  df-rlim 14011  df-sum 14208  df-0p 23157  df-ply 23662  df-idp 23663  df-coe 23664  df-dgr 23665  df-quot 23764
This theorem is referenced by:  vieta1  23785
  Copyright terms: Public domain W3C validator