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

Theorem vieta1lem2 24047
Description: Lemma for vieta1 24048: 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 11022 . . . . . . 7 (𝜑 → (𝐷 + 1) ∈ ℕ)
52, 4eqeltrrd 2700 . . . . . 6 (𝜑𝑁 ∈ ℕ)
65nnne0d 11050 . . . . 5 (𝜑𝑁 ≠ 0)
71, 6eqnetrd 2858 . . . 4 (𝜑 → (#‘𝑅) ≠ 0)
8 vieta1.4 . . . . . . . 8 (𝜑𝐹 ∈ (Poly‘𝑆))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (deg‘𝐹)
109, 6syl5eqner 2866 . . . . . . . . 9 (𝜑 → (deg‘𝐹) ≠ 0)
11 fveq2 6178 . . . . . . . . . . 11 (𝐹 = 0𝑝 → (deg‘𝐹) = (deg‘0𝑝))
12 dgr0 23999 . . . . . . . . . . 11 (deg‘0𝑝) = 0
1311, 12syl6eq 2670 . . . . . . . . . 10 (𝐹 = 0𝑝 → (deg‘𝐹) = 0)
1413necon3i 2823 . . . . . . . . 9 ((deg‘𝐹) ≠ 0 → 𝐹 ≠ 0𝑝)
1510, 14syl 17 . . . . . . . 8 (𝜑𝐹 ≠ 0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (𝐹 “ {0})
1716fta1 24044 . . . . . . . 8 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝐹 ≠ 0𝑝) → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
188, 15, 17syl2anc 692 . . . . . . 7 (𝜑 → (𝑅 ∈ Fin ∧ (#‘𝑅) ≤ (deg‘𝐹)))
1918simpld 475 . . . . . 6 (𝜑𝑅 ∈ Fin)
20 hasheq0 13137 . . . . . 6 (𝑅 ∈ Fin → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
2119, 20syl 17 . . . . 5 (𝜑 → ((#‘𝑅) = 0 ↔ 𝑅 = ∅))
2221necon3bid 2835 . . . 4 (𝜑 → ((#‘𝑅) ≠ 0 ↔ 𝑅 ≠ ∅))
237, 22mpbid 222 . . 3 (𝜑𝑅 ≠ ∅)
24 n0 3923 . . 3 (𝑅 ≠ ∅ ↔ ∃𝑧 𝑧𝑅)
2523, 24sylib 208 . 2 (𝜑 → ∃𝑧 𝑧𝑅)
26 incom 3797 . . . . 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 24046 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (𝑄 ∈ (Poly‘ℂ) ∧ 𝐷 = (deg‘𝑄)))
3130simprd 479 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐷 = (deg‘𝑄))
3230simpld 475 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝑄 ∈ (Poly‘ℂ))
33 dgrcl 23970 . . . . . . . . . . 11 (𝑄 ∈ (Poly‘ℂ) → (deg‘𝑄) ∈ ℕ0)
3432, 33syl 17 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℕ0)
3534nn0red 11337 . . . . . . . . 9 ((𝜑𝑧𝑅) → (deg‘𝑄) ∈ ℝ)
3631, 35eqeltrd 2699 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 ∈ ℝ)
3736ltp1d 10939 . . . . . . . 8 ((𝜑𝑧𝑅) → 𝐷 < (𝐷 + 1))
3836, 37gtned 10157 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 + 1) ≠ 𝐷)
39 snssi 4330 . . . . . . . . . . 11 (𝑧 ∈ (𝑄 “ {0}) → {𝑧} ⊆ (𝑄 “ {0}))
40 ssequn1 3775 . . . . . . . . . . 11 ({𝑧} ⊆ (𝑄 “ {0}) ↔ ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4139, 40sylib 208 . . . . . . . . . 10 (𝑧 ∈ (𝑄 “ {0}) → ({𝑧} ∪ (𝑄 “ {0})) = (𝑄 “ {0}))
4241fveq2d 6182 . . . . . . . . 9 (𝑧 ∈ (𝑄 “ {0}) → (#‘({𝑧} ∪ (𝑄 “ {0}))) = (#‘(𝑄 “ {0})))
438adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ∈ (Poly‘𝑆))
44 cnvimass 5473 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 “ {0}) ⊆ dom 𝐹
4516, 44eqsstri 3627 . . . . . . . . . . . . . . . . . . . 20 𝑅 ⊆ dom 𝐹
46 plyf 23935 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ)
47 fdm 6038 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → dom 𝐹 = ℂ)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → dom 𝐹 = ℂ)
4945, 48syl5sseq 3645 . . . . . . . . . . . . . . . . . . 19 (𝜑𝑅 ⊆ ℂ)
5049sselda 3595 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝑧 ∈ ℂ)
5116eleq2i 2691 . . . . . . . . . . . . . . . . . . . 20 (𝑧𝑅𝑧 ∈ (𝐹 “ {0}))
52 ffn 6032 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:ℂ⟶ℂ → 𝐹 Fn ℂ)
53 fniniseg 6324 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn ℂ → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑧 ∈ (𝐹 “ {0}) ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5551, 54syl5bb 272 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑧𝑅 ↔ (𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0)))
5655simplbda 653 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝐹𝑧) = 0)
57 eqid 2620 . . . . . . . . . . . . . . . . . . 19 (Xp𝑓 − (ℂ × {𝑧})) = (Xp𝑓 − (ℂ × {𝑧}))
5857facth 24042 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Poly‘𝑆) ∧ 𝑧 ∈ ℂ ∧ (𝐹𝑧) = 0) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))))
5943, 50, 56, 58syl3anc 1324 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧})))))
6029oveq2i 6646 . . . . . . . . . . . . . . . . 17 ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · (𝐹 quot (Xp𝑓 − (ℂ × {𝑧}))))
6159, 60syl6eqr 2672 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))
6261cnveqd 5287 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐹 = ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))
6362imaeq1d 5453 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝐹 “ {0}) = (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}))
6416, 63syl5eq 2666 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 𝑅 = (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}))
65 cnex 10002 . . . . . . . . . . . . . . 15 ℂ ∈ V
6665a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ℂ ∈ V)
6757plyremlem 24040 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ ℂ → ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6850, 67syl 17 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1 ∧ ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧}))
6968simp1d 1071 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ))
70 plyf 23935 . . . . . . . . . . . . . . 15 ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (Xp𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
7169, 70syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ)
72 plyf 23935 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Poly‘ℂ) → 𝑄:ℂ⟶ℂ)
7332, 72syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄:ℂ⟶ℂ)
74 ofmulrt 24018 . . . . . . . . . . . . . 14 ((ℂ ∈ V ∧ (Xp𝑓 − (ℂ × {𝑧})):ℂ⟶ℂ ∧ 𝑄:ℂ⟶ℂ) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}) = (((Xp𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7566, 71, 73, 74syl3anc 1324 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) “ {0}) = (((Xp𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})))
7668simp3d 1073 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) “ {0}) = {𝑧})
7776uneq1d 3758 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) “ {0}) ∪ (𝑄 “ {0})) = ({𝑧} ∪ (𝑄 “ {0})))
7864, 75, 773eqtrd 2658 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → 𝑅 = ({𝑧} ∪ (𝑄 “ {0})))
7978fveq2d 6182 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (#‘𝑅) = (#‘({𝑧} ∪ (𝑄 “ {0}))))
801, 2eqtr4d 2657 . . . . . . . . . . . 12 (𝜑 → (#‘𝑅) = (𝐷 + 1))
8180adantr 481 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (#‘𝑅) = (𝐷 + 1))
8279, 81eqtr3d 2656 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (#‘({𝑧} ∪ (𝑄 “ {0}))) = (𝐷 + 1))
8315adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐹 ≠ 0𝑝)
8461, 83eqnetrrd 2859 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) ≠ 0𝑝)
85 plymul0or 24017 . . . . . . . . . . . . . . . . . . 19 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = 0𝑝 ↔ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8669, 32, 85syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) = 0𝑝 ↔ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8786necon3abid 2827 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄) ≠ 0𝑝 ↔ ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝)))
8884, 87mpbid 222 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
89 neanior 2883 . . . . . . . . . . . . . . . 16 (((Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝) ↔ ¬ ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝𝑄 = 0𝑝))
9088, 89sylibr 224 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝𝑄 ≠ 0𝑝))
9190simprd 479 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 𝑄 ≠ 0𝑝)
92 eqid 2620 . . . . . . . . . . . . . . 15 (𝑄 “ {0}) = (𝑄 “ {0})
9392fta1 24044 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝) → ((𝑄 “ {0}) ∈ Fin ∧ (#‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9432, 91, 93syl2anc 692 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∈ Fin ∧ (#‘(𝑄 “ {0})) ≤ (deg‘𝑄)))
9594simprd 479 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ≤ (deg‘𝑄))
9695, 31breqtrrd 4672 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ≤ 𝐷)
97 snfi 8023 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9894simpld 475 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (𝑄 “ {0}) ∈ Fin)
99 hashun2 13155 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (𝑄 “ {0}) ∈ Fin) → (#‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(𝑄 “ {0}))))
10097, 98, 99sylancr 694 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (#‘({𝑧} ∪ (𝑄 “ {0}))) ≤ ((#‘{𝑧}) + (#‘(𝑄 “ {0}))))
101 ax-1cn 9979 . . . . . . . . . . . . . . 15 1 ∈ ℂ
1023nncnd 11021 . . . . . . . . . . . . . . . 16 (𝜑𝐷 ∈ ℂ)
103102adantr 481 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → 𝐷 ∈ ℂ)
104 addcom 10207 . . . . . . . . . . . . . . 15 ((1 ∈ ℂ ∧ 𝐷 ∈ ℂ) → (1 + 𝐷) = (𝐷 + 1))
105101, 103, 104sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (1 + 𝐷) = (𝐷 + 1))
10682, 105eqtr4d 2657 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (#‘({𝑧} ∪ (𝑄 “ {0}))) = (1 + 𝐷))
107 hashsng 13142 . . . . . . . . . . . . . . 15 (𝑧𝑅 → (#‘{𝑧}) = 1)
108107adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (#‘{𝑧}) = 1)
109108oveq1d 6650 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((#‘{𝑧}) + (#‘(𝑄 “ {0}))) = (1 + (#‘(𝑄 “ {0}))))
110100, 106, 1093brtr3d 4675 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (1 + 𝐷) ≤ (1 + (#‘(𝑄 “ {0}))))
111 hashcl 13130 . . . . . . . . . . . . . . 15 ((𝑄 “ {0}) ∈ Fin → (#‘(𝑄 “ {0})) ∈ ℕ0)
11298, 111syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ∈ ℕ0)
113112nn0red 11337 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) ∈ ℝ)
114 1red 10040 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → 1 ∈ ℝ)
11536, 113, 114leadd2d 10607 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (𝐷 ≤ (#‘(𝑄 “ {0})) ↔ (1 + 𝐷) ≤ (1 + (#‘(𝑄 “ {0})))))
116110, 115mpbird 247 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 𝐷 ≤ (#‘(𝑄 “ {0})))
117113, 36letri3d 10164 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((#‘(𝑄 “ {0})) = 𝐷 ↔ ((#‘(𝑄 “ {0})) ≤ 𝐷𝐷 ≤ (#‘(𝑄 “ {0})))))
11896, 116, 117mpbir2and 956 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) = 𝐷)
11982, 118eqeq12d 2635 . . . . . . . . 9 ((𝜑𝑧𝑅) → ((#‘({𝑧} ∪ (𝑄 “ {0}))) = (#‘(𝑄 “ {0})) ↔ (𝐷 + 1) = 𝐷))
12042, 119syl5ib 234 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝑧 ∈ (𝑄 “ {0}) → (𝐷 + 1) = 𝐷))
121120necon3ad 2804 . . . . . . 7 ((𝜑𝑧𝑅) → ((𝐷 + 1) ≠ 𝐷 → ¬ 𝑧 ∈ (𝑄 “ {0})))
12238, 121mpd 15 . . . . . 6 ((𝜑𝑧𝑅) → ¬ 𝑧 ∈ (𝑄 “ {0}))
123 disjsn 4237 . . . . . 6 (((𝑄 “ {0}) ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ (𝑄 “ {0}))
124122, 123sylibr 224 . . . . 5 ((𝜑𝑧𝑅) → ((𝑄 “ {0}) ∩ {𝑧}) = ∅)
12526, 124syl5eq 2666 . . . 4 ((𝜑𝑧𝑅) → ({𝑧} ∩ (𝑄 “ {0})) = ∅)
12619adantr 481 . . . 4 ((𝜑𝑧𝑅) → 𝑅 ∈ Fin)
12749adantr 481 . . . . 5 ((𝜑𝑧𝑅) → 𝑅 ⊆ ℂ)
128127sselda 3595 . . . 4 (((𝜑𝑧𝑅) ∧ 𝑥𝑅) → 𝑥 ∈ ℂ)
129125, 78, 126, 128fsumsplit 14452 . . 3 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥))
130 id 22 . . . . . . 7 (𝑥 = 𝑧𝑥 = 𝑧)
131130sumsn 14456 . . . . . 6 ((𝑧 ∈ ℂ ∧ 𝑧 ∈ ℂ) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13250, 50, 131syl2anc 692 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = 𝑧)
13350negnegd 10368 . . . . 5 ((𝜑𝑧𝑅) → --𝑧 = 𝑧)
134132, 133eqtr4d 2657 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ {𝑧}𝑥 = --𝑧)
135118, 31eqtrd 2654 . . . . . 6 ((𝜑𝑧𝑅) → (#‘(𝑄 “ {0})) = (deg‘𝑄))
13628adantr 481 . . . . . . 7 ((𝜑𝑧𝑅) → ∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))))
137 fveq2 6178 . . . . . . . . . . 11 (𝑓 = 𝑄 → (deg‘𝑓) = (deg‘𝑄))
138137eqeq2d 2630 . . . . . . . . . 10 (𝑓 = 𝑄 → (𝐷 = (deg‘𝑓) ↔ 𝐷 = (deg‘𝑄)))
139 cnveq 5285 . . . . . . . . . . . . 13 (𝑓 = 𝑄𝑓 = 𝑄)
140139imaeq1d 5453 . . . . . . . . . . . 12 (𝑓 = 𝑄 → (𝑓 “ {0}) = (𝑄 “ {0}))
141140fveq2d 6182 . . . . . . . . . . 11 (𝑓 = 𝑄 → (#‘(𝑓 “ {0})) = (#‘(𝑄 “ {0})))
142141, 137eqeq12d 2635 . . . . . . . . . 10 (𝑓 = 𝑄 → ((#‘(𝑓 “ {0})) = (deg‘𝑓) ↔ (#‘(𝑄 “ {0})) = (deg‘𝑄)))
143138, 142anbi12d 746 . . . . . . . . 9 (𝑓 = 𝑄 → ((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) ↔ (𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄))))
144140sumeq1d 14412 . . . . . . . . . 10 (𝑓 = 𝑄 → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = Σ𝑥 ∈ (𝑄 “ {0})𝑥)
145 fveq2 6178 . . . . . . . . . . . . 13 (𝑓 = 𝑄 → (coeff‘𝑓) = (coeff‘𝑄))
146137oveq1d 6650 . . . . . . . . . . . . 13 (𝑓 = 𝑄 → ((deg‘𝑓) − 1) = ((deg‘𝑄) − 1))
147145, 146fveq12d 6184 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((coeff‘𝑓)‘((deg‘𝑓) − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
148145, 137fveq12d 6184 . . . . . . . . . . . 12 (𝑓 = 𝑄 → ((coeff‘𝑓)‘(deg‘𝑓)) = ((coeff‘𝑄)‘(deg‘𝑄)))
149147, 148oveq12d 6653 . . . . . . . . . . 11 (𝑓 = 𝑄 → (((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
150149negeqd 10260 . . . . . . . . . 10 (𝑓 = 𝑄 → -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
151144, 150eqeq12d 2635 . . . . . . . . 9 (𝑓 = 𝑄 → (Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓))) ↔ Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
152143, 151imbi12d 334 . . . . . . . 8 (𝑓 = 𝑄 → (((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) ↔ ((𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
153152rspcv 3300 . . . . . . 7 (𝑄 ∈ (Poly‘ℂ) → (∀𝑓 ∈ (Poly‘ℂ)((𝐷 = (deg‘𝑓) ∧ (#‘(𝑓 “ {0})) = (deg‘𝑓)) → Σ𝑥 ∈ (𝑓 “ {0})𝑥 = -(((coeff‘𝑓)‘((deg‘𝑓) − 1)) / ((coeff‘𝑓)‘(deg‘𝑓)))) → ((𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))))
15432, 136, 153sylc 65 . . . . . 6 ((𝜑𝑧𝑅) → ((𝐷 = (deg‘𝑄) ∧ (#‘(𝑄 “ {0})) = (deg‘𝑄)) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄)))))
15531, 135, 154mp2and 714 . . . . 5 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
15631oveq1d 6650 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐷 − 1) = ((deg‘𝑄) − 1))
157156fveq2d 6182 . . . . . . 7 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) = ((coeff‘𝑄)‘((deg‘𝑄) − 1)))
15861fveq2d 6182 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (coeff‘𝐹) = (coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
15927, 158syl5eq 2666 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝐴 = (coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
16061fveq2d 6182 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘𝐹) = (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)))
16168simp2d 1072 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 1)
162 ax-1ne0 9990 . . . . . . . . . . . . . . 15 1 ≠ 0
163162a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → 1 ≠ 0)
164161, 163eqnetrd 2858 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ≠ 0)
165 fveq2 6178 . . . . . . . . . . . . . . 15 ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = (deg‘0𝑝))
166165, 12syl6eq 2670 . . . . . . . . . . . . . 14 ((Xp𝑓 − (ℂ × {𝑧})) = 0𝑝 → (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = 0)
167166necon3i 2823 . . . . . . . . . . . . 13 ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) ≠ 0 → (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝)
168164, 167syl 17 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝)
169 eqid 2620 . . . . . . . . . . . . 13 (deg‘(Xp𝑓 − (ℂ × {𝑧}))) = (deg‘(Xp𝑓 − (ℂ × {𝑧})))
170 eqid 2620 . . . . . . . . . . . . 13 (deg‘𝑄) = (deg‘𝑄)
171169, 170dgrmul 24007 . . . . . . . . . . . 12 ((((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ (Xp𝑓 − (ℂ × {𝑧})) ≠ 0𝑝) ∧ (𝑄 ∈ (Poly‘ℂ) ∧ 𝑄 ≠ 0𝑝)) → (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
17269, 168, 32, 91, 171syl22anc 1325 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (deg‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄)) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
173160, 172eqtrd 2654 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (deg‘𝐹) = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
1749, 173syl5eq 2666 . . . . . . . . 9 ((𝜑𝑧𝑅) → 𝑁 = ((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄)))
175159, 174fveq12d 6184 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))))
176 eqid 2620 . . . . . . . . . 10 (coeff‘(Xp𝑓 − (ℂ × {𝑧}))) = (coeff‘(Xp𝑓 − (ℂ × {𝑧})))
177 eqid 2620 . . . . . . . . . 10 (coeff‘𝑄) = (coeff‘𝑄)
178176, 177, 169, 170coemulhi 23991 . . . . . . . . 9 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ)) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
17969, 32, 178syl2anc 692 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘((deg‘(Xp𝑓 − (ℂ × {𝑧}))) + (deg‘𝑄))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))))
180161fveq2d 6182 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) = ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1))
181 ssid 3616 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
182 plyid 23946 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 1 ∈ ℂ) → Xp ∈ (Poly‘ℂ))
183181, 101, 182mp2an 707 . . . . . . . . . . . . . 14 Xp ∈ (Poly‘ℂ)
184 plyconst 23943 . . . . . . . . . . . . . . 15 ((ℂ ⊆ ℂ ∧ 𝑧 ∈ ℂ) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
185181, 50, 184sylancr 694 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (ℂ × {𝑧}) ∈ (Poly‘ℂ))
186 eqid 2620 . . . . . . . . . . . . . . 15 (coeff‘Xp) = (coeff‘Xp)
187 eqid 2620 . . . . . . . . . . . . . . 15 (coeff‘(ℂ × {𝑧})) = (coeff‘(ℂ × {𝑧}))
188186, 187coesub 23994 . . . . . . . . . . . . . 14 ((Xp ∈ (Poly‘ℂ) ∧ (ℂ × {𝑧}) ∈ (Poly‘ℂ)) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧}))))
189183, 185, 188sylancr 694 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))) = ((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧}))))
190189fveq1d 6180 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) = (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1))
191 1nn0 11293 . . . . . . . . . . . . . 14 1 ∈ ℕ0
192186coef3 23969 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Poly‘ℂ) → (coeff‘Xp):ℕ0⟶ℂ)
193 ffn 6032 . . . . . . . . . . . . . . . . 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 23969 . . . . . . . . . . . . . . . 16 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → (coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ)
197 ffn 6032 . . . . . . . . . . . . . . . 16 ((coeff‘(ℂ × {𝑧})):ℕ0⟶ℂ → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
198185, 196, 1973syl 18 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (coeff‘(ℂ × {𝑧})) Fn ℕ0)
199 nn0ex 11283 . . . . . . . . . . . . . . . 16 0 ∈ V
200199a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ℕ0 ∈ V)
201 inidm 3814 . . . . . . . . . . . . . . 15 (ℕ0 ∩ ℕ0) = ℕ0
202 coeidp 24000 . . . . . . . . . . . . . . . . 17 (1 ∈ ℕ0 → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
203202adantl 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = if(1 = 1, 1, 0))
204 eqid 2620 . . . . . . . . . . . . . . . . 17 1 = 1
205204iftruei 4084 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
206203, 205syl6eq 2670 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘Xp)‘1) = 1)
207 0lt1 10535 . . . . . . . . . . . . . . . . . 18 0 < 1
208 0re 10025 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
209 1re 10024 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
210208, 209ltnlei 10143 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ ¬ 1 ≤ 0)
211207, 210mpbi 220 . . . . . . . . . . . . . . . . 17 ¬ 1 ≤ 0
21250adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → 𝑧 ∈ ℂ)
213 0dgr 23982 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ ℂ → (deg‘(ℂ × {𝑧})) = 0)
214212, 213syl 17 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (deg‘(ℂ × {𝑧})) = 0)
215214breq2d 4656 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (1 ≤ (deg‘(ℂ × {𝑧})) ↔ 1 ≤ 0))
216211, 215mtbiri 317 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ¬ 1 ≤ (deg‘(ℂ × {𝑧})))
217 eqid 2620 . . . . . . . . . . . . . . . . . . . 20 (deg‘(ℂ × {𝑧})) = (deg‘(ℂ × {𝑧}))
218187, 217dgrub 23971 . . . . . . . . . . . . . . . . . . 19 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0 ∧ ((coeff‘(ℂ × {𝑧}))‘1) ≠ 0) → 1 ≤ (deg‘(ℂ × {𝑧})))
2192183expia 1265 . . . . . . . . . . . . . . . . . 18 (((ℂ × {𝑧}) ∈ (Poly‘ℂ) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
220185, 219sylan 488 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘(ℂ × {𝑧}))‘1) ≠ 0 → 1 ≤ (deg‘(ℂ × {𝑧}))))
221220necon1bd 2809 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (¬ 1 ≤ (deg‘(ℂ × {𝑧})) → ((coeff‘(ℂ × {𝑧}))‘1) = 0))
222216, 221mpd 15 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘1) = 0)
223195, 198, 200, 200, 201, 206, 222ofval 6891 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 1 ∈ ℕ0) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
224191, 223mpan2 706 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = (1 − 0))
225 1m0e1 11116 . . . . . . . . . . . . 13 (1 − 0) = 1
226224, 225syl6eq 2670 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘1) = 1)
227190, 226eqtrd 2654 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) = 1)
228180, 227eqtrd 2654 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) = 1)
229228oveq1d 6650 . . . . . . . . 9 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = (1 · ((coeff‘𝑄)‘(deg‘𝑄))))
230177coef3 23969 . . . . . . . . . . . 12 (𝑄 ∈ (Poly‘ℂ) → (coeff‘𝑄):ℕ0⟶ℂ)
23132, 230syl 17 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (coeff‘𝑄):ℕ0⟶ℂ)
232231, 34ffvelrnd 6346 . . . . . . . . . 10 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(deg‘𝑄)) ∈ ℂ)
233232mulid2d 10043 . . . . . . . . 9 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
234229, 233eqtrd 2654 . . . . . . . 8 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘(deg‘(Xp𝑓 − (ℂ × {𝑧})))) · ((coeff‘𝑄)‘(deg‘𝑄))) = ((coeff‘𝑄)‘(deg‘𝑄)))
235175, 179, 2343eqtrd 2658 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐴𝑁) = ((coeff‘𝑄)‘(deg‘𝑄)))
236157, 235oveq12d 6653 . . . . . 6 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = (((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
237236negeqd 10260 . . . . 5 ((𝜑𝑧𝑅) → -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) = -(((coeff‘𝑄)‘((deg‘𝑄) − 1)) / ((coeff‘𝑄)‘(deg‘𝑄))))
238155, 237eqtr4d 2657 . . . 4 ((𝜑𝑧𝑅) → Σ𝑥 ∈ (𝑄 “ {0})𝑥 = -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)))
239134, 238oveq12d 6653 . . 3 ((𝜑𝑧𝑅) → (Σ𝑥 ∈ {𝑧}𝑥 + Σ𝑥 ∈ (𝑄 “ {0})𝑥) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
24050negcld 10364 . . . . 5 ((𝜑𝑧𝑅) → -𝑧 ∈ ℂ)
241 nnm1nn0 11319 . . . . . . . . 9 (𝐷 ∈ ℕ → (𝐷 − 1) ∈ ℕ0)
2423, 241syl 17 . . . . . . . 8 (𝜑 → (𝐷 − 1) ∈ ℕ0)
243242adantr 481 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐷 − 1) ∈ ℕ0)
244231, 243ffvelrnd 6346 . . . . . 6 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘(𝐷 − 1)) ∈ ℂ)
245235, 232eqeltrd 2699 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ∈ ℂ)
2469, 27dgreq0 24002 . . . . . . . . 9 (𝐹 ∈ (Poly‘𝑆) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
24743, 246syl 17 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐹 = 0𝑝 ↔ (𝐴𝑁) = 0))
248247necon3bid 2835 . . . . . . 7 ((𝜑𝑧𝑅) → (𝐹 ≠ 0𝑝 ↔ (𝐴𝑁) ≠ 0))
24983, 248mpbid 222 . . . . . 6 ((𝜑𝑧𝑅) → (𝐴𝑁) ≠ 0)
250244, 245, 249divcld 10786 . . . . 5 ((𝜑𝑧𝑅) → (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁)) ∈ ℂ)
251240, 250negdid 10390 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
252240, 245mulcld 10045 . . . . . . 7 ((𝜑𝑧𝑅) → (-𝑧 · (𝐴𝑁)) ∈ ℂ)
253252, 244, 245, 249divdird 10824 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
254 nnm1nn0 11319 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
2555, 254syl 17 . . . . . . . . . 10 (𝜑 → (𝑁 − 1) ∈ ℕ0)
256255adantr 481 . . . . . . . . 9 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ0)
257176, 177coemul 23989 . . . . . . . . 9 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑄 ∈ (Poly‘ℂ) ∧ (𝑁 − 1) ∈ ℕ0) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
25869, 32, 256, 257syl3anc 1324 . . . . . . . 8 ((𝜑𝑧𝑅) → ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘(𝑁 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
259159fveq1d 6180 . . . . . . . 8 ((𝜑𝑧𝑅) → (𝐴‘(𝑁 − 1)) = ((coeff‘((Xp𝑓 − (ℂ × {𝑧})) ∘𝑓 · 𝑄))‘(𝑁 − 1)))
260 1e0p1 11537 . . . . . . . . . . . 12 1 = (0 + 1)
261260oveq2i 6646 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
262261sumeq1i 14409 . . . . . . . . . 10 Σ𝑘 ∈ (0...1)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)))
263 0nn0 11292 . . . . . . . . . . . . 13 0 ∈ ℕ0
264 nn0uz 11707 . . . . . . . . . . . . 13 0 = (ℤ‘0)
265263, 264eleqtri 2697 . . . . . . . . . . . 12 0 ∈ (ℤ‘0)
266265a1i 11 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → 0 ∈ (ℤ‘0))
267261eleq2i 2691 . . . . . . . . . . . 12 (𝑘 ∈ (0...1) ↔ 𝑘 ∈ (0...(0 + 1)))
268176coef3 23969 . . . . . . . . . . . . . . 15 ((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))):ℕ0⟶ℂ)
26969, 268syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → (coeff‘(Xp𝑓 − (ℂ × {𝑧}))):ℕ0⟶ℂ)
270 elfznn0 12417 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...1) → 𝑘 ∈ ℕ0)
271 ffvelrn 6343 . . . . . . . . . . . . . 14 (((coeff‘(Xp𝑓 − (ℂ × {𝑧}))):ℕ0⟶ℂ ∧ 𝑘 ∈ ℕ0) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
272269, 270, 271syl2an 494 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ∈ ℂ)
2732oveq1d 6650 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = (𝑁 − 1))
274 pncan 10272 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐷 + 1) − 1) = 𝐷)
275102, 101, 274sylancl 693 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 + 1) − 1) = 𝐷)
276273, 275eqtr3d 2656 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑁 − 1) = 𝐷)
277276adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → (𝑁 − 1) = 𝐷)
2783adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑧𝑅) → 𝐷 ∈ ℕ)
279277, 278eqeltrd 2699 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ ℕ)
280 nnuz 11708 . . . . . . . . . . . . . . . . 17 ℕ = (ℤ‘1)
281279, 280syl6eleq 2709 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (𝑁 − 1) ∈ (ℤ‘1))
282 fzss2 12366 . . . . . . . . . . . . . . . 16 ((𝑁 − 1) ∈ (ℤ‘1) → (0...1) ⊆ (0...(𝑁 − 1)))
283281, 282syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (0...1) ⊆ (0...(𝑁 − 1)))
284283sselda 3595 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
285 fznn0sub 12358 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...(𝑁 − 1)) → ((𝑁 − 1) − 𝑘) ∈ ℕ0)
286 ffvelrn 6343 . . . . . . . . . . . . . . 15 (((coeff‘𝑄):ℕ0⟶ℂ ∧ ((𝑁 − 1) − 𝑘) ∈ ℕ0) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
287231, 285, 286syl2an 494 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
288284, 287syldan 487 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
289272, 288mulcld 10045 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...1)) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
290267, 289sylan2br 493 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ (0...(0 + 1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) ∈ ℂ)
291 id 22 . . . . . . . . . . . . . 14 (𝑘 = (0 + 1) → 𝑘 = (0 + 1))
292291, 260syl6eqr 2672 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → 𝑘 = 1)
293292fveq2d 6182 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1))
294292oveq2d 6651 . . . . . . . . . . . . 13 (𝑘 = (0 + 1) → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 1))
295294fveq2d 6182 . . . . . . . . . . . 12 (𝑘 = (0 + 1) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 1)))
296293, 295oveq12d 6653 . . . . . . . . . . 11 (𝑘 = (0 + 1) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))))
297266, 290, 296fsump1 14468 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...(0 + 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
298262, 297syl5eq 2666 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))))
299 eldifn 3725 . . . . . . . . . . . . . 14 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → ¬ 𝑘 ∈ (0...1))
300299adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ¬ 𝑘 ∈ (0...1))
301 eldifi 3724 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (0...(𝑁 − 1)))
302 elfznn0 12417 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0)
303301, 302syl 17 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ ℕ0)
304176, 169dgrub 23971 . . . . . . . . . . . . . . . . 17 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0 ∧ ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0) → 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧}))))
3053043expia 1265 . . . . . . . . . . . . . . . 16 (((Xp𝑓 − (ℂ × {𝑧})) ∈ (Poly‘ℂ) ∧ 𝑘 ∈ ℕ0) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧})))))
30669, 303, 305syl2an 494 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧})))))
307 elfzuz 12323 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ (ℤ‘0))
308301, 307syl 17 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1)) → 𝑘 ∈ (ℤ‘0))
309308adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → 𝑘 ∈ (ℤ‘0))
310 1z 11392 . . . . . . . . . . . . . . . . 17 1 ∈ ℤ
311 elfz5 12319 . . . . . . . . . . . . . . . . 17 ((𝑘 ∈ (ℤ‘0) ∧ 1 ∈ ℤ) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
312309, 310, 311sylancl 693 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ 1))
313161breq2d 4656 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
314313adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧}))) ↔ 𝑘 ≤ 1))
315312, 314bitr4d 271 . . . . . . . . . . . . . . 15 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (𝑘 ∈ (0...1) ↔ 𝑘 ≤ (deg‘(Xp𝑓 − (ℂ × {𝑧})))))
316306, 315sylibrd 249 . . . . . . . . . . . . . 14 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) ≠ 0 → 𝑘 ∈ (0...1)))
317316necon1bd 2809 . . . . . . . . . . . . 13 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (¬ 𝑘 ∈ (0...1) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = 0))
318300, 317mpd 15 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = 0)
319318oveq1d 6650 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
320301, 287sylan2 491 . . . . . . . . . . . 12 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) ∈ ℂ)
321320mul02d 10219 . . . . . . . . . . 11 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (0 · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
322319, 321eqtrd 2654 . . . . . . . . . 10 (((𝜑𝑧𝑅) ∧ 𝑘 ∈ ((0...(𝑁 − 1)) ∖ (0...1))) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = 0)
323 fzfid 12755 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (0...(𝑁 − 1)) ∈ Fin)
324283, 289, 322, 323fsumss 14437 . . . . . . . . 9 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...1)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
325 0z 11373 . . . . . . . . . . . 12 0 ∈ ℤ
326189fveq1d 6180 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) = (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0))
327 coeidp 24000 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = if(0 = 1, 1, 0))
328162nesymi 2848 . . . . . . . . . . . . . . . . . . . . 21 ¬ 0 = 1
329328iffalsei 4087 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
330327, 329syl6eq 2670 . . . . . . . . . . . . . . . . . . 19 (0 ∈ ℕ0 → ((coeff‘Xp)‘0) = 0)
331330adantl 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘Xp)‘0) = 0)
332 0cn 10017 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℂ
333 vex 3198 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
334333fvconst2 6454 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ ℂ → ((ℂ × {𝑧})‘0) = 𝑧)
335332, 334ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((ℂ × {𝑧})‘0) = 𝑧
336187coefv0 23985 . . . . . . . . . . . . . . . . . . . . 21 ((ℂ × {𝑧}) ∈ (Poly‘ℂ) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
337185, 336syl 17 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑧𝑅) → ((ℂ × {𝑧})‘0) = ((coeff‘(ℂ × {𝑧}))‘0))
338335, 337syl5reqr 2669 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑧𝑅) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
339338adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → ((coeff‘(ℂ × {𝑧}))‘0) = 𝑧)
340195, 198, 200, 200, 201, 331, 339ofval 6891 . . . . . . . . . . . . . . . . 17 (((𝜑𝑧𝑅) ∧ 0 ∈ ℕ0) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
341263, 340mpan2 706 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = (0 − 𝑧))
342 df-neg 10254 . . . . . . . . . . . . . . . 16 -𝑧 = (0 − 𝑧)
343341, 342syl6eqr 2672 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → (((coeff‘Xp) ∘𝑓 − (coeff‘(ℂ × {𝑧})))‘0) = -𝑧)
344326, 343eqtrd 2654 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) = -𝑧)
345277oveq1d 6650 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (𝐷 − 0))
346103subid1d 10366 . . . . . . . . . . . . . . . . 17 ((𝜑𝑧𝑅) → (𝐷 − 0) = 𝐷)
347345, 346, 313eqtrd 2658 . . . . . . . . . . . . . . . 16 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 0) = (deg‘𝑄))
348347fveq2d 6182 . . . . . . . . . . . . . . 15 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = ((coeff‘𝑄)‘(deg‘𝑄)))
349348, 235eqtr4d 2657 . . . . . . . . . . . . . 14 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 0)) = (𝐴𝑁))
350344, 349oveq12d 6653 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) = (-𝑧 · (𝐴𝑁)))
351350, 252eqeltrd 2699 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ)
352 fveq2 6178 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) = ((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0))
353 oveq2 6643 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ((𝑁 − 1) − 𝑘) = ((𝑁 − 1) − 0))
354353fveq2d 6182 . . . . . . . . . . . . . 14 (𝑘 = 0 → ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘)) = ((coeff‘𝑄)‘((𝑁 − 1) − 0)))
355352, 354oveq12d 6653 . . . . . . . . . . . . 13 (𝑘 = 0 → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
356355fsum1 14457 . . . . . . . . . . . 12 ((0 ∈ ℤ ∧ (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))) ∈ ℂ) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
357325, 351, 356sylancr 694 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘0) · ((coeff‘𝑄)‘((𝑁 − 1) − 0))))
358357, 350eqtrd 2654 . . . . . . . . . 10 ((𝜑𝑧𝑅) → Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) = (-𝑧 · (𝐴𝑁)))
359277oveq1d 6650 . . . . . . . . . . . . 13 ((𝜑𝑧𝑅) → ((𝑁 − 1) − 1) = (𝐷 − 1))
360359fveq2d 6182 . . . . . . . . . . . 12 ((𝜑𝑧𝑅) → ((coeff‘𝑄)‘((𝑁 − 1) − 1)) = ((coeff‘𝑄)‘(𝐷 − 1)))
361227, 360oveq12d 6653 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = (1 · ((coeff‘𝑄)‘(𝐷 − 1))))
362244mulid2d 10043 . . . . . . . . . . 11 ((𝜑𝑧𝑅) → (1 · ((coeff‘𝑄)‘(𝐷 − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
363361, 362eqtrd 2654 . . . . . . . . . 10 ((𝜑𝑧𝑅) → (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1))) = ((coeff‘𝑄)‘(𝐷 − 1)))
364358, 363oveq12d 6653 . . . . . . . . 9 ((𝜑𝑧𝑅) → (Σ𝑘 ∈ (0...0)(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))) + (((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘1) · ((coeff‘𝑄)‘((𝑁 − 1) − 1)))) = ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))))
365298, 324, 3643eqtr3rd 2663 . . . . . . . 8 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = Σ𝑘 ∈ (0...(𝑁 − 1))(((coeff‘(Xp𝑓 − (ℂ × {𝑧})))‘𝑘) · ((coeff‘𝑄)‘((𝑁 − 1) − 𝑘))))
366258, 259, 3653eqtr4rd 2665 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) = (𝐴‘(𝑁 − 1)))
367366oveq1d 6650 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) + ((coeff‘𝑄)‘(𝐷 − 1))) / (𝐴𝑁)) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
368240, 245, 249divcan4d 10792 . . . . . . 7 ((𝜑𝑧𝑅) → ((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) = -𝑧)
369368oveq1d 6650 . . . . . 6 ((𝜑𝑧𝑅) → (((-𝑧 · (𝐴𝑁)) / (𝐴𝑁)) + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))))
370253, 367, 3693eqtr3rd 2663 . . . . 5 ((𝜑𝑧𝑅) → (-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = ((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
371370negeqd 10260 . . . 4 ((𝜑𝑧𝑅) → -(-𝑧 + (((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
372251, 371eqtr3d 2656 . . 3 ((𝜑𝑧𝑅) → (--𝑧 + -(((coeff‘𝑄)‘(𝐷 − 1)) / (𝐴𝑁))) = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
373129, 239, 3723eqtrd 2658 . 2 ((𝜑𝑧𝑅) → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
37425, 373exlimddv 1861 1 (𝜑 → Σ𝑥𝑅 𝑥 = -((𝐴‘(𝑁 − 1)) / (𝐴𝑁)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1481  wex 1702  wcel 1988  wne 2791  wral 2909  Vcvv 3195  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  ifcif 4077  {csn 4168   class class class wbr 4644   × cxp 5102  ccnv 5103  dom cdm 5104  cima 5107   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  𝑓 cof 6880  Fincfn 7940  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926   < clt 10059  cle 10060  cmin 10251  -cneg 10252   / cdiv 10669  cn 11005  0cn0 11277  cz 11362  cuz 11672  ...cfz 12311  #chash 13100  Σcsu 14397  0𝑝c0p 23417  Polycply 23921  Xpcidp 23922  coeffccoe 23923  degcdgr 23924   quot cquot 24026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-n0 11278  df-xnn0 11349  df-z 11363  df-uz 11673  df-rp 11818  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-clim 14200  df-rlim 14201  df-sum 14398  df-0p 23418  df-ply 23925  df-idp 23926  df-coe 23927  df-dgr 23928  df-quot 24027
This theorem is referenced by:  vieta1  24048
  Copyright terms: Public domain W3C validator