MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vieta1lem2 Structured version   Visualization version   GIF version
Theorem vieta1lem2 26061
Description: Lemma for vieta1 26062: 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 12234 . . . . . . 7 (πœ‘ β†’ (𝐷 + 1) ∈ β„•)
52, 4eqeltrrd 2833 . . . . . 6 (πœ‘ β†’ 𝑁 ∈ β„•)
65nnne0d 12267 . . . . 5 (πœ‘ β†’ 𝑁 β‰  0)
71, 6eqnetrd 3007 . . . 4 (πœ‘ β†’ (β™―β€˜π‘…) β‰  0)
8 vieta1.4 . . . . . . . 8 (πœ‘ β†’ 𝐹 ∈ (Polyβ€˜π‘†))
9 vieta1.2 . . . . . . . . . 10 𝑁 = (degβ€˜πΉ)
109, 6eqnetrrid 3015 . . . . . . . . 9 (πœ‘ β†’ (degβ€˜πΉ) β‰  0)
11 fveq2 6891 . . . . . . . . . . 11 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = (degβ€˜0𝑝))
12 dgr0 26013 . . . . . . . . . . 11 (degβ€˜0𝑝) = 0
1311, 12eqtrdi 2787 . . . . . . . . . 10 (𝐹 = 0𝑝 β†’ (degβ€˜πΉ) = 0)
1413necon3i 2972 . . . . . . . . 9 ((degβ€˜πΉ) β‰  0 β†’ 𝐹 β‰  0𝑝)
1510, 14syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹 β‰  0𝑝)
16 vieta1.3 . . . . . . . . 9 𝑅 = (◑𝐹 β€œ {0})
1716fta1 26058 . . . . . . . 8 ((𝐹 ∈ (Polyβ€˜π‘†) ∧ 𝐹 β‰  0𝑝) β†’ (𝑅 ∈ Fin ∧ (β™―β€˜π‘…) ≀ (degβ€˜πΉ)))
188, 15, 17syl2anc 583 . . . . . . 7 (πœ‘ β†’ (𝑅 ∈ Fin ∧ (β™―β€˜π‘…) ≀ (degβ€˜πΉ)))
1918simpld 494 . . . . . 6 (πœ‘ β†’ 𝑅 ∈ Fin)
20 hasheq0 14328 . . . . . 6 (𝑅 ∈ Fin β†’ ((β™―β€˜π‘…) = 0 ↔ 𝑅 = βˆ…))
2119, 20syl 17 . . . . 5 (πœ‘ β†’ ((β™―β€˜π‘…) = 0 ↔ 𝑅 = βˆ…))
2221necon3bid 2984 . . . 4 (πœ‘ β†’ ((β™―β€˜π‘…) β‰  0 ↔ 𝑅 β‰  βˆ…))
237, 22mpbid 231 . . 3 (πœ‘ β†’ 𝑅 β‰  βˆ…)
24 n0 4346 . . 3 (𝑅 β‰  βˆ… ↔ βˆƒπ‘§ 𝑧 ∈ 𝑅)
2523, 24sylib 217 . 2 (πœ‘ β†’ βˆƒπ‘§ 𝑧 ∈ 𝑅)
26 incom 4201 . . . . 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 26060 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝐷 = (degβ€˜π‘„)))
3130simprd 495 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 = (degβ€˜π‘„))
3230simpld 494 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄 ∈ (Polyβ€˜β„‚))
33 dgrcl 25983 . . . . . . . . . . 11 (𝑄 ∈ (Polyβ€˜β„‚) β†’ (degβ€˜π‘„) ∈ β„•0)
3432, 33syl 17 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜π‘„) ∈ β„•0)
3534nn0red 12538 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜π‘„) ∈ ℝ)
3631, 35eqeltrd 2832 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ ℝ)
3736ltp1d 12149 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 < (𝐷 + 1))
3836, 37gtned 11354 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 + 1) β‰  𝐷)
39 snssi 4811 . . . . . . . . . . 11 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ {𝑧} βŠ† (◑𝑄 β€œ {0}))
40 ssequn1 4180 . . . . . . . . . . 11 ({𝑧} βŠ† (◑𝑄 β€œ {0}) ↔ ({𝑧} βˆͺ (◑𝑄 β€œ {0})) = (◑𝑄 β€œ {0}))
4139, 40sylib 217 . . . . . . . . . 10 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ ({𝑧} βˆͺ (◑𝑄 β€œ {0})) = (◑𝑄 β€œ {0}))
4241fveq2d 6895 . . . . . . . . 9 (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (β™―β€˜(◑𝑄 β€œ {0})))
438adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 ∈ (Polyβ€˜π‘†))
44 cnvimass 6080 . . . . . . . . . . . . . . . . . . . . 21 (◑𝐹 β€œ {0}) βŠ† dom 𝐹
4516, 44eqsstri 4016 . . . . . . . . . . . . . . . . . . . 20 𝑅 βŠ† dom 𝐹
46 plyf 25948 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 ∈ (Polyβ€˜π‘†) β†’ 𝐹:β„‚βŸΆβ„‚)
47 fdm 6726 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:β„‚βŸΆβ„‚ β†’ dom 𝐹 = β„‚)
488, 46, 473syl 18 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ dom 𝐹 = β„‚)
4945, 48sseqtrid 4034 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝑅 βŠ† β„‚)
5049sselda 3982 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑧 ∈ β„‚)
5116eleq2i 2824 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ 𝑅 ↔ 𝑧 ∈ (◑𝐹 β€œ {0}))
52 ffn 6717 . . . . . . . . . . . . . . . . . . . . 21 (𝐹:β„‚βŸΆβ„‚ β†’ 𝐹 Fn β„‚)
53 fniniseg 7061 . . . . . . . . . . . . . . . . . . . . 21 (𝐹 Fn β„‚ β†’ (𝑧 ∈ (◑𝐹 β€œ {0}) ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
548, 46, 52, 534syl 19 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ (𝑧 ∈ (◑𝐹 β€œ {0}) ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
5551, 54bitrid 283 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑧 ∈ 𝑅 ↔ (𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0)))
5655simplbda 499 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (πΉβ€˜π‘§) = 0)
57 eqid 2731 . . . . . . . . . . . . . . . . . . 19 (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = (Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))
5857facth 26056 . . . . . . . . . . . . . . . . . 18 ((𝐹 ∈ (Polyβ€˜π‘†) ∧ 𝑧 ∈ β„‚ ∧ (πΉβ€˜π‘§) = 0) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
5943, 50, 56, 58syl3anc 1370 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
6029oveq2i 7423 . . . . . . . . . . . . . . . . 17 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· (𝐹 quot (Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))))
6159, 60eqtr4di 2789 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 = ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))
6261cnveqd 5875 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ◑𝐹 = β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))
6362imaeq1d 6058 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (◑𝐹 β€œ {0}) = (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}))
6416, 63eqtrid 2783 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 = (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}))
65 cnex 11195 . . . . . . . . . . . . . 14 β„‚ ∈ V
6657plyremlem 26054 . . . . . . . . . . . . . . . . 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 1141 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚))
69 plyf 25948 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚)
7068, 69syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚)
71 plyf 25948 . . . . . . . . . . . . . . 15 (𝑄 ∈ (Polyβ€˜β„‚) β†’ 𝑄:β„‚βŸΆβ„‚)
7232, 71syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄:β„‚βŸΆβ„‚)
73 ofmulrt 26032 . . . . . . . . . . . . . 14 ((β„‚ ∈ V ∧ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})):β„‚βŸΆβ„‚ ∧ 𝑄:β„‚βŸΆβ„‚) β†’ (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}) = ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})))
7465, 70, 72, 73mp3an2i 1465 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β—‘((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β€œ {0}) = ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})))
7567simp3d 1143 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) = {𝑧})
7675uneq1d 4162 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β—‘(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β€œ {0}) βˆͺ (◑𝑄 β€œ {0})) = ({𝑧} βˆͺ (◑𝑄 β€œ {0})))
7764, 74, 763eqtrd 2775 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 = ({𝑧} βˆͺ (◑𝑄 β€œ {0})))
7877fveq2d 6895 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜π‘…) = (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))))
791, 2eqtr4d 2774 . . . . . . . . . . . 12 (πœ‘ β†’ (β™―β€˜π‘…) = (𝐷 + 1))
8079adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜π‘…) = (𝐷 + 1))
8178, 80eqtr3d 2773 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (𝐷 + 1))
8215adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐹 β‰  0𝑝)
8361, 82eqnetrrd 3008 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β‰  0𝑝)
84 plymul0or 26031 . . . . . . . . . . . . . . . . . . 19 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚)) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = 0𝑝 ↔ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8568, 32, 84syl2anc 583 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) = 0𝑝 ↔ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8685necon3abid 2976 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄) β‰  0𝑝 ↔ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝)))
8783, 86mpbid 231 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
88 neanior 3034 . . . . . . . . . . . . . . . 16 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝 ∧ 𝑄 β‰  0𝑝) ↔ Β¬ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 ∨ 𝑄 = 0𝑝))
8987, 88sylibr 233 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝 ∧ 𝑄 β‰  0𝑝))
9089simprd 495 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑄 β‰  0𝑝)
91 eqid 2731 . . . . . . . . . . . . . . 15 (◑𝑄 β€œ {0}) = (◑𝑄 β€œ {0})
9291fta1 26058 . . . . . . . . . . . . . 14 ((𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝑄 β‰  0𝑝) β†’ ((◑𝑄 β€œ {0}) ∈ Fin ∧ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„)))
9332, 90, 92syl2anc 583 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((◑𝑄 β€œ {0}) ∈ Fin ∧ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„)))
9493simprd 495 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ≀ (degβ€˜π‘„))
9594, 31breqtrrd 5176 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ≀ 𝐷)
96 snfi 9048 . . . . . . . . . . . . . 14 {𝑧} ∈ Fin
9793simpld 494 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (◑𝑄 β€œ {0}) ∈ Fin)
98 hashun2 14348 . . . . . . . . . . . . . 14 (({𝑧} ∈ Fin ∧ (◑𝑄 β€œ {0}) ∈ Fin) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) ≀ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))))
9996, 97, 98sylancr 586 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) ≀ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))))
100 ax-1cn 11172 . . . . . . . . . . . . . . 15 1 ∈ β„‚
1013nncnd 12233 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐷 ∈ β„‚)
102101adantr 480 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ β„‚)
103 addcom 11405 . . . . . . . . . . . . . . 15 ((1 ∈ β„‚ ∧ 𝐷 ∈ β„‚) β†’ (1 + 𝐷) = (𝐷 + 1))
104100, 102, 103sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 + 𝐷) = (𝐷 + 1))
10581, 104eqtr4d 2774 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (1 + 𝐷))
106 hashsng 14334 . . . . . . . . . . . . . . 15 (𝑧 ∈ 𝑅 β†’ (β™―β€˜{𝑧}) = 1)
107106adantl 481 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜{𝑧}) = 1)
108107oveq1d 7427 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜{𝑧}) + (β™―β€˜(◑𝑄 β€œ {0}))) = (1 + (β™―β€˜(◑𝑄 β€œ {0}))))
10999, 105, 1083brtr3d 5179 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 + 𝐷) ≀ (1 + (β™―β€˜(◑𝑄 β€œ {0}))))
110 hashcl 14321 . . . . . . . . . . . . . . 15 ((◑𝑄 β€œ {0}) ∈ Fin β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ β„•0)
11197, 110syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ β„•0)
112111nn0red 12538 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) ∈ ℝ)
113 1red 11220 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 1 ∈ ℝ)
11436, 112, 113leadd2d 11814 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})) ↔ (1 + 𝐷) ≀ (1 + (β™―β€˜(◑𝑄 β€œ {0})))))
115109, 114mpbird 257 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})))
116112, 36letri3d 11361 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜(◑𝑄 β€œ {0})) = 𝐷 ↔ ((β™―β€˜(◑𝑄 β€œ {0})) ≀ 𝐷 ∧ 𝐷 ≀ (β™―β€˜(◑𝑄 β€œ {0})))))
11795, 115, 116mpbir2and 710 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) = 𝐷)
11881, 117eqeq12d 2747 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β™―β€˜({𝑧} βˆͺ (◑𝑄 β€œ {0}))) = (β™―β€˜(◑𝑄 β€œ {0})) ↔ (𝐷 + 1) = 𝐷))
11942, 118imbitrid 243 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑧 ∈ (◑𝑄 β€œ {0}) β†’ (𝐷 + 1) = 𝐷))
120119necon3ad 2952 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝐷 + 1) β‰  𝐷 β†’ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0})))
12138, 120mpd 15 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0}))
122 disjsn 4715 . . . . . 6 (((◑𝑄 β€œ {0}) ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ (◑𝑄 β€œ {0}))
123121, 122sylibr 233 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((◑𝑄 β€œ {0}) ∩ {𝑧}) = βˆ…)
12426, 123eqtrid 2783 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ({𝑧} ∩ (◑𝑄 β€œ {0})) = βˆ…)
12519adantr 480 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 ∈ Fin)
12649adantr 480 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑅 βŠ† β„‚)
127126sselda 3982 . . . 4 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘₯ ∈ 𝑅) β†’ π‘₯ ∈ β„‚)
128124, 77, 125, 127fsumsplit 15692 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = (Ξ£π‘₯ ∈ {𝑧}π‘₯ + Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯))
129 id 22 . . . . . . 7 (π‘₯ = 𝑧 β†’ π‘₯ = 𝑧)
130129sumsn 15697 . . . . . 6 ((𝑧 ∈ β„‚ ∧ 𝑧 ∈ β„‚) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = 𝑧)
13150, 50, 130syl2anc 583 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = 𝑧)
13250negnegd 11567 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ --𝑧 = 𝑧)
133131, 132eqtr4d 2774 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ {𝑧}π‘₯ = --𝑧)
134117, 31eqtrd 2771 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„))
135 fveq2 6891 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (degβ€˜π‘“) = (degβ€˜π‘„))
136135eqeq2d 2742 . . . . . . . . 9 (𝑓 = 𝑄 β†’ (𝐷 = (degβ€˜π‘“) ↔ 𝐷 = (degβ€˜π‘„)))
137 cnveq 5873 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ ◑𝑓 = ◑𝑄)
138137imaeq1d 6058 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ (◑𝑓 β€œ {0}) = (◑𝑄 β€œ {0}))
139138fveq2d 6895 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (β™―β€˜(◑𝑓 β€œ {0})) = (β™―β€˜(◑𝑄 β€œ {0})))
140139, 135eqeq12d 2747 . . . . . . . . 9 (𝑓 = 𝑄 β†’ ((β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“) ↔ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)))
141136, 140anbi12d 630 . . . . . . . 8 (𝑓 = 𝑄 β†’ ((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) ↔ (𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„))))
142138sumeq1d 15652 . . . . . . . . 9 (𝑓 = 𝑄 β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯)
143 fveq2 6891 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ (coeffβ€˜π‘“) = (coeffβ€˜π‘„))
144135oveq1d 7427 . . . . . . . . . . . 12 (𝑓 = 𝑄 β†’ ((degβ€˜π‘“) βˆ’ 1) = ((degβ€˜π‘„) βˆ’ 1))
145143, 144fveq12d 6898 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ ((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)))
146143, 135fveq12d 6898 . . . . . . . . . . 11 (𝑓 = 𝑄 β†’ ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
147145, 146oveq12d 7430 . . . . . . . . . 10 (𝑓 = 𝑄 β†’ (((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) = (((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
148147negeqd 11459 . . . . . . . . 9 (𝑓 = 𝑄 β†’ -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
149142, 148eqeq12d 2747 . . . . . . . 8 (𝑓 = 𝑄 β†’ (Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“))) ↔ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))))
150141, 149imbi12d 344 . . . . . . 7 (𝑓 = 𝑄 β†’ (((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)))) ↔ ((𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))))
15128adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ βˆ€π‘“ ∈ (Polyβ€˜β„‚)((𝐷 = (degβ€˜π‘“) ∧ (β™―β€˜(◑𝑓 β€œ {0})) = (degβ€˜π‘“)) β†’ Ξ£π‘₯ ∈ (◑𝑓 β€œ {0})π‘₯ = -(((coeffβ€˜π‘“)β€˜((degβ€˜π‘“) βˆ’ 1)) / ((coeffβ€˜π‘“)β€˜(degβ€˜π‘“)))))
152150, 151, 32rspcdva 3613 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝐷 = (degβ€˜π‘„) ∧ (β™―β€˜(◑𝑄 β€œ {0})) = (degβ€˜π‘„)) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))))
15331, 134, 152mp2and 696 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
15431fvoveq1d 7434 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)))
15561fveq2d 6895 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜πΉ) = (coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15627, 155eqtrid 2783 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐴 = (coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15761fveq2d 6895 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜πΉ) = (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)))
15867simp2d 1142 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 1)
159 ax-1ne0 11183 . . . . . . . . . . . . . . 15 1 β‰  0
160159a1i 11 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 1 β‰  0)
161158, 160eqnetrd 3007 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) β‰  0)
162 fveq2 6891 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (degβ€˜0𝑝))
163162, 12eqtrdi 2787 . . . . . . . . . . . . . 14 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) = 0𝑝 β†’ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = 0)
164163necon3i 2972 . . . . . . . . . . . . 13 ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) β‰  0 β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝)
165161, 164syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝)
166 eqid 2731 . . . . . . . . . . . . 13 (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))
167 eqid 2731 . . . . . . . . . . . . 13 (degβ€˜π‘„) = (degβ€˜π‘„)
168166, 167dgrmul 26021 . . . . . . . . . . . 12 ((((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ (Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) β‰  0𝑝) ∧ (𝑄 ∈ (Polyβ€˜β„‚) ∧ 𝑄 β‰  0𝑝)) β†’ (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
16968, 165, 32, 90, 168syl22anc 836 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄)) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
170157, 169eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (degβ€˜πΉ) = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
1719, 170eqtrid 2783 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝑁 = ((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„)))
172156, 171fveq12d 6898 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) = ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))))
173 eqid 2731 . . . . . . . . . 10 (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))
174 eqid 2731 . . . . . . . . . 10 (coeffβ€˜π‘„) = (coeffβ€˜π‘„)
175173, 174, 166, 167coemulhi 26004 . . . . . . . . 9 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚)) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
17668, 32, 175syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜((degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) + (degβ€˜π‘„))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
177158fveq2d 6895 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1))
178 ssid 4004 . . . . . . . . . . . . . . 15 β„‚ βŠ† β„‚
179 plyid 25959 . . . . . . . . . . . . . . 15 ((β„‚ βŠ† β„‚ ∧ 1 ∈ β„‚) β†’ Xp ∈ (Polyβ€˜β„‚))
180178, 100, 179mp2an 689 . . . . . . . . . . . . . 14 Xp ∈ (Polyβ€˜β„‚)
181 plyconst 25956 . . . . . . . . . . . . . . 15 ((β„‚ βŠ† β„‚ ∧ 𝑧 ∈ β„‚) β†’ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚))
182178, 50, 181sylancr 586 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚))
183 eqid 2731 . . . . . . . . . . . . . . 15 (coeffβ€˜Xp) = (coeffβ€˜Xp)
184 eqid 2731 . . . . . . . . . . . . . . 15 (coeffβ€˜(β„‚ Γ— {𝑧})) = (coeffβ€˜(β„‚ Γ— {𝑧}))
185183, 184coesub 26007 . . . . . . . . . . . . . 14 ((Xp ∈ (Polyβ€˜β„‚) ∧ (β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚)) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = ((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧}))))
186180, 182, 185sylancr 586 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) = ((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧}))))
187186fveq1d 6893 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) = (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1))
188 1nn0 12493 . . . . . . . . . . . . . 14 1 ∈ β„•0
189183coef3 25982 . . . . . . . . . . . . . . . . 17 (Xp ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜Xp):β„•0βŸΆβ„‚)
190 ffn 6717 . . . . . . . . . . . . . . . . 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 25982 . . . . . . . . . . . . . . . 16 ((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜(β„‚ Γ— {𝑧})):β„•0βŸΆβ„‚)
194 ffn 6717 . . . . . . . . . . . . . . . 16 ((coeffβ€˜(β„‚ Γ— {𝑧})):β„•0βŸΆβ„‚ β†’ (coeffβ€˜(β„‚ Γ— {𝑧})) Fn β„•0)
195182, 193, 1943syl 18 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(β„‚ Γ— {𝑧})) Fn β„•0)
196 nn0ex 12483 . . . . . . . . . . . . . . . 16 β„•0 ∈ V
197196a1i 11 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ β„•0 ∈ V)
198 inidm 4218 . . . . . . . . . . . . . . 15 (β„•0 ∩ β„•0) = β„•0
199 coeidp 26014 . . . . . . . . . . . . . . . . 17 (1 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜1) = if(1 = 1, 1, 0))
200199adantl 481 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜1) = if(1 = 1, 1, 0))
201 eqid 2731 . . . . . . . . . . . . . . . . 17 1 = 1
202201iftruei 4535 . . . . . . . . . . . . . . . 16 if(1 = 1, 1, 0) = 1
203200, 202eqtrdi 2787 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜1) = 1)
204 0lt1 11741 . . . . . . . . . . . . . . . . . 18 0 < 1
205 0re 11221 . . . . . . . . . . . . . . . . . . 19 0 ∈ ℝ
206 1re 11219 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ
207205, 206ltnlei 11340 . . . . . . . . . . . . . . . . . 18 (0 < 1 ↔ Β¬ 1 ≀ 0)
208204, 207mpbi 229 . . . . . . . . . . . . . . . . 17 Β¬ 1 ≀ 0
20950adantr 480 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ 𝑧 ∈ β„‚)
210 0dgr 25995 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ β„‚ β†’ (degβ€˜(β„‚ Γ— {𝑧})) = 0)
211209, 210syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (degβ€˜(β„‚ Γ— {𝑧})) = 0)
212211breq2d 5160 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (1 ≀ (degβ€˜(β„‚ Γ— {𝑧})) ↔ 1 ≀ 0))
213208, 212mtbiri 327 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ Β¬ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})))
214 eqid 2731 . . . . . . . . . . . . . . . . . . . 20 (degβ€˜(β„‚ Γ— {𝑧})) = (degβ€˜(β„‚ Γ— {𝑧}))
215184, 214dgrub 25984 . . . . . . . . . . . . . . . . . . 19 (((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) ∧ 1 ∈ β„•0 ∧ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0) β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})))
2162153expia 1120 . . . . . . . . . . . . . . . . . 18 (((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0 β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧}))))
217182, 216sylan 579 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) β‰  0 β†’ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧}))))
218217necon1bd 2957 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (Β¬ 1 ≀ (degβ€˜(β„‚ Γ— {𝑧})) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) = 0))
219213, 218mpd 15 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜1) = 0)
220192, 195, 197, 197, 198, 203, 219ofval 7685 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 1 ∈ β„•0) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = (1 βˆ’ 0))
221188, 220mpan2 688 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = (1 βˆ’ 0))
222 1m0e1 12338 . . . . . . . . . . . . 13 (1 βˆ’ 0) = 1
223221, 222eqtrdi 2787 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜1) = 1)
224187, 223eqtrd 2771 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) = 1)
225177, 224eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) = 1)
226225oveq1d 7427 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = (1 Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
227174coef3 25982 . . . . . . . . . . . 12 (𝑄 ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜π‘„):β„•0βŸΆβ„‚)
22832, 227syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜π‘„):β„•0βŸΆβ„‚)
229228, 34ffvelcdmd 7087 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)) ∈ β„‚)
230229mullidd 11237 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
231226, 230eqtrd 2771 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜(degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))) Β· ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
232172, 176, 2313eqtrd 2775 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
233154, 232oveq12d 7430 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) = (((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
234233negeqd 11459 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) = -(((coeffβ€˜π‘„)β€˜((degβ€˜π‘„) βˆ’ 1)) / ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„))))
235153, 234eqtr4d 2774 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯ = -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)))
236133, 235oveq12d 7430 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Ξ£π‘₯ ∈ {𝑧}π‘₯ + Ξ£π‘₯ ∈ (◑𝑄 β€œ {0})π‘₯) = (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
23750negcld 11563 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -𝑧 ∈ β„‚)
238 nnm1nn0 12518 . . . . . . . . 9 (𝐷 ∈ β„• β†’ (𝐷 βˆ’ 1) ∈ β„•0)
2393, 238syl 17 . . . . . . . 8 (πœ‘ β†’ (𝐷 βˆ’ 1) ∈ β„•0)
240239adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 βˆ’ 1) ∈ β„•0)
241228, 240ffvelcdmd 7087 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) ∈ β„‚)
242232, 229eqeltrd 2832 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) ∈ β„‚)
2439, 27dgreq0 26016 . . . . . . . . 9 (𝐹 ∈ (Polyβ€˜π‘†) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
24443, 243syl 17 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐹 = 0𝑝 ↔ (π΄β€˜π‘) = 0))
245244necon3bid 2984 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐹 β‰  0𝑝 ↔ (π΄β€˜π‘) β‰  0))
24682, 245mpbid 231 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜π‘) β‰  0)
247241, 242, 246divcld 11995 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘)) ∈ β„‚)
248237, 247negdid 11589 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
249237, 242mulcld 11239 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (-𝑧 Β· (π΄β€˜π‘)) ∈ β„‚)
250249, 241, 242, 246divdird 12033 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) / (π΄β€˜π‘)) = (((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
251 nnm1nn0 12518 . . . . . . . . . . 11 (𝑁 ∈ β„• β†’ (𝑁 βˆ’ 1) ∈ β„•0)
2525, 251syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝑁 βˆ’ 1) ∈ β„•0)
253252adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ β„•0)
254173, 174coemul 26002 . . . . . . . . 9 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ 𝑄 ∈ (Polyβ€˜β„‚) ∧ (𝑁 βˆ’ 1) ∈ β„•0) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
25568, 32, 253, 254syl3anc 1370 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
256156fveq1d 6893 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π΄β€˜(𝑁 βˆ’ 1)) = ((coeffβ€˜((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∘f Β· 𝑄))β€˜(𝑁 βˆ’ 1)))
257 1e0p1 12724 . . . . . . . . . . . 12 1 = (0 + 1)
258257oveq2i 7423 . . . . . . . . . . 11 (0...1) = (0...(0 + 1))
259258sumeq1i 15649 . . . . . . . . . 10 Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = Ξ£π‘˜ ∈ (0...(0 + 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)))
260 0nn0 12492 . . . . . . . . . . . . 13 0 ∈ β„•0
261 nn0uz 12869 . . . . . . . . . . . . 13 β„•0 = (β„€β‰₯β€˜0)
262260, 261eleqtri 2830 . . . . . . . . . . . 12 0 ∈ (β„€β‰₯β€˜0)
263262a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 0 ∈ (β„€β‰₯β€˜0))
264258eleq2i 2824 . . . . . . . . . . . 12 (π‘˜ ∈ (0...1) ↔ π‘˜ ∈ (0...(0 + 1)))
265173coef3 25982 . . . . . . . . . . . . . . 15 ((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚)
26668, 265syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚)
267 elfznn0 13599 . . . . . . . . . . . . . 14 (π‘˜ ∈ (0...1) β†’ π‘˜ ∈ β„•0)
268 ffvelcdm 7083 . . . . . . . . . . . . . 14 (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))):β„•0βŸΆβ„‚ ∧ π‘˜ ∈ β„•0) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) ∈ β„‚)
269266, 267, 268syl2an 595 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) ∈ β„‚)
2702oveq1d 7427 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐷 + 1) βˆ’ 1) = (𝑁 βˆ’ 1))
271 pncan 11471 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((𝐷 + 1) βˆ’ 1) = 𝐷)
272101, 100, 271sylancl 585 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐷 + 1) βˆ’ 1) = 𝐷)
273270, 272eqtr3d 2773 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝑁 βˆ’ 1) = 𝐷)
274273adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) = 𝐷)
2753adantr 480 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ 𝐷 ∈ β„•)
276274, 275eqeltrd 2832 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ β„•)
277 nnuz 12870 . . . . . . . . . . . . . . . . 17 β„• = (β„€β‰₯β€˜1)
278276, 277eleqtrdi 2842 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜1))
279 fzss2 13546 . . . . . . . . . . . . . . . 16 ((𝑁 βˆ’ 1) ∈ (β„€β‰₯β€˜1) β†’ (0...1) βŠ† (0...(𝑁 βˆ’ 1)))
280278, 279syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (0...1) βŠ† (0...(𝑁 βˆ’ 1)))
281280sselda 3982 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ π‘˜ ∈ (0...(𝑁 βˆ’ 1)))
282 fznn0sub 13538 . . . . . . . . . . . . . . 15 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) ∈ β„•0)
283 ffvelcdm 7083 . . . . . . . . . . . . . . 15 (((coeffβ€˜π‘„):β„•0βŸΆβ„‚ ∧ ((𝑁 βˆ’ 1) βˆ’ π‘˜) ∈ β„•0) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
284228, 282, 283syl2an 595 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...(𝑁 βˆ’ 1))) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
285281, 284syldan 590 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
286269, 285mulcld 11239 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...1)) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) ∈ β„‚)
287264, 286sylan2br 594 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ (0...(0 + 1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) ∈ β„‚)
288 id 22 . . . . . . . . . . . . . 14 (π‘˜ = (0 + 1) β†’ π‘˜ = (0 + 1))
289288, 257eqtr4di 2789 . . . . . . . . . . . . 13 (π‘˜ = (0 + 1) β†’ π‘˜ = 1)
290289fveq2d 6895 . . . . . . . . . . . 12 (π‘˜ = (0 + 1) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1))
291289oveq2d 7428 . . . . . . . . . . . . 13 (π‘˜ = (0 + 1) β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) = ((𝑁 βˆ’ 1) βˆ’ 1))
292291fveq2d 6895 . . . . . . . . . . . 12 (π‘˜ = (0 + 1) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) = ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))
293290, 292oveq12d 7430 . . . . . . . . . . 11 (π‘˜ = (0 + 1) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))))
294263, 287, 293fsump1 15707 . . . . . . . . . 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 2783 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))))
296 eldifn 4127 . . . . . . . . . . . . . 14 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ Β¬ π‘˜ ∈ (0...1))
297296adantl 481 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ Β¬ π‘˜ ∈ (0...1))
298 eldifi 4126 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ (0...(𝑁 βˆ’ 1)))
299 elfznn0 13599 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ π‘˜ ∈ β„•0)
300298, 299syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ β„•0)
301173, 166dgrub 25984 . . . . . . . . . . . . . . . . 17 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ π‘˜ ∈ β„•0 ∧ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0) β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))))
3023013expia 1120 . . . . . . . . . . . . . . . 16 (((Xp ∘f βˆ’ (β„‚ Γ— {𝑧})) ∈ (Polyβ€˜β„‚) ∧ π‘˜ ∈ β„•0) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
30368, 300, 302syl2an 595 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) β‰  0 β†’ π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))))
304 elfzuz 13502 . . . . . . . . . . . . . . . . . . 19 (π‘˜ ∈ (0...(𝑁 βˆ’ 1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
305298, 304syl 17 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1)) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
306305adantl 481 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ π‘˜ ∈ (β„€β‰₯β€˜0))
307 1z 12597 . . . . . . . . . . . . . . . . 17 1 ∈ β„€
308 elfz5 13498 . . . . . . . . . . . . . . . . 17 ((π‘˜ ∈ (β„€β‰₯β€˜0) ∧ 1 ∈ β„€) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ 1))
309306, 307, 308sylancl 585 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (π‘˜ ∈ (0...1) ↔ π‘˜ ≀ 1))
310158breq2d 5160 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (π‘˜ ≀ (degβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧}))) ↔ π‘˜ ≀ 1))
311310adantr 480 . . . . . . . . . . . . . . . 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 2957 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (Β¬ π‘˜ ∈ (0...1) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = 0))
315297, 314mpd 15 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = 0)
316315oveq1d 7427 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (0 Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
317298, 284sylan2 592 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) ∈ β„‚)
318317mul02d 11417 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (0 Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = 0)
319316, 318eqtrd 2771 . . . . . . . . . 10 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ π‘˜ ∈ ((0...(𝑁 βˆ’ 1)) βˆ– (0...1))) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = 0)
320 fzfid 13943 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (0...(𝑁 βˆ’ 1)) ∈ Fin)
321280, 286, 319, 320fsumss 15676 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...1)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
322 0z 12574 . . . . . . . . . . . 12 0 ∈ β„€
323186fveq1d 6893 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) = (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0))
324 coeidp 26014 . . . . . . . . . . . . . . . . . . . 20 (0 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜0) = if(0 = 1, 1, 0))
325159nesymi 2997 . . . . . . . . . . . . . . . . . . . . 21 Β¬ 0 = 1
326325iffalsei 4538 . . . . . . . . . . . . . . . . . . . 20 if(0 = 1, 1, 0) = 0
327324, 326eqtrdi 2787 . . . . . . . . . . . . . . . . . . 19 (0 ∈ β„•0 β†’ ((coeffβ€˜Xp)β€˜0) = 0)
328327adantl 481 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ ((coeffβ€˜Xp)β€˜0) = 0)
329184coefv0 25998 . . . . . . . . . . . . . . . . . . . . 21 ((β„‚ Γ— {𝑧}) ∈ (Polyβ€˜β„‚) β†’ ((β„‚ Γ— {𝑧})β€˜0) = ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0))
330182, 329syl 17 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((β„‚ Γ— {𝑧})β€˜0) = ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0))
331 0cn 11211 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ β„‚
332 vex 3477 . . . . . . . . . . . . . . . . . . . . . 22 𝑧 ∈ V
333332fvconst2 7207 . . . . . . . . . . . . . . . . . . . . 21 (0 ∈ β„‚ β†’ ((β„‚ Γ— {𝑧})β€˜0) = 𝑧)
334331, 333ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 ((β„‚ Γ— {𝑧})β€˜0) = 𝑧
335330, 334eqtr3di 2786 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0) = 𝑧)
336335adantr 480 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ ((coeffβ€˜(β„‚ Γ— {𝑧}))β€˜0) = 𝑧)
337192, 195, 197, 197, 198, 328, 336ofval 7685 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑧 ∈ 𝑅) ∧ 0 ∈ β„•0) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = (0 βˆ’ 𝑧))
338260, 337mpan2 688 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = (0 βˆ’ 𝑧))
339 df-neg 11452 . . . . . . . . . . . . . . . 16 -𝑧 = (0 βˆ’ 𝑧)
340338, 339eqtr4di 2789 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜Xp) ∘f βˆ’ (coeffβ€˜(β„‚ Γ— {𝑧})))β€˜0) = -𝑧)
341323, 340eqtrd 2771 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) = -𝑧)
342274oveq1d 7427 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝑁 βˆ’ 1) βˆ’ 0) = (𝐷 βˆ’ 0))
343102subid1d 11565 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (𝐷 βˆ’ 0) = 𝐷)
344342, 343, 313eqtrd 2775 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((𝑁 βˆ’ 1) βˆ’ 0) = (degβ€˜π‘„))
345344fveq2d 6895 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)) = ((coeffβ€˜π‘„)β€˜(degβ€˜π‘„)))
346345, 232eqtr4d 2774 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)) = (π΄β€˜π‘))
347341, 346oveq12d 7430 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) = (-𝑧 Β· (π΄β€˜π‘)))
348347, 249eqeltrd 2832 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))) ∈ β„‚)
349 fveq2 6891 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) = ((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0))
350 oveq2 7420 . . . . . . . . . . . . . . 15 (π‘˜ = 0 β†’ ((𝑁 βˆ’ 1) βˆ’ π‘˜) = ((𝑁 βˆ’ 1) βˆ’ 0))
351350fveq2d 6895 . . . . . . . . . . . . . 14 (π‘˜ = 0 β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜)) = ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0)))
352349, 351oveq12d 7430 . . . . . . . . . . . . 13 (π‘˜ = 0 β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
353352fsum1 15698 . . . . . . . . . . . 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 586 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜0) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 0))))
355354, 347eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) = (-𝑧 Β· (π΄β€˜π‘)))
356274fvoveq1d 7434 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
357224, 356oveq12d 7430 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))) = (1 Β· ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))))
358241mullidd 11237 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (1 Β· ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
359357, 358eqtrd 2771 . . . . . . . . . 10 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1))) = ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)))
360355, 359oveq12d 7430 . . . . . . . . 9 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (Ξ£π‘˜ ∈ (0...0)(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))) + (((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜1) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ 1)))) = ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))))
361295, 321, 3603eqtr3rd 2780 . . . . . . . 8 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = Ξ£π‘˜ ∈ (0...(𝑁 βˆ’ 1))(((coeffβ€˜(Xp ∘f βˆ’ (β„‚ Γ— {𝑧})))β€˜π‘˜) Β· ((coeffβ€˜π‘„)β€˜((𝑁 βˆ’ 1) βˆ’ π‘˜))))
362255, 256, 3613eqtr4rd 2782 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) = (π΄β€˜(𝑁 βˆ’ 1)))
363362oveq1d 7427 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) + ((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1))) / (π΄β€˜π‘)) = ((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
364237, 242, 246divcan4d 12001 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ ((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) = -𝑧)
365364oveq1d 7427 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (((-𝑧 Β· (π΄β€˜π‘)) / (π΄β€˜π‘)) + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = (-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))))
366250, 363, 3653eqtr3rd 2780 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = ((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
367366negeqd 11459 . . . 4 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ -(-𝑧 + (((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
368248, 367eqtr3d 2773 . . 3 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ (--𝑧 + -(((coeffβ€˜π‘„)β€˜(𝐷 βˆ’ 1)) / (π΄β€˜π‘))) = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
369128, 236, 3683eqtrd 2775 . 2 ((πœ‘ ∧ 𝑧 ∈ 𝑅) β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
37025, 369exlimddv 1937 1 (πœ‘ β†’ Ξ£π‘₯ ∈ 𝑅 π‘₯ = -((π΄β€˜(𝑁 βˆ’ 1)) / (π΄β€˜π‘)))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 844   ∧ w3a 1086   = wceq 1540  βˆƒwex 1780   ∈ wcel 2105   β‰  wne 2939  βˆ€wral 3060  Vcvv 3473   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528  {csn 4628   class class class wbr 5148   Γ— cxp 5674  β—‘ccnv 5675  dom cdm 5676   β€œ cima 5679   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7412   ∘f cof 7672  Fincfn 8943  β„‚cc 11112  β„cr 11113  0cc0 11114  1c1 11115   + caddc 11117   Β· cmul 11119   < clt 11253   ≀ cle 11254   βˆ’ cmin 11449  -cneg 11450   / cdiv 11876  β„•cn 12217  β„•0cn0 12477  β„€cz 12563  β„€β‰₯cuz 12827  ...cfz 13489  β™―chash 14295  Ξ£csu 15637  0𝑝c0p 25419  Polycply 25934  Xpcidp 25935  coeffccoe 25936  degcdgr 25937   quot cquot 26040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-inf2 9640  ax-cnex 11170  ax-resscn 11171  ax-1cn 11172  ax-icn 11173  ax-addcl 11174  ax-addrcl 11175  ax-mulcl 11176  ax-mulrcl 11177  ax-mulcom 11178  ax-addass 11179  ax-mulass 11180  ax-distr 11181  ax-i2m1 11182  ax-1ne0 11183  ax-1rid 11184  ax-rnegex 11185  ax-rrecex 11186  ax-cnre 11187  ax-pre-lttri 11188  ax-pre-lttrn 11189  ax-pre-ltadd 11190  ax-pre-mulgt0 11191  ax-pre-sup 11192
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-of 7674  df-om 7860  df-1st 7979  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-oadd 8474  df-er 8707  df-map 8826  df-pm 8827  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-sup 9441  df-inf 9442  df-oi 9509  df-dju 9900  df-card 9938  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-n0 12478  df-xnn0 12550  df-z 12564  df-uz 12828  df-rp 12980  df-fz 13490  df-fzo 13633  df-fl 13762  df-seq 13972  df-exp 14033  df-hash 14296  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-clim 15437  df-rlim 15438  df-sum 15638  df-0p 25420  df-ply 25938  df-idp 25939  df-coe 25940  df-dgr 25941  df-quot 26041
This theorem is referenced by:  vieta1  26062
  Copyright terms: Public domain W3C validator