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

Theorem vieta1lem2 25687
Description: Lemma for vieta1 25688: 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 12177 . . . . . . 7 (πœ‘ β†’ (𝐷 + 1) ∈ β„•)
52, 4eqeltrrd 2839 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
65nnne0d 12210 . . . . 5 (πœ‘ β†’ 𝑁 β‰  0)
71, 6eqnetrd 3012 . . . 4 (πœ‘ β†’ (β™―β€˜π‘…) β‰  0)
8 vieta1.4 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ (Polyβ€˜π‘†))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (degβ€˜πΉ)
109, 6eqnetrrid 3020 . . . . . . . . 9 (πœ‘ β†’ (degβ€˜πΉ) β‰  0)
11 fveq2 6847 . . . . . . . . . . 11 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = (degβ€˜0𝑝))
12 dgr0 25639 . . . . . . . . . . 11 (degβ€˜0𝑝) = 0
1311, 12eqtrdi 2793 . . . . . . . . . 10 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = 0)
1413necon3i 2977 . . . . . . . . 9 ((degβ€˜πΉ) β‰  0 β†’ 𝐹 β‰  0𝑝)
1510, 14syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹 β‰  0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (◑𝐹 β€œ {0})
1716fta1 25684 . . . . . . . 8 ((𝐹 ∈ (Polyβ€˜π‘†) ∧ 𝐹 β‰  0𝑝) β†’ (𝑅 ∈ Fin ∧ (β™―β€˜π‘…) ≀ (degβ€˜πΉ)))
188, 15, 17syl2anc 585 . . . . . . 7 (πœ‘ β†’ (𝑅 ∈ Fin ∧ (β™―β€˜π‘…) ≀ (degβ€˜πΉ)))
1918simpld 496 . . . . . 6 (πœ‘ β†’ 𝑅 ∈ Fin)
20 hasheq0 14270 . . . . . 6 (𝑅 ∈ Fin β†’ ((β™―β€˜π‘…) = 0 ↔ 𝑅 = βˆ…))
2119, 20syl 17 . . . . 5 (πœ‘ β†’ ((β™―β€˜π‘…) = 0 ↔ 𝑅 = βˆ…))
2221necon3bid 2989 . . . 4 (πœ‘ β†’ ((β™―β€˜π‘…) β‰  0 ↔ 𝑅 β‰  βˆ…))
237, 22mpbid 231 . . 3 (πœ‘ β†’ 𝑅 β‰  βˆ…)
24 n0 4311 . . 3 (𝑅 β‰  βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ 𝑅)
2523, 24sylib 217 . 2 (πœ‘ β†’ βˆƒπ‘§ 𝑧 ∈ 𝑅)
26 incom 4166 . . . . 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 25686 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝐷 = (degβ€˜π‘„)))
3130simprd 497 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 = (degβ€˜π‘„))
3230simpld 496 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄 ∈ (Polyβ€˜β„‚))
33 dgrcl 25610 . . . . . . . . . . 11 (𝑄 ∈ (Polyβ€˜β„‚) β†’ (degβ€˜π‘„) ∈ β„•0)
3432, 33syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜π‘„) ∈ β„•0)
3534nn0red 12481 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜π‘„) ∈ ℝ)
3631, 35eqeltrd 2838 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ ℝ)
3736ltp1d 12092 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 < (𝐷 + 1))
3836, 37gtned 11297 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 + 1) β‰  𝐷)
39 snssi 4773 . . . . . . . . . . 11 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ {𝑧} βŠ† (◑𝑄 β€œ {0}))
40 ssequn1 4145 . . . . . . . . . . 11 ({𝑧} βŠ† (◑𝑄 β€œ {0}) ↔ ({𝑧} βˆͺ (◑𝑄 β€œ {0})) = (◑𝑄 β€œ {0}))
4139, 40sylib 217 . . . . . . . . . 10 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ ({𝑧} βˆͺ (◑𝑄 β€œ {0})) = (◑𝑄 β€œ {0}))
4241fveq2d 6851 . . . . . . . . 9 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (β™―β€˜(◑𝑄 β€œ {0})))
438adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 ∈ (Polyβ€˜π‘†))
44 cnvimass 6038 . . . . . . . . . . . . . . . . . . . . 21 (◑𝐹 β€œ {0}) βŠ† dom 𝐹
4516, 44eqsstri 3983 . . . . . . . . . . . . . . . . . . . 20 𝑅 βŠ† dom 𝐹
46 plyf 25575 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Polyβ€˜π‘†) β†’ 𝐹:β„‚βŸΆβ„‚)
47 fdm 6682 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:β„‚βŸΆβ„‚ β†’ dom 𝐹 = β„‚)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ dom 𝐹 = β„‚)
4945, 48sseqtrid 4001 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑅 βŠ† β„‚)
5049sselda 3949 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑧 ∈ β„‚)
5116eleq2i 2830 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◑𝐹 β€œ {0}))
52 ffn 6673 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:β„‚βŸΆβ„‚ β†’ 𝐹 Fn β„‚)
53 fniniseg 7015 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn β„‚ β†’ (𝑧 ∈ (◑𝐹 β€œ {0}) ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑧 ∈ (◑𝐹 β€œ {0}) ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
5551, 54bitrid 283 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
5655simplbda 501 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (πΉβ€˜π‘§) = 0)
57 eqid 2737 . . . . . . . . . . . . . . . . . . 19 (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = (Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))
5857facth 25682 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Polyβ€˜π‘†) ∧ 𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
5943, 50, 56, 58syl3anc 1372 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
6029oveq2i 7373 . . . . . . . . . . . . . . . . 17 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))))
6159, 60eqtr4di 2795 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))
6261cnveqd 5836 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ◑𝐹 = β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))
6362imaeq1d 6017 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (◑𝐹 β€œ {0}) = (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}))
6416, 63eqtrid 2789 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 = (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}))
65 cnex 11139 . . . . . . . . . . . . . 14 β„‚ ∈ V
6657plyremlem 25680 . . . . . . . . . . . . . . . . 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 1143 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚))
69 plyf 25575 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚)
71 plyf 25575 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Polyβ€˜β„‚) β†’ 𝑄:β„‚βŸΆβ„‚)
7232, 71syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄:β„‚βŸΆβ„‚)
73 ofmulrt 25658 . . . . . . . . . . . . . 14 ((β„‚ ∈ V ∧ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚ ∧ 𝑄:β„‚βŸΆβ„‚) β†’ (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}) = ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})))
7465, 70, 72, 73mp3an2i 1467 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}) = ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})))
7567simp3d 1145 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) = {𝑧})
7675uneq1d 4127 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})) = ({𝑧} βˆͺ (◑𝑄 β€œ {0})))
7764, 74, 763eqtrd 2781 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 = ({𝑧} βˆͺ (◑𝑄 β€œ {0})))
7877fveq2d 6851 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜π‘…) = (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))))
791, 2eqtr4d 2780 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜π‘…) = (𝐷 + 1))
8079adantr 482 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜π‘…) = (𝐷 + 1))
8178, 80eqtr3d 2779 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (𝐷 + 1))
8215adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 β‰  0𝑝)
8361, 82eqnetrrd 3013 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β‰  0𝑝)
84 plymul0or 25657 . . . . . . . . . . . . . . . . . . 19 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚)) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = 0𝑝 ↔ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8568, 32, 84syl2anc 585 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = 0𝑝 ↔ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8685necon3abid 2981 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β‰  0𝑝 ↔ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8783, 86mpbid 231 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88 neanior 3038 . . . . . . . . . . . . . . . 16 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝 ∧ 𝑄 β‰  0𝑝) ↔ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
8987, 88sylibr 233 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝 ∧ 𝑄 β‰  0𝑝))
9089simprd 497 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄 β‰  0𝑝)
91 eqid 2737 . . . . . . . . . . . . . . 15 (◑𝑄 β€œ {0}) = (◑𝑄 β€œ {0})
9291fta1 25684 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝑄 β‰  0𝑝) β†’ ((◑𝑄 β€œ {0}) ∈ Fin ∧ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„)))
9332, 90, 92syl2anc 585 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((◑𝑄 β€œ {0}) ∈ Fin ∧ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„)))
9493simprd 497 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„))
9594, 31breqtrrd 5138 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ≀ 𝐷)
96 snfi 8995 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9793simpld 496 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (◑𝑄 β€œ {0}) ∈ Fin)
98 hashun2 14290 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (◑𝑄 β€œ {0}) ∈ Fin) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) ≀ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))))
9996, 97, 98sylancr 588 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) ≀ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))))
100 ax-1cn 11116 . . . . . . . . . . . . . . 15 1 ∈ β„‚
1013nncnd 12176 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐷 ∈ β„‚)
102101adantr 482 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ β„‚)
103 addcom 11348 . . . . . . . . . . . . . . 15 ((1 ∈ β„‚ ∧ 𝐷 ∈ β„‚) β†’ (1 + 𝐷) = (𝐷 + 1))
104100, 102, 103sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 + 𝐷) = (𝐷 + 1))
10581, 104eqtr4d 2780 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (1 + 𝐷))
106 hashsng 14276 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝑅 β†’ (β™―β€˜{𝑧}) = 1)
107106adantl 483 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜{𝑧}) = 1)
108107oveq1d 7377 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))) = (1 + (β™―β€˜(◑𝑄 β€œ {0}))))
10999, 105, 1083brtr3d 5141 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 + 𝐷) ≀ (1 + (β™―β€˜(◑𝑄 β€œ {0}))))
110 hashcl 14263 . . . . . . . . . . . . . . 15 ((◑𝑄 β€œ {0}) ∈ Fin β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ β„•0)
11197, 110syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ β„•0)
112111nn0red 12481 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ ℝ)
113 1red 11163 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 1 ∈ ℝ)
11436, 112, 113leadd2d 11757 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})) ↔ (1 + 𝐷) ≀ (1 + (β™―β€˜(◑𝑄 β€œ {0})))))
115109, 114mpbird 257 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})))
116112, 36letri3d 11304 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜(◑𝑄 β€œ {0})) = 𝐷 ↔ ((β™―β€˜(◑𝑄 β€œ {0})) ≀ 𝐷 ∧ 𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})))))
11795, 115, 116mpbir2and 712 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) = 𝐷)
11881, 117eqeq12d 2753 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (β™―β€˜(◑𝑄 β€œ {0})) ↔ (𝐷 + 1) = 𝐷))
11942, 118imbitrid 243 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ (𝐷 + 1) = 𝐷))
120119necon3ad 2957 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝐷 + 1) β‰  𝐷 β†’ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0})))
12138, 120mpd 15 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0}))
122 disjsn 4677 . . . . . 6 (((◑𝑄 β€œ {0}) ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0}))
123121, 122sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((◑𝑄 β€œ {0}) ∩ {𝑧}) = βˆ…)
12426, 123eqtrid 2789 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ({𝑧} ∩ (◑𝑄 β€œ {0})) = βˆ…)
12519adantr 482 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 ∈ Fin)
12649adantr 482 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 βŠ† β„‚)
127126sselda 3949 . . . 4 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘₯ ∈ 𝑅) β†’ π‘₯ ∈ β„‚)
128124, 77, 125, 127fsumsplit 15633 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = (Ξ£π‘₯ ∈ {𝑧}π‘₯ + Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯))
129 id 22 . . . . . . 7 (π‘₯ = 𝑧 β†’ π‘₯ = 𝑧)
130129sumsn 15638 . . . . . 6 ((𝑧 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = 𝑧)
13150, 50, 130syl2anc 585 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = 𝑧)
13250negnegd 11510 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ --𝑧 = 𝑧)
133131, 132eqtr4d 2780 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = --𝑧)
134117, 31eqtrd 2777 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„))
135 fveq2 6847 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (degβ€˜π‘“) = (degβ€˜π‘„))
136135eqeq2d 2748 . . . . . . . . 9 (𝑓 = 𝑄 β†’ (𝐷 = (degβ€˜π‘“) ↔ 𝐷 = (degβ€˜π‘„)))
137 cnveq 5834 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ ◑𝑓 = ◑𝑄)
138137imaeq1d 6017 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ (◑𝑓 β€œ {0}) = (◑𝑄 β€œ {0}))
139138fveq2d 6851 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (β™―β€˜(◑𝑓 β€œ {0})) = (β™―β€˜(◑𝑄 β€œ {0})))
140139, 135eqeq12d 2753 . . . . . . . . 9 (𝑓 = 𝑄 β†’ ((β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“) ↔ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)))
141136, 140anbi12d 632 . . . . . . . 8 (𝑓 = 𝑄 β†’ ((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) ↔ (𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„))))
142138sumeq1d 15593 . . . . . . . . 9 (𝑓 = 𝑄 β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯)
143 fveq2 6847 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ (coeffβ€˜π‘“) = (coeffβ€˜π‘„))
144135oveq1d 7377 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ ((degβ€˜π‘“) βˆ’ 1) = ((degβ€˜π‘„) βˆ’ 1))
145143, 144fveq12d 6854 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ ((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)))
146143, 135fveq12d 6854 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
147145, 146oveq12d 7380 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) = (((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
148147negeqd 11402 . . . . . . . . 9 (𝑓 = 𝑄 β†’ -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
149142, 148eqeq12d 2753 . . . . . . . 8 (𝑓 = 𝑄 β†’ (Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) ↔ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))))
150141, 149imbi12d 345 . . . . . . 7 (𝑓 = 𝑄 β†’ (((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)))) ↔ ((𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))))
15128adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ βˆ€π‘“ ∈ (Polyβ€˜β„‚)((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)))))
152150, 151, 32rspcdva 3585 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))))
15331, 134, 152mp2and 698 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
15431fvoveq1d 7384 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)))
15561fveq2d 6851 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜πΉ) = (coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15627, 155eqtrid 2789 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐴 = (coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15761fveq2d 6851 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜πΉ) = (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15867simp2d 1144 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 1)
159 ax-1ne0 11127 . . . . . . . . . . . . . . 15 1 β‰  0
160159a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 1 β‰  0)
161158, 160eqnetrd 3012 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) β‰  0)
162 fveq2 6847 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (degβ€˜0𝑝))
163162, 12eqtrdi 2793 . . . . . . . . . . . . . 14 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 0)
164163necon3i 2977 . . . . . . . . . . . . 13 ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) β‰  0 β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝)
165161, 164syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝)
166 eqid 2737 . . . . . . . . . . . . 13 (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))
167 eqid 2737 . . . . . . . . . . . . 13 (degβ€˜π‘„) = (degβ€˜π‘„)
168166, 167dgrmul 25647 . . . . . . . . . . . 12 ((((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝) ∧ (𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝑄 β‰  0𝑝)) β†’ (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
16968, 165, 32, 90, 168syl22anc 838 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
170157, 169eqtrd 2777 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜πΉ) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
1719, 170eqtrid 2789 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑁 = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
172156, 171fveq12d 6854 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) = ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))))
173 eqid 2737 . . . . . . . . . 10 (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))
174 eqid 2737 . . . . . . . . . 10 (coeffβ€˜π‘„) = (coeffβ€˜π‘„)
175173, 174, 166, 167coemulhi 25631 . . . . . . . . 9 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚)) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
17668, 32, 175syl2anc 585 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
177158fveq2d 6851 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1))
178 ssid 3971 . . . . . . . . . . . . . . 15 β„‚ βŠ† β„‚
179 plyid 25586 . . . . . . . . . . . . . . 15 ((β„‚ βŠ† β„‚ ∧ 1 ∈ β„‚) β†’ Xp ∈ (Polyβ€˜β„‚))
180178, 100, 179mp2an 691 . . . . . . . . . . . . . 14 Xp ∈ (Polyβ€˜β„‚)
181 plyconst 25583 . . . . . . . . . . . . . . 15 ((β„‚ βŠ† β„‚ ∧ 𝑧 ∈ β„‚) β†’ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚))
182178, 50, 181sylancr 588 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚))
183 eqid 2737 . . . . . . . . . . . . . . 15 (coeffβ€˜Xp) = (coeffβ€˜Xp)
184 eqid 2737 . . . . . . . . . . . . . . 15 (coeffβ€˜(β„‚ Γ— {𝑧})) = (coeffβ€˜(β„‚ Γ— {𝑧}))
185183, 184coesub 25634 . . . . . . . . . . . . . 14 ((Xp ∈ (Polyβ€˜β„‚) ∧ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚)) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = ((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧}))))
186180, 182, 185sylancr 588 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = ((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧}))))
187186fveq1d 6849 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) = (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1))
188 1nn0 12436 . . . . . . . . . . . . . 14 1 ∈ β„•0
189183coef3 25609 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜Xp):β„•0βŸΆβ„‚)
190 ffn 6673 . . . . . . . . . . . . . . . . 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 25609 . . . . . . . . . . . . . . . 16 ((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜(β„‚ Γ— {𝑧})):β„•0βŸΆβ„‚)
194 ffn 6673 . . . . . . . . . . . . . . . 16 ((coeffβ€˜(β„‚ Γ— {𝑧})):β„•0βŸΆβ„‚ β†’ (coeffβ€˜(β„‚ Γ— {𝑧})) Fn β„•0)
195182, 193, 1943syl 18 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(β„‚ Γ— {𝑧})) Fn β„•0)
196 nn0ex 12426 . . . . . . . . . . . . . . . 16 β„•0 ∈ V
197196a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ β„•0 ∈ V)
198 inidm 4183 . . . . . . . . . . . . . . 15 (β„•0 ∩ β„•0) = β„•0
199 coeidp 25640 . . . . . . . . . . . . . . . . 17 (1 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜1) = if(1 = 1, 1, 0))
200199adantl 483 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜1) = if(1 = 1, 1, 0))
201 eqid 2737 . . . . . . . . . . . . . . . . 17 1 = 1
202201iftruei 4498 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
203200, 202eqtrdi 2793 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜1) = 1)
204 0lt1 11684 . . . . . . . . . . . . . . . . . 18 0 < 1
205 0re 11164 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
206 1re 11162 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
207205, 206ltnlei 11283 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ Β¬ 1 ≀ 0)
208204, 207mpbi 229 . . . . . . . . . . . . . . . . 17 Β¬ 1 ≀ 0
20950adantr 482 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ 𝑧 ∈ β„‚)
210 0dgr 25622 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ β„‚ β†’ (degβ€˜(β„‚ Γ— {𝑧})) = 0)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (degβ€˜(β„‚ Γ— {𝑧})) = 0)
212211breq2d 5122 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (1 ≀ (degβ€˜(β„‚ Γ— {𝑧})) ↔ 1 ≀ 0))
213208, 212mtbiri 327 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ Β¬ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})))
214 eqid 2737 . . . . . . . . . . . . . . . . . . . 20 (degβ€˜(β„‚ Γ— {𝑧})) = (degβ€˜(β„‚ Γ— {𝑧}))
215184, 214dgrub 25611 . . . . . . . . . . . . . . . . . . 19 (((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) ∧ 1 ∈ β„•0 ∧ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0) β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})))
2162153expia 1122 . . . . . . . . . . . . . . . . . 18 (((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0 β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧}))))
217182, 216sylan 581 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0 β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧}))))
218217necon1bd 2962 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (Β¬ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) = 0))
219213, 218mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) = 0)
220192, 195, 197, 197, 198, 203, 219ofval 7633 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = (1 βˆ’ 0))
221188, 220mpan2 690 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = (1 βˆ’ 0))
222 1m0e1 12281 . . . . . . . . . . . . 13 (1 βˆ’ 0) = 1
223221, 222eqtrdi 2793 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = 1)
224187, 223eqtrd 2777 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) = 1)
225177, 224eqtrd 2777 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) = 1)
226225oveq1d 7377 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = (1 Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
227174coef3 25609 . . . . . . . . . . . 12 (𝑄 ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜π‘„):β„•0βŸΆβ„‚)
22832, 227syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜π‘„):β„•0βŸΆβ„‚)
229228, 34ffvelcdmd 7041 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)) ∈ β„‚)
230229mulid2d 11180 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
231226, 230eqtrd 2777 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
232172, 176, 2313eqtrd 2781 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
233154, 232oveq12d 7380 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) = (((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
234233negeqd 11402 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
235153, 234eqtr4d 2780 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)))
236133, 235oveq12d 7380 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Ξ£π‘₯ ∈ {𝑧}π‘₯ + Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯) = (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
23750negcld 11506 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -𝑧 ∈ β„‚)
238 nnm1nn0 12461 . . . . . . . . 9 (𝐷 ∈ β„• β†’ (𝐷 βˆ’ 1) ∈ β„•0)
2393, 238syl 17 . . . . . . . 8 (πœ‘ β†’ (𝐷 βˆ’ 1) ∈ β„•0)
240239adantr 482 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 βˆ’ 1) ∈ β„•0)
241228, 240ffvelcdmd 7041 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) ∈ β„‚)
242232, 229eqeltrd 2838 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) ∈ β„‚)
2439, 27dgreq0 25642 . . . . . . . . 9 (𝐹 ∈ (Polyβ€˜π‘†) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
24443, 243syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
245244necon3bid 2989 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐹 β‰  0𝑝 ↔ (π΄β€˜π‘) β‰  0))
24682, 245mpbid 231 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) β‰  0)
247241, 242, 246divcld 11938 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) ∈ β„‚)
248237, 247negdid 11532 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
249237, 242mulcld 11182 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (-𝑧 Β· (π΄β€˜π‘)) ∈ β„‚)
250249, 241, 242, 246divdird 11976 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) / (π΄β€˜π‘)) = (((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
251 nnm1nn0 12461 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) ∈ β„•0)
2525, 251syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„•0)
253252adantr 482 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ β„•0)
254173, 174coemul 25629 . . . . . . . . 9 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚) ∧ (𝑁 βˆ’ 1) ∈ β„•0) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
25568, 32, 253, 254syl3anc 1372 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
256156fveq1d 6849 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜(𝑁 βˆ’ 1)) = ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)))
257 1e0p1 12667 . . . . . . . . . . . 12 1 = (0 + 1)
258257oveq2i 7373 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
259258sumeq1i 15590 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = Ξ£π‘˜ ∈ (0...(0 + 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)))
260 0nn0 12435 . . . . . . . . . . . . 13 0 ∈ β„•0
261 nn0uz 12812 . . . . . . . . . . . . 13 β„•0 = (β„€β‰₯β€˜0)
262260, 261eleqtri 2836 . . . . . . . . . . . 12 0 ∈ (β„€β‰₯β€˜0)
263262a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 0 ∈ (β„€β‰₯β€˜0))
264258eleq2i 2830 . . . . . . . . . . . 12 (π‘˜ ∈ (0...1) ↔ π‘˜ ∈ (0...(0 + 1)))
265173coef3 25609 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚)
26668, 265syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚)
267 elfznn0 13541 . . . . . . . . . . . . . 14 (π‘˜ ∈ (0...1) β†’ π‘˜ ∈ β„•0)
268 ffvelcdm 7037 . . . . . . . . . . . . . 14 (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚ ∧ π‘˜ ∈ β„•0) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) ∈ β„‚)
269266, 267, 268syl2an 597 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) ∈ β„‚)
2702oveq1d 7377 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐷 + 1) βˆ’ 1) = (𝑁 βˆ’ 1))
271 pncan 11414 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝐷 + 1) βˆ’ 1) = 𝐷)
272101, 100, 271sylancl 587 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐷 + 1) βˆ’ 1) = 𝐷)
273270, 272eqtr3d 2779 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 βˆ’ 1) = 𝐷)
274273adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) = 𝐷)
2753adantr 482 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ β„•)
276274, 275eqeltrd 2838 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ β„•)
277 nnuz 12813 . . . . . . . . . . . . . . . . 17 β„• = (β„€β‰₯β€˜1)
278276, 277eleqtrdi 2848 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜1))
279 fzss2 13488 . . . . . . . . . . . . . . . 16 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜1) β†’ (0...1) βŠ† (0...(𝑁 βˆ’ 1)))
280278, 279syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (0...1) βŠ† (0...(𝑁 βˆ’ 1)))
281280sselda 3949 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ π‘˜ ∈ (0...(𝑁 βˆ’ 1)))
282 fznn0sub 13480 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) ∈ β„•0)
283 ffvelcdm 7037 . . . . . . . . . . . . . . 15 (((coeffβ€˜π‘„):β„•0βŸΆβ„‚ ∧ ((𝑁 βˆ’ 1) βˆ’ π‘˜) ∈ β„•0) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
284228, 282, 283syl2an 597 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...(𝑁 βˆ’ 1))) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
285281, 284syldan 592 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
286269, 285mulcld 11182 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) ∈ β„‚)
287264, 286sylan2br 596 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...(0 + 1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) ∈ β„‚)
288 id 22 . . . . . . . . . . . . . 14 (π‘˜ = (0 + 1) β†’ π‘˜ = (0 + 1))
289288, 257eqtr4di 2795 . . . . . . . . . . . . 13 (π‘˜ = (0 + 1) β†’ π‘˜ = 1)
290289fveq2d 6851 . . . . . . . . . . . 12 (π‘˜ = (0 + 1) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1))
291289oveq2d 7378 . . . . . . . . . . . . 13 (π‘˜ = (0 + 1) β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) = ((𝑁 βˆ’ 1) βˆ’ 1))
292291fveq2d 6851 . . . . . . . . . . . 12 (π‘˜ = (0 + 1) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) = ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))
293290, 292oveq12d 7380 . . . . . . . . . . 11 (π‘˜ = (0 + 1) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))))
294263, 287, 293fsump1 15648 . . . . . . . . . 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 2789 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))))
296 eldifn 4092 . . . . . . . . . . . . . 14 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ Β¬ π‘˜ ∈ (0...1))
297296adantl 483 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ Β¬ π‘˜ ∈ (0...1))
298 eldifi 4091 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ (0...(𝑁 βˆ’ 1)))
299 elfznn0 13541 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ π‘˜ ∈ β„•0)
300298, 299syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ β„•0)
301173, 166dgrub 25611 . . . . . . . . . . . . . . . . 17 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ π‘˜ ∈ β„•0 ∧ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))))
3023013expia 1122 . . . . . . . . . . . . . . . 16 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ π‘˜ ∈ β„•0) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
30368, 300, 302syl2an 597 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
304 elfzuz 13444 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
305298, 304syl 17 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
306305adantl 483 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
307 1z 12540 . . . . . . . . . . . . . . . . 17 1 ∈ β„€
308 elfz5 13440 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ (β„€β‰₯β€˜0) ∧ 1 ∈ β„€) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ 1))
309306, 307, 308sylancl 587 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ 1))
310158breq2d 5122 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) ↔ π‘˜ ≀ 1))
311310adantr 482 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) ↔ π‘˜ ≀ 1))
312309, 311bitr4d 282 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
313303, 312sylibrd 259 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ∈ (0...1)))
314313necon1bd 2962 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (Β¬ π‘˜ ∈ (0...1) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = 0))
315297, 314mpd 15 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = 0)
316315oveq1d 7377 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (0 Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
317298, 284sylan2 594 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
318317mul02d 11360 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (0 Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = 0)
319316, 318eqtrd 2777 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = 0)
320 fzfid 13885 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (0...(𝑁 βˆ’ 1)) ∈ Fin)
321280, 286, 319, 320fsumss 15617 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
322 0z 12517 . . . . . . . . . . . 12 0 ∈ β„€
323186fveq1d 6849 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) = (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0))
324 coeidp 25640 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜0) = if(0 = 1, 1, 0))
325159nesymi 3002 . . . . . . . . . . . . . . . . . . . . 21 Β¬ 0 = 1
326325iffalsei 4501 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
327324, 326eqtrdi 2793 . . . . . . . . . . . . . . . . . . 19 (0 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜0) = 0)
328327adantl 483 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜0) = 0)
329184coefv0 25625 . . . . . . . . . . . . . . . . . . . . 21 ((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) β†’ ((β„‚ Γ— {𝑧})β€˜0) = ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0))
330182, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β„‚ Γ— {𝑧})β€˜0) = ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0))
331 0cn 11154 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„‚
332 vex 3452 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
333332fvconst2 7158 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ β„‚ β†’ ((β„‚ Γ— {𝑧})β€˜0) = 𝑧)
334331, 333ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„‚ Γ— {𝑧})β€˜0) = 𝑧
335330, 334eqtr3di 2792 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0) = 𝑧)
336335adantr 482 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0) = 𝑧)
337192, 195, 197, 197, 198, 328, 336ofval 7633 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = (0 βˆ’ 𝑧))
338260, 337mpan2 690 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = (0 βˆ’ 𝑧))
339 df-neg 11395 . . . . . . . . . . . . . . . 16 -𝑧 = (0 βˆ’ 𝑧)
340338, 339eqtr4di 2795 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = -𝑧)
341323, 340eqtrd 2777 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) = -𝑧)
342274oveq1d 7377 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝑁 βˆ’ 1) βˆ’ 0) = (𝐷 βˆ’ 0))
343102subid1d 11508 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 βˆ’ 0) = 𝐷)
344342, 343, 313eqtrd 2781 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝑁 βˆ’ 1) βˆ’ 0) = (degβ€˜π‘„))
345344fveq2d 6851 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
346345, 232eqtr4d 2780 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)) = (π΄β€˜π‘))
347341, 346oveq12d 7380 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) = (-𝑧 Β· (π΄β€˜π‘)))
348347, 249eqeltrd 2838 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) ∈ β„‚)
349 fveq2 6847 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0))
350 oveq2 7370 . . . . . . . . . . . . . . 15 (π‘˜ = 0 β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) = ((𝑁 βˆ’ 1) βˆ’ 0))
351350fveq2d 6851 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) = ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)))
352349, 351oveq12d 7380 . . . . . . . . . . . . 13 (π‘˜ = 0 β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
353352fsum1 15639 . . . . . . . . . . . 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 588 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
355354, 347eqtrd 2777 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (-𝑧 Β· (π΄β€˜π‘)))
356274fvoveq1d 7384 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
357224, 356oveq12d 7380 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))) = (1 Β· ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))))
358241mulid2d 11180 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 Β· ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
359357, 358eqtrd 2777 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
360355, 359oveq12d 7380 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))) = ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))))
361295, 321, 3603eqtr3rd 2786 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
362255, 256, 3613eqtr4rd 2788 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = (π΄β€˜(𝑁 βˆ’ 1)))
363362oveq1d 7377 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) / (π΄β€˜π‘)) = ((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
364237, 242, 246divcan4d 11944 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) = -𝑧)
365364oveq1d 7377 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = (-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
366250, 363, 3653eqtr3rd 2786 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = ((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
367366negeqd 11402 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
368248, 367eqtr3d 2779 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
369128, 236, 3683eqtrd 2781 . 2 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
37025, 369exlimddv 1939 1 (πœ‘ β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542  βˆƒwex 1782   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065  Vcvv 3448   βˆ– cdif 3912   βˆͺ cun 3913   ∩ cin 3914   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  {csn 4591   class class class wbr 5110   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638   β€œ cima 5641   Fn wfn 6496  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362   ∘f cof 7620  Fincfn 8890  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392  -cneg 11393   / cdiv 11819  β„•cn 12160  β„•0cn0 12420  β„€cz 12506  β„€β‰₯cuz 12770  ...cfz 13431  β™―chash 14237  Ξ£csu 15577  0𝑝c0p 25049  Polycply 25561  Xpcidp 25562  coeffccoe 25563  degcdgr 25564   quot cquot 25666
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-om 7808  df-1st 7926  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-oadd 8421  df-er 8655  df-map 8774  df-pm 8775  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-n0 12421  df-xnn0 12493  df-z 12507  df-uz 12771  df-rp 12923  df-fz 13432  df-fzo 13575  df-fl 13704  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-clim 15377  df-rlim 15378  df-sum 15578  df-0p 25050  df-ply 25565  df-idp 25566  df-coe 25567  df-dgr 25568  df-quot 25667
This theorem is referenced by:  vieta1  25688
  Copyright terms: Public domain W3C validator