MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vieta1lem2 Structured version   Visualization version   GIF version
Theorem vieta1lem2 26060
Description: Lemma for vieta1 26061: 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 ∘f βˆ’ (β„‚ Γ— {𝑧})))
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 12233 . . . . . . 7 (πœ‘ β†’ (𝐷 + 1) ∈ β„•)
52, 4eqeltrrd 2832 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
65nnne0d 12266 . . . . 5 (πœ‘ β†’ 𝑁 β‰  0)
71, 6eqnetrd 3006 . . . 4 (πœ‘ β†’ (β™―β€˜π‘…) β‰  0)
8 vieta1.4 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ (Polyβ€˜π‘†))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (degβ€˜πΉ)
109, 6eqnetrrid 3014 . . . . . . . . 9 (πœ‘ β†’ (degβ€˜πΉ) β‰  0)
11 fveq2 6890 . . . . . . . . . . 11 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = (degβ€˜0𝑝))
12 dgr0 26012 . . . . . . . . . . 11 (degβ€˜0𝑝) = 0
1311, 12eqtrdi 2786 . . . . . . . . . 10 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = 0)
1413necon3i 2971 . . . . . . . . 9 ((degβ€˜πΉ) β‰  0 β†’ 𝐹 β‰  0𝑝)
1510, 14syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹 β‰  0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (◑𝐹 β€œ {0})
1716fta1 26057 . . . . . . . 8 ((𝐹 ∈ (Polyβ€˜π‘†) ∧ 𝐹 β‰  0𝑝) β†’ (𝑅 ∈ Fin ∧ (β™―β€˜π‘…) ≀ (degβ€˜πΉ)))
188, 15, 17syl2anc 582 . . . . . . 7 (πœ‘ β†’ (𝑅 ∈ Fin ∧ (β™―β€˜π‘…) ≀ (degβ€˜πΉ)))
1918simpld 493 . . . . . 6 (πœ‘ β†’ 𝑅 ∈ Fin)
20 hasheq0 14327 . . . . . 6 (𝑅 ∈ Fin β†’ ((β™―β€˜π‘…) = 0 ↔ 𝑅 = βˆ…))
2119, 20syl 17 . . . . 5 (πœ‘ β†’ ((β™―β€˜π‘…) = 0 ↔ 𝑅 = βˆ…))
2221necon3bid 2983 . . . 4 (πœ‘ β†’ ((β™―β€˜π‘…) β‰  0 ↔ 𝑅 β‰  βˆ…))
237, 22mpbid 231 . . 3 (πœ‘ β†’ 𝑅 β‰  βˆ…)
24 n0 4345 . . 3 (𝑅 β‰  βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ 𝑅)
2523, 24sylib 217 . 2 (πœ‘ β†’ βˆƒπ‘§ 𝑧 ∈ 𝑅)
26 incom 4200 . . . . 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 ∘f βˆ’ (β„‚ Γ— {𝑧})))
3027, 9, 16, 8, 1, 3, 2, 28, 29vieta1lem1 26059 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝐷 = (degβ€˜π‘„)))
3130simprd 494 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 = (degβ€˜π‘„))
3230simpld 493 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄 ∈ (Polyβ€˜β„‚))
33 dgrcl 25982 . . . . . . . . . . 11 (𝑄 ∈ (Polyβ€˜β„‚) β†’ (degβ€˜π‘„) ∈ β„•0)
3432, 33syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜π‘„) ∈ β„•0)
3534nn0red 12537 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜π‘„) ∈ ℝ)
3631, 35eqeltrd 2831 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ ℝ)
3736ltp1d 12148 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 < (𝐷 + 1))
3836, 37gtned 11353 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 + 1) β‰  𝐷)
39 snssi 4810 . . . . . . . . . . 11 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ {𝑧} βŠ† (◑𝑄 β€œ {0}))
40 ssequn1 4179 . . . . . . . . . . 11 ({𝑧} βŠ† (◑𝑄 β€œ {0}) ↔ ({𝑧} βˆͺ (◑𝑄 β€œ {0})) = (◑𝑄 β€œ {0}))
4139, 40sylib 217 . . . . . . . . . 10 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ ({𝑧} βˆͺ (◑𝑄 β€œ {0})) = (◑𝑄 β€œ {0}))
4241fveq2d 6894 . . . . . . . . 9 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (β™―β€˜(◑𝑄 β€œ {0})))
438adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 ∈ (Polyβ€˜π‘†))
44 cnvimass 6079 . . . . . . . . . . . . . . . . . . . . 21 (◑𝐹 β€œ {0}) βŠ† dom 𝐹
4516, 44eqsstri 4015 . . . . . . . . . . . . . . . . . . . 20 𝑅 βŠ† dom 𝐹
46 plyf 25947 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Polyβ€˜π‘†) β†’ 𝐹:β„‚βŸΆβ„‚)
47 fdm 6725 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:β„‚βŸΆβ„‚ β†’ dom 𝐹 = β„‚)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ dom 𝐹 = β„‚)
4945, 48sseqtrid 4033 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑅 βŠ† β„‚)
5049sselda 3981 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑧 ∈ β„‚)
5116eleq2i 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◑𝐹 β€œ {0}))
52 ffn 6716 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:β„‚βŸΆβ„‚ β†’ 𝐹 Fn β„‚)
53 fniniseg 7060 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn β„‚ β†’ (𝑧 ∈ (◑𝐹 β€œ {0}) ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑧 ∈ (◑𝐹 β€œ {0}) ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
5551, 54bitrid 282 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
5655simplbda 498 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (πΉβ€˜π‘§) = 0)
57 eqid 2730 . . . . . . . . . . . . . . . . . . 19 (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = (Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))
5857facth 26055 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Polyβ€˜π‘†) ∧ 𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
5943, 50, 56, 58syl3anc 1369 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
6029oveq2i 7422 . . . . . . . . . . . . . . . . 17 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))))
6159, 60eqtr4di 2788 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))
6261cnveqd 5874 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ◑𝐹 = β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))
6362imaeq1d 6057 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (◑𝐹 β€œ {0}) = (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}))
6416, 63eqtrid 2782 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 = (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}))
65 cnex 11193 . . . . . . . . . . . . . 14 β„‚ ∈ V
6657plyremlem 26053 . . . . . . . . . . . . . . . . 17 (𝑧 ∈ β„‚ β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 1 ∧ (β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) = {𝑧}))
6750, 66syl 17 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 1 ∧ (β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) = {𝑧}))
6867simp1d 1140 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚))
69 plyf 25947 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚)
71 plyf 25947 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Polyβ€˜β„‚) β†’ 𝑄:β„‚βŸΆβ„‚)
7232, 71syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄:β„‚βŸΆβ„‚)
73 ofmulrt 26031 . . . . . . . . . . . . . 14 ((β„‚ ∈ V ∧ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚ ∧ 𝑄:β„‚βŸΆβ„‚) β†’ (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}) = ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})))
7465, 70, 72, 73mp3an2i 1464 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}) = ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})))
7567simp3d 1142 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) = {𝑧})
7675uneq1d 4161 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})) = ({𝑧} βˆͺ (◑𝑄 β€œ {0})))
7764, 74, 763eqtrd 2774 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 = ({𝑧} βˆͺ (◑𝑄 β€œ {0})))
7877fveq2d 6894 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜π‘…) = (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))))
791, 2eqtr4d 2773 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜π‘…) = (𝐷 + 1))
8079adantr 479 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜π‘…) = (𝐷 + 1))
8178, 80eqtr3d 2772 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (𝐷 + 1))
8215adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 β‰  0𝑝)
8361, 82eqnetrrd 3007 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β‰  0𝑝)
84 plymul0or 26030 . . . . . . . . . . . . . . . . . . 19 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚)) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = 0𝑝 ↔ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8568, 32, 84syl2anc 582 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = 0𝑝 ↔ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8685necon3abid 2975 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β‰  0𝑝 ↔ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8783, 86mpbid 231 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88 neanior 3033 . . . . . . . . . . . . . . . 16 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝 ∧ 𝑄 β‰  0𝑝) ↔ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
8987, 88sylibr 233 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝 ∧ 𝑄 β‰  0𝑝))
9089simprd 494 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄 β‰  0𝑝)
91 eqid 2730 . . . . . . . . . . . . . . 15 (◑𝑄 β€œ {0}) = (◑𝑄 β€œ {0})
9291fta1 26057 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝑄 β‰  0𝑝) β†’ ((◑𝑄 β€œ {0}) ∈ Fin ∧ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„)))
9332, 90, 92syl2anc 582 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((◑𝑄 β€œ {0}) ∈ Fin ∧ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„)))
9493simprd 494 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„))
9594, 31breqtrrd 5175 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ≀ 𝐷)
96 snfi 9046 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9793simpld 493 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (◑𝑄 β€œ {0}) ∈ Fin)
98 hashun2 14347 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (◑𝑄 β€œ {0}) ∈ Fin) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) ≀ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))))
9996, 97, 98sylancr 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) ≀ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))))
100 ax-1cn 11170 . . . . . . . . . . . . . . 15 1 ∈ β„‚
1013nncnd 12232 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐷 ∈ β„‚)
102101adantr 479 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ β„‚)
103 addcom 11404 . . . . . . . . . . . . . . 15 ((1 ∈ β„‚ ∧ 𝐷 ∈ β„‚) β†’ (1 + 𝐷) = (𝐷 + 1))
104100, 102, 103sylancr 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 + 𝐷) = (𝐷 + 1))
10581, 104eqtr4d 2773 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (1 + 𝐷))
106 hashsng 14333 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝑅 β†’ (β™―β€˜{𝑧}) = 1)
107106adantl 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜{𝑧}) = 1)
108107oveq1d 7426 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))) = (1 + (β™―β€˜(◑𝑄 β€œ {0}))))
10999, 105, 1083brtr3d 5178 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 + 𝐷) ≀ (1 + (β™―β€˜(◑𝑄 β€œ {0}))))
110 hashcl 14320 . . . . . . . . . . . . . . 15 ((◑𝑄 β€œ {0}) ∈ Fin β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ β„•0)
11197, 110syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ β„•0)
112111nn0red 12537 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ ℝ)
113 1red 11219 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 1 ∈ ℝ)
11436, 112, 113leadd2d 11813 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})) ↔ (1 + 𝐷) ≀ (1 + (β™―β€˜(◑𝑄 β€œ {0})))))
115109, 114mpbird 256 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})))
116112, 36letri3d 11360 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜(◑𝑄 β€œ {0})) = 𝐷 ↔ ((β™―β€˜(◑𝑄 β€œ {0})) ≀ 𝐷 ∧ 𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})))))
11795, 115, 116mpbir2and 709 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) = 𝐷)
11881, 117eqeq12d 2746 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (β™―β€˜(◑𝑄 β€œ {0})) ↔ (𝐷 + 1) = 𝐷))
11942, 118imbitrid 243 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ (𝐷 + 1) = 𝐷))
120119necon3ad 2951 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝐷 + 1) β‰  𝐷 β†’ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0})))
12138, 120mpd 15 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0}))
122 disjsn 4714 . . . . . 6 (((◑𝑄 β€œ {0}) ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0}))
123121, 122sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((◑𝑄 β€œ {0}) ∩ {𝑧}) = βˆ…)
12426, 123eqtrid 2782 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ({𝑧} ∩ (◑𝑄 β€œ {0})) = βˆ…)
12519adantr 479 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 ∈ Fin)
12649adantr 479 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 βŠ† β„‚)
127126sselda 3981 . . . 4 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘₯ ∈ 𝑅) β†’ π‘₯ ∈ β„‚)
128124, 77, 125, 127fsumsplit 15691 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = (Ξ£π‘₯ ∈ {𝑧}π‘₯ + Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯))
129 id 22 . . . . . . 7 (π‘₯ = 𝑧 β†’ π‘₯ = 𝑧)
130129sumsn 15696 . . . . . 6 ((𝑧 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = 𝑧)
13150, 50, 130syl2anc 582 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = 𝑧)
13250negnegd 11566 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ --𝑧 = 𝑧)
133131, 132eqtr4d 2773 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = --𝑧)
134117, 31eqtrd 2770 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„))
135 fveq2 6890 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (degβ€˜π‘“) = (degβ€˜π‘„))
136135eqeq2d 2741 . . . . . . . . 9 (𝑓 = 𝑄 β†’ (𝐷 = (degβ€˜π‘“) ↔ 𝐷 = (degβ€˜π‘„)))
137 cnveq 5872 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ ◑𝑓 = ◑𝑄)
138137imaeq1d 6057 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ (◑𝑓 β€œ {0}) = (◑𝑄 β€œ {0}))
139138fveq2d 6894 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (β™―β€˜(◑𝑓 β€œ {0})) = (β™―β€˜(◑𝑄 β€œ {0})))
140139, 135eqeq12d 2746 . . . . . . . . 9 (𝑓 = 𝑄 β†’ ((β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“) ↔ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)))
141136, 140anbi12d 629 . . . . . . . 8 (𝑓 = 𝑄 β†’ ((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) ↔ (𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„))))
142138sumeq1d 15651 . . . . . . . . 9 (𝑓 = 𝑄 β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯)
143 fveq2 6890 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ (coeffβ€˜π‘“) = (coeffβ€˜π‘„))
144135oveq1d 7426 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ ((degβ€˜π‘“) βˆ’ 1) = ((degβ€˜π‘„) βˆ’ 1))
145143, 144fveq12d 6897 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ ((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)))
146143, 135fveq12d 6897 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
147145, 146oveq12d 7429 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) = (((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
148147negeqd 11458 . . . . . . . . 9 (𝑓 = 𝑄 β†’ -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
149142, 148eqeq12d 2746 . . . . . . . 8 (𝑓 = 𝑄 β†’ (Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) ↔ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))))
150141, 149imbi12d 343 . . . . . . 7 (𝑓 = 𝑄 β†’ (((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)))) ↔ ((𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))))
15128adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ βˆ€π‘“ ∈ (Polyβ€˜β„‚)((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)))))
152150, 151, 32rspcdva 3612 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))))
15331, 134, 152mp2and 695 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
15431fvoveq1d 7433 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)))
15561fveq2d 6894 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜πΉ) = (coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15627, 155eqtrid 2782 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐴 = (coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15761fveq2d 6894 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜πΉ) = (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15867simp2d 1141 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 1)
159 ax-1ne0 11181 . . . . . . . . . . . . . . 15 1 β‰  0
160159a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 1 β‰  0)
161158, 160eqnetrd 3006 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) β‰  0)
162 fveq2 6890 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (degβ€˜0𝑝))
163162, 12eqtrdi 2786 . . . . . . . . . . . . . 14 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 0)
164163necon3i 2971 . . . . . . . . . . . . 13 ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) β‰  0 β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝)
165161, 164syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝)
166 eqid 2730 . . . . . . . . . . . . 13 (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))
167 eqid 2730 . . . . . . . . . . . . 13 (degβ€˜π‘„) = (degβ€˜π‘„)
168166, 167dgrmul 26020 . . . . . . . . . . . 12 ((((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝) ∧ (𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝑄 β‰  0𝑝)) β†’ (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
16968, 165, 32, 90, 168syl22anc 835 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
170157, 169eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜πΉ) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
1719, 170eqtrid 2782 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑁 = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
172156, 171fveq12d 6897 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) = ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))))
173 eqid 2730 . . . . . . . . . 10 (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))
174 eqid 2730 . . . . . . . . . 10 (coeffβ€˜π‘„) = (coeffβ€˜π‘„)
175173, 174, 166, 167coemulhi 26003 . . . . . . . . 9 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚)) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
17668, 32, 175syl2anc 582 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
177158fveq2d 6894 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1))
178 ssid 4003 . . . . . . . . . . . . . . 15 β„‚ βŠ† β„‚
179 plyid 25958 . . . . . . . . . . . . . . 15 ((β„‚ βŠ† β„‚ ∧ 1 ∈ β„‚) β†’ Xp ∈ (Polyβ€˜β„‚))
180178, 100, 179mp2an 688 . . . . . . . . . . . . . 14 Xp ∈ (Polyβ€˜β„‚)
181 plyconst 25955 . . . . . . . . . . . . . . 15 ((β„‚ βŠ† β„‚ ∧ 𝑧 ∈ β„‚) β†’ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚))
182178, 50, 181sylancr 585 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚))
183 eqid 2730 . . . . . . . . . . . . . . 15 (coeffβ€˜Xp) = (coeffβ€˜Xp)
184 eqid 2730 . . . . . . . . . . . . . . 15 (coeffβ€˜(β„‚ Γ— {𝑧})) = (coeffβ€˜(β„‚ Γ— {𝑧}))
185183, 184coesub 26006 . . . . . . . . . . . . . 14 ((Xp ∈ (Polyβ€˜β„‚) ∧ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚)) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = ((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧}))))
186180, 182, 185sylancr 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = ((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧}))))
187186fveq1d 6892 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) = (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1))
188 1nn0 12492 . . . . . . . . . . . . . 14 1 ∈ β„•0
189183coef3 25981 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜Xp):β„•0βŸΆβ„‚)
190 ffn 6716 . . . . . . . . . . . . . . . . 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 25981 . . . . . . . . . . . . . . . 16 ((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜(β„‚ Γ— {𝑧})):β„•0βŸΆβ„‚)
194 ffn 6716 . . . . . . . . . . . . . . . 16 ((coeffβ€˜(β„‚ Γ— {𝑧})):β„•0βŸΆβ„‚ β†’ (coeffβ€˜(β„‚ Γ— {𝑧})) Fn β„•0)
195182, 193, 1943syl 18 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(β„‚ Γ— {𝑧})) Fn β„•0)
196 nn0ex 12482 . . . . . . . . . . . . . . . 16 β„•0 ∈ V
197196a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ β„•0 ∈ V)
198 inidm 4217 . . . . . . . . . . . . . . 15 (β„•0 ∩ β„•0) = β„•0
199 coeidp 26013 . . . . . . . . . . . . . . . . 17 (1 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜1) = if(1 = 1, 1, 0))
200199adantl 480 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜1) = if(1 = 1, 1, 0))
201 eqid 2730 . . . . . . . . . . . . . . . . 17 1 = 1
202201iftruei 4534 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
203200, 202eqtrdi 2786 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜1) = 1)
204 0lt1 11740 . . . . . . . . . . . . . . . . . 18 0 < 1
205 0re 11220 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
206 1re 11218 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
207205, 206ltnlei 11339 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ Β¬ 1 ≀ 0)
208204, 207mpbi 229 . . . . . . . . . . . . . . . . 17 Β¬ 1 ≀ 0
20950adantr 479 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ 𝑧 ∈ β„‚)
210 0dgr 25994 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ β„‚ β†’ (degβ€˜(β„‚ Γ— {𝑧})) = 0)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (degβ€˜(β„‚ Γ— {𝑧})) = 0)
212211breq2d 5159 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (1 ≀ (degβ€˜(β„‚ Γ— {𝑧})) ↔ 1 ≀ 0))
213208, 212mtbiri 326 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ Β¬ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})))
214 eqid 2730 . . . . . . . . . . . . . . . . . . . 20 (degβ€˜(β„‚ Γ— {𝑧})) = (degβ€˜(β„‚ Γ— {𝑧}))
215184, 214dgrub 25983 . . . . . . . . . . . . . . . . . . 19 (((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) ∧ 1 ∈ β„•0 ∧ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0) β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})))
2162153expia 1119 . . . . . . . . . . . . . . . . . 18 (((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0 β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧}))))
217182, 216sylan 578 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0 β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧}))))
218217necon1bd 2956 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (Β¬ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) = 0))
219213, 218mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) = 0)
220192, 195, 197, 197, 198, 203, 219ofval 7683 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = (1 βˆ’ 0))
221188, 220mpan2 687 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = (1 βˆ’ 0))
222 1m0e1 12337 . . . . . . . . . . . . 13 (1 βˆ’ 0) = 1
223221, 222eqtrdi 2786 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = 1)
224187, 223eqtrd 2770 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) = 1)
225177, 224eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) = 1)
226225oveq1d 7426 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = (1 Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
227174coef3 25981 . . . . . . . . . . . 12 (𝑄 ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜π‘„):β„•0βŸΆβ„‚)
22832, 227syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜π‘„):β„•0βŸΆβ„‚)
229228, 34ffvelcdmd 7086 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)) ∈ β„‚)
230229mullidd 11236 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
231226, 230eqtrd 2770 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
232172, 176, 2313eqtrd 2774 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
233154, 232oveq12d 7429 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) = (((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
234233negeqd 11458 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
235153, 234eqtr4d 2773 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)))
236133, 235oveq12d 7429 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Ξ£π‘₯ ∈ {𝑧}π‘₯ + Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯) = (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
23750negcld 11562 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -𝑧 ∈ β„‚)
238 nnm1nn0 12517 . . . . . . . . 9 (𝐷 ∈ β„• β†’ (𝐷 βˆ’ 1) ∈ β„•0)
2393, 238syl 17 . . . . . . . 8 (πœ‘ β†’ (𝐷 βˆ’ 1) ∈ β„•0)
240239adantr 479 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 βˆ’ 1) ∈ β„•0)
241228, 240ffvelcdmd 7086 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) ∈ β„‚)
242232, 229eqeltrd 2831 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) ∈ β„‚)
2439, 27dgreq0 26015 . . . . . . . . 9 (𝐹 ∈ (Polyβ€˜π‘†) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
24443, 243syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
245244necon3bid 2983 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐹 β‰  0𝑝 ↔ (π΄β€˜π‘) β‰  0))
24682, 245mpbid 231 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) β‰  0)
247241, 242, 246divcld 11994 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) ∈ β„‚)
248237, 247negdid 11588 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
249237, 242mulcld 11238 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (-𝑧 Β· (π΄β€˜π‘)) ∈ β„‚)
250249, 241, 242, 246divdird 12032 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) / (π΄β€˜π‘)) = (((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
251 nnm1nn0 12517 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) ∈ β„•0)
2525, 251syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„•0)
253252adantr 479 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ β„•0)
254173, 174coemul 26001 . . . . . . . . 9 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚) ∧ (𝑁 βˆ’ 1) ∈ β„•0) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
25568, 32, 253, 254syl3anc 1369 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
256156fveq1d 6892 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜(𝑁 βˆ’ 1)) = ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)))
257 1e0p1 12723 . . . . . . . . . . . 12 1 = (0 + 1)
258257oveq2i 7422 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
259258sumeq1i 15648 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = Ξ£π‘˜ ∈ (0...(0 + 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)))
260 0nn0 12491 . . . . . . . . . . . . 13 0 ∈ β„•0
261 nn0uz 12868 . . . . . . . . . . . . 13 β„•0 = (β„€β‰₯β€˜0)
262260, 261eleqtri 2829 . . . . . . . . . . . 12 0 ∈ (β„€β‰₯β€˜0)
263262a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 0 ∈ (β„€β‰₯β€˜0))
264258eleq2i 2823 . . . . . . . . . . . 12 (π‘˜ ∈ (0...1) ↔ π‘˜ ∈ (0...(0 + 1)))
265173coef3 25981 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚)
26668, 265syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚)
267 elfznn0 13598 . . . . . . . . . . . . . 14 (π‘˜ ∈ (0...1) β†’ π‘˜ ∈ β„•0)
268 ffvelcdm 7082 . . . . . . . . . . . . . 14 (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚ ∧ π‘˜ ∈ β„•0) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) ∈ β„‚)
269266, 267, 268syl2an 594 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) ∈ β„‚)
2702oveq1d 7426 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐷 + 1) βˆ’ 1) = (𝑁 βˆ’ 1))
271 pncan 11470 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝐷 + 1) βˆ’ 1) = 𝐷)
272101, 100, 271sylancl 584 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐷 + 1) βˆ’ 1) = 𝐷)
273270, 272eqtr3d 2772 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 βˆ’ 1) = 𝐷)
274273adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) = 𝐷)
2753adantr 479 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ β„•)
276274, 275eqeltrd 2831 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ β„•)
277 nnuz 12869 . . . . . . . . . . . . . . . . 17 β„• = (β„€β‰₯β€˜1)
278276, 277eleqtrdi 2841 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜1))
279 fzss2 13545 . . . . . . . . . . . . . . . 16 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜1) β†’ (0...1) βŠ† (0...(𝑁 βˆ’ 1)))
280278, 279syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (0...1) βŠ† (0...(𝑁 βˆ’ 1)))
281280sselda 3981 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ π‘˜ ∈ (0...(𝑁 βˆ’ 1)))
282 fznn0sub 13537 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) ∈ β„•0)
283 ffvelcdm 7082 . . . . . . . . . . . . . . 15 (((coeffβ€˜π‘„):β„•0βŸΆβ„‚ ∧ ((𝑁 βˆ’ 1) βˆ’ π‘˜) ∈ β„•0) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
284228, 282, 283syl2an 594 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...(𝑁 βˆ’ 1))) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
285281, 284syldan 589 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
286269, 285mulcld 11238 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) ∈ β„‚)
287264, 286sylan2br 593 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...(0 + 1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) ∈ β„‚)
288 id 22 . . . . . . . . . . . . . 14 (π‘˜ = (0 + 1) β†’ π‘˜ = (0 + 1))
289288, 257eqtr4di 2788 . . . . . . . . . . . . 13 (π‘˜ = (0 + 1) β†’ π‘˜ = 1)
290289fveq2d 6894 . . . . . . . . . . . 12 (π‘˜ = (0 + 1) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1))
291289oveq2d 7427 . . . . . . . . . . . . 13 (π‘˜ = (0 + 1) β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) = ((𝑁 βˆ’ 1) βˆ’ 1))
292291fveq2d 6894 . . . . . . . . . . . 12 (π‘˜ = (0 + 1) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) = ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))
293290, 292oveq12d 7429 . . . . . . . . . . 11 (π‘˜ = (0 + 1) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))))
294263, 287, 293fsump1 15706 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...(0 + 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))))
295259, 294eqtrid 2782 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))))
296 eldifn 4126 . . . . . . . . . . . . . 14 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ Β¬ π‘˜ ∈ (0...1))
297296adantl 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ Β¬ π‘˜ ∈ (0...1))
298 eldifi 4125 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ (0...(𝑁 βˆ’ 1)))
299 elfznn0 13598 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ π‘˜ ∈ β„•0)
300298, 299syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ β„•0)
301173, 166dgrub 25983 . . . . . . . . . . . . . . . . 17 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ π‘˜ ∈ β„•0 ∧ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))))
3023013expia 1119 . . . . . . . . . . . . . . . 16 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ π‘˜ ∈ β„•0) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
30368, 300, 302syl2an 594 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
304 elfzuz 13501 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
305298, 304syl 17 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
306305adantl 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
307 1z 12596 . . . . . . . . . . . . . . . . 17 1 ∈ β„€
308 elfz5 13497 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ (β„€β‰₯β€˜0) ∧ 1 ∈ β„€) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ 1))
309306, 307, 308sylancl 584 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ 1))
310158breq2d 5159 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) ↔ π‘˜ ≀ 1))
311310adantr 479 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) ↔ π‘˜ ≀ 1))
312309, 311bitr4d 281 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
313303, 312sylibrd 258 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ∈ (0...1)))
314313necon1bd 2956 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (Β¬ π‘˜ ∈ (0...1) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = 0))
315297, 314mpd 15 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = 0)
316315oveq1d 7426 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (0 Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
317298, 284sylan2 591 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
318317mul02d 11416 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (0 Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = 0)
319316, 318eqtrd 2770 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = 0)
320 fzfid 13942 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (0...(𝑁 βˆ’ 1)) ∈ Fin)
321280, 286, 319, 320fsumss 15675 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
322 0z 12573 . . . . . . . . . . . 12 0 ∈ β„€
323186fveq1d 6892 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) = (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0))
324 coeidp 26013 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜0) = if(0 = 1, 1, 0))
325159nesymi 2996 . . . . . . . . . . . . . . . . . . . . 21 Β¬ 0 = 1
326325iffalsei 4537 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
327324, 326eqtrdi 2786 . . . . . . . . . . . . . . . . . . 19 (0 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜0) = 0)
328327adantl 480 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜0) = 0)
329184coefv0 25997 . . . . . . . . . . . . . . . . . . . . 21 ((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) β†’ ((β„‚ Γ— {𝑧})β€˜0) = ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0))
330182, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β„‚ Γ— {𝑧})β€˜0) = ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0))
331 0cn 11210 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„‚
332 vex 3476 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
333332fvconst2 7206 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ β„‚ β†’ ((β„‚ Γ— {𝑧})β€˜0) = 𝑧)
334331, 333ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„‚ Γ— {𝑧})β€˜0) = 𝑧
335330, 334eqtr3di 2785 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0) = 𝑧)
336335adantr 479 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0) = 𝑧)
337192, 195, 197, 197, 198, 328, 336ofval 7683 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = (0 βˆ’ 𝑧))
338260, 337mpan2 687 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = (0 βˆ’ 𝑧))
339 df-neg 11451 . . . . . . . . . . . . . . . 16 -𝑧 = (0 βˆ’ 𝑧)
340338, 339eqtr4di 2788 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = -𝑧)
341323, 340eqtrd 2770 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) = -𝑧)
342274oveq1d 7426 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝑁 βˆ’ 1) βˆ’ 0) = (𝐷 βˆ’ 0))
343102subid1d 11564 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 βˆ’ 0) = 𝐷)
344342, 343, 313eqtrd 2774 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝑁 βˆ’ 1) βˆ’ 0) = (degβ€˜π‘„))
345344fveq2d 6894 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
346345, 232eqtr4d 2773 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)) = (π΄β€˜π‘))
347341, 346oveq12d 7429 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) = (-𝑧 Β· (π΄β€˜π‘)))
348347, 249eqeltrd 2831 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) ∈ β„‚)
349 fveq2 6890 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0))
350 oveq2 7419 . . . . . . . . . . . . . . 15 (π‘˜ = 0 β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) = ((𝑁 βˆ’ 1) βˆ’ 0))
351350fveq2d 6894 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) = ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)))
352349, 351oveq12d 7429 . . . . . . . . . . . . 13 (π‘˜ = 0 β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
353352fsum1 15697 . . . . . . . . . . . 12 ((0 ∈ β„€ ∧ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) ∈ β„‚) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
354322, 348, 353sylancr 585 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
355354, 347eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (-𝑧 Β· (π΄β€˜π‘)))
356274fvoveq1d 7433 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
357224, 356oveq12d 7429 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))) = (1 Β· ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))))
358241mullidd 11236 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 Β· ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
359357, 358eqtrd 2770 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
360355, 359oveq12d 7429 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))) = ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))))
361295, 321, 3603eqtr3rd 2779 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
362255, 256, 3613eqtr4rd 2781 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = (π΄β€˜(𝑁 βˆ’ 1)))
363362oveq1d 7426 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) / (π΄β€˜π‘)) = ((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
364237, 242, 246divcan4d 12000 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) = -𝑧)
365364oveq1d 7426 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = (-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
366250, 363, 3653eqtr3rd 2779 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = ((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
367366negeqd 11458 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
368248, 367eqtr3d 2772 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
369128, 236, 3683eqtrd 2774 . 2 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
37025, 369exlimddv 1936 1 (πœ‘ β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539  βˆƒwex 1779   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  Vcvv 3472   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  ifcif 4527  {csn 4627   class class class wbr 5147   Γ— cxp 5673  β—‘ccnv 5674  dom cdm 5675   β€œ cima 5678   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411   ∘f cof 7670  Fincfn 8941  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113   + caddc 11115   Β· cmul 11117   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  -cneg 11449   / cdiv 11875  β„•cn 12216  β„•0cn0 12476  β„€cz 12562  β„€β‰₯cuz 12826  ...cfz 13488  β™―chash 14294  Ξ£csu 15636  0𝑝c0p 25418  Polycply 25933  Xpcidp 25934  coeffccoe 25935  degcdgr 25936   quot cquot 26039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-inf 9440  df-oi 9507  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-n0 12477  df-xnn0 12549  df-z 12563  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-fl 13761  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-rlim 15437  df-sum 15637  df-0p 25419  df-ply 25937  df-idp 25938  df-coe 25939  df-dgr 25940  df-quot 26040
This theorem is referenced by:  vieta1  26061
  Copyright terms: Public domain W3C validator