Metamath Proof Explorer

Theorem vieta1lem2

Description: Lemma for vieta1 : inductive step. Let z be a root of F . Then F = ( Xp - z ) x. Q for some Q by the factor theorem, and Q is a degree- D polynomial, so by the induction hypothesis sum_ x e. (`' Q " 0 ) x = -u ( coeff `Q )( D - 1 ) / ( coeffQ )D , so sum_ x e. R x = z - ( coeffQ )` ` ( D - 1 ) / ( coeffQ )D . Now the coefficients of F are A( D + 1 ) = ( coeffQ )D and AD = sum_ k e. ( 0 ... D ) ( coeffXp - z )k x. ( coeffQ ) ` `( D - k ) , which works out to -u z x. ( coeffQ )D + ( coeffQ )( D - 1 ) , so putting it all together we have sum_ x e. R x = -u AD / A( D + 1 ) as we wanted to show. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses vieta1.1 
|- A = ( coeff ` F )
vieta1.2 
|- N = ( deg ` F )
vieta1.3 
|- R = ( `' F " { 0 } )
vieta1.4 
|- ( ph -> F e. ( Poly ` S ) )
vieta1.5 
|- ( ph -> ( # ` R ) = N )
vieta1lem.6 
|- ( ph -> D e. NN )
vieta1lem.7 
|- ( ph -> ( D + 1 ) = N )
vieta1lem.8 
|- ( ph -> A. f e. ( Poly ` CC ) ( ( D = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
vieta1lem.9 
|- Q = ( F quot ( Xp oF - ( CC X. { z } ) ) )
Assertion vieta1lem2 
|- ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )

Proof

Step Hyp Ref Expression
1 vieta1.1 
 |-  A = ( coeff ` F )
2 vieta1.2 
 |-  N = ( deg ` F )
3 vieta1.3 
 |-  R = ( `' F " { 0 } )
4 vieta1.4 
 |-  ( ph -> F e. ( Poly ` S ) )
5 vieta1.5 
 |-  ( ph -> ( # ` R ) = N )
6 vieta1lem.6 
 |-  ( ph -> D e. NN )
7 vieta1lem.7 
 |-  ( ph -> ( D + 1 ) = N )
8 vieta1lem.8 
 |-  ( ph -> A. f e. ( Poly ` CC ) ( ( D = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
9 vieta1lem.9 
 |-  Q = ( F quot ( Xp oF - ( CC X. { z } ) ) )
10 6 peano2nnd 
 |-  ( ph -> ( D + 1 ) e. NN )
11 7 10 eqeltrrd 
 |-  ( ph -> N e. NN )
12 11 nnne0d 
 |-  ( ph -> N =/= 0 )
13 5 12 eqnetrd 
 |-  ( ph -> ( # ` R ) =/= 0 )
14 2 12 eqnetrrid 
 |-  ( ph -> ( deg ` F ) =/= 0 )
15 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
16 dgr0 
 |-  ( deg ` 0p ) = 0
17 15 16 eqtrdi 
 |-  ( F = 0p -> ( deg ` F ) = 0 )
18 17 necon3i 
 |-  ( ( deg ` F ) =/= 0 -> F =/= 0p )
19 14 18 syl 
 |-  ( ph -> F =/= 0p )
20 3 fta1 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) )
21 4 19 20 syl2anc 
 |-  ( ph -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) )
22 21 simpld 
 |-  ( ph -> R e. Fin )
23 hasheq0 
 |-  ( R e. Fin -> ( ( # ` R ) = 0 <-> R = (/) ) )
24 22 23 syl 
 |-  ( ph -> ( ( # ` R ) = 0 <-> R = (/) ) )
25 24 necon3bid 
 |-  ( ph -> ( ( # ` R ) =/= 0 <-> R =/= (/) ) )
26 13 25 mpbid 
 |-  ( ph -> R =/= (/) )
27 n0 
 |-  ( R =/= (/) <-> E. z z e. R )
28 26 27 sylib 
 |-  ( ph -> E. z z e. R )
29 incom 
 |-  ( { z } i^i ( `' Q " { 0 } ) ) = ( ( `' Q " { 0 } ) i^i { z } )
30 1 2 3 4 5 6 7 8 9 vieta1lem1 
 |-  ( ( ph /\ z e. R ) -> ( Q e. ( Poly ` CC ) /\ D = ( deg ` Q ) ) )
31 30 simprd 
 |-  ( ( ph /\ z e. R ) -> D = ( deg ` Q ) )
32 30 simpld 
 |-  ( ( ph /\ z e. R ) -> Q e. ( Poly ` CC ) )
33 dgrcl 
 |-  ( Q e. ( Poly ` CC ) -> ( deg ` Q ) e. NN0 )
34 32 33 syl 
 |-  ( ( ph /\ z e. R ) -> ( deg ` Q ) e. NN0 )
35 34 nn0red 
 |-  ( ( ph /\ z e. R ) -> ( deg ` Q ) e. RR )
36 31 35 eqeltrd 
 |-  ( ( ph /\ z e. R ) -> D e. RR )
37 36 ltp1d 
 |-  ( ( ph /\ z e. R ) -> D < ( D + 1 ) )
38 36 37 gtned 
 |-  ( ( ph /\ z e. R ) -> ( D + 1 ) =/= D )
39 snssi 
 |-  ( z e. ( `' Q " { 0 } ) -> { z } C_ ( `' Q " { 0 } ) )
40 ssequn1 
 |-  ( { z } C_ ( `' Q " { 0 } ) <-> ( { z } u. ( `' Q " { 0 } ) ) = ( `' Q " { 0 } ) )
41 39 40 sylib 
 |-  ( z e. ( `' Q " { 0 } ) -> ( { z } u. ( `' Q " { 0 } ) ) = ( `' Q " { 0 } ) )
42 41 fveq2d 
 |-  ( z e. ( `' Q " { 0 } ) -> ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) = ( # ` ( `' Q " { 0 } ) ) )
43 4 adantr 
 |-  ( ( ph /\ z e. R ) -> F e. ( Poly ` S ) )
44 cnvimass 
 |-  ( `' F " { 0 } ) C_ dom F
45 3 44 eqsstri 
 |-  R C_ dom F
46 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
47 fdm 
 |-  ( F : CC --> CC -> dom F = CC )
48 4 46 47 3syl 
 |-  ( ph -> dom F = CC )
49 45 48 sseqtrid 
 |-  ( ph -> R C_ CC )
50 49 sselda 
 |-  ( ( ph /\ z e. R ) -> z e. CC )
51 3 eleq2i 
 |-  ( z e. R <-> z e. ( `' F " { 0 } ) )
52 ffn 
 |-  ( F : CC --> CC -> F Fn CC )
53 fniniseg 
 |-  ( F Fn CC -> ( z e. ( `' F " { 0 } ) <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
54 4 46 52 53 4syl 
 |-  ( ph -> ( z e. ( `' F " { 0 } ) <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
55 51 54 bitrid 
 |-  ( ph -> ( z e. R <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
56 55 simplbda 
 |-  ( ( ph /\ z e. R ) -> ( F ` z ) = 0 )
57 eqid 
 |-  ( Xp oF - ( CC X. { z } ) ) = ( Xp oF - ( CC X. { z } ) )
58 57 facth 
 |-  ( ( F e. ( Poly ` S ) /\ z e. CC /\ ( F ` z ) = 0 ) -> F = ( ( Xp oF - ( CC X. { z } ) ) oF x. ( F quot ( Xp oF - ( CC X. { z } ) ) ) ) )
59 43 50 56 58 syl3anc 
 |-  ( ( ph /\ z e. R ) -> F = ( ( Xp oF - ( CC X. { z } ) ) oF x. ( F quot ( Xp oF - ( CC X. { z } ) ) ) ) )
60 9 oveq2i 
 |-  ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) = ( ( Xp oF - ( CC X. { z } ) ) oF x. ( F quot ( Xp oF - ( CC X. { z } ) ) ) )
61 59 60 eqtr4di 
 |-  ( ( ph /\ z e. R ) -> F = ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) )
62 61 cnveqd 
 |-  ( ( ph /\ z e. R ) -> `' F = `' ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) )
63 62 imaeq1d 
 |-  ( ( ph /\ z e. R ) -> ( `' F " { 0 } ) = ( `' ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) " { 0 } ) )
64 3 63 eqtrid 
 |-  ( ( ph /\ z e. R ) -> R = ( `' ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) " { 0 } ) )
65 cnex 
 |-  CC e. _V
66 57 plyremlem 
 |-  ( z e. CC -> ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { z } ) ) " { 0 } ) = { z } ) )
67 50 66 syl 
 |-  ( ( ph /\ z e. R ) -> ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { z } ) ) " { 0 } ) = { z } ) )
68 67 simp1d 
 |-  ( ( ph /\ z e. R ) -> ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) )
69 plyf 
 |-  ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) -> ( Xp oF - ( CC X. { z } ) ) : CC --> CC )
70 68 69 syl 
 |-  ( ( ph /\ z e. R ) -> ( Xp oF - ( CC X. { z } ) ) : CC --> CC )
71 plyf 
 |-  ( Q e. ( Poly ` CC ) -> Q : CC --> CC )
72 32 71 syl 
 |-  ( ( ph /\ z e. R ) -> Q : CC --> CC )
73 ofmulrt 
 |-  ( ( CC e. _V /\ ( Xp oF - ( CC X. { z } ) ) : CC --> CC /\ Q : CC --> CC ) -> ( `' ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) " { 0 } ) = ( ( `' ( Xp oF - ( CC X. { z } ) ) " { 0 } ) u. ( `' Q " { 0 } ) ) )
74 65 70 72 73 mp3an2i 
 |-  ( ( ph /\ z e. R ) -> ( `' ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) " { 0 } ) = ( ( `' ( Xp oF - ( CC X. { z } ) ) " { 0 } ) u. ( `' Q " { 0 } ) ) )
75 67 simp3d 
 |-  ( ( ph /\ z e. R ) -> ( `' ( Xp oF - ( CC X. { z } ) ) " { 0 } ) = { z } )
76 75 uneq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( `' ( Xp oF - ( CC X. { z } ) ) " { 0 } ) u. ( `' Q " { 0 } ) ) = ( { z } u. ( `' Q " { 0 } ) ) )
77 64 74 76 3eqtrd 
 |-  ( ( ph /\ z e. R ) -> R = ( { z } u. ( `' Q " { 0 } ) ) )
78 77 fveq2d 
 |-  ( ( ph /\ z e. R ) -> ( # ` R ) = ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) )
79 5 7 eqtr4d 
 |-  ( ph -> ( # ` R ) = ( D + 1 ) )
80 79 adantr 
 |-  ( ( ph /\ z e. R ) -> ( # ` R ) = ( D + 1 ) )
81 78 80 eqtr3d 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) = ( D + 1 ) )
82 19 adantr 
 |-  ( ( ph /\ z e. R ) -> F =/= 0p )
83 61 82 eqnetrrd 
 |-  ( ( ph /\ z e. R ) -> ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) =/= 0p )
84 plymul0or 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ Q e. ( Poly ` CC ) ) -> ( ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) = 0p <-> ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) ) )
85 68 32 84 syl2anc 
 |-  ( ( ph /\ z e. R ) -> ( ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) = 0p <-> ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) ) )
86 85 necon3abid 
 |-  ( ( ph /\ z e. R ) -> ( ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) =/= 0p <-> -. ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) ) )
87 83 86 mpbid 
 |-  ( ( ph /\ z e. R ) -> -. ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) )
88 neanior 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) =/= 0p /\ Q =/= 0p ) <-> -. ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) )
89 87 88 sylibr 
 |-  ( ( ph /\ z e. R ) -> ( ( Xp oF - ( CC X. { z } ) ) =/= 0p /\ Q =/= 0p ) )
90 89 simprd 
 |-  ( ( ph /\ z e. R ) -> Q =/= 0p )
91 eqid 
 |-  ( `' Q " { 0 } ) = ( `' Q " { 0 } )
92 91 fta1 
 |-  ( ( Q e. ( Poly ` CC ) /\ Q =/= 0p ) -> ( ( `' Q " { 0 } ) e. Fin /\ ( # ` ( `' Q " { 0 } ) ) <_ ( deg ` Q ) ) )
93 32 90 92 syl2anc 
 |-  ( ( ph /\ z e. R ) -> ( ( `' Q " { 0 } ) e. Fin /\ ( # ` ( `' Q " { 0 } ) ) <_ ( deg ` Q ) ) )
94 93 simprd 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( `' Q " { 0 } ) ) <_ ( deg ` Q ) )
95 94 31 breqtrrd 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( `' Q " { 0 } ) ) <_ D )
96 snfi 
 |-  { z } e. Fin
97 93 simpld 
 |-  ( ( ph /\ z e. R ) -> ( `' Q " { 0 } ) e. Fin )
98 hashun2 
 |-  ( ( { z } e. Fin /\ ( `' Q " { 0 } ) e. Fin ) -> ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) <_ ( ( # ` { z } ) + ( # ` ( `' Q " { 0 } ) ) ) )
99 96 97 98 sylancr 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) <_ ( ( # ` { z } ) + ( # ` ( `' Q " { 0 } ) ) ) )
100 ax-1cn 
 |-  1 e. CC
101 6 nncnd 
 |-  ( ph -> D e. CC )
102 101 adantr 
 |-  ( ( ph /\ z e. R ) -> D e. CC )
103 addcom 
 |-  ( ( 1 e. CC /\ D e. CC ) -> ( 1 + D ) = ( D + 1 ) )
104 100 102 103 sylancr 
 |-  ( ( ph /\ z e. R ) -> ( 1 + D ) = ( D + 1 ) )
105 81 104 eqtr4d 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) = ( 1 + D ) )
106 hashsng 
 |-  ( z e. R -> ( # ` { z } ) = 1 )
107 106 adantl 
 |-  ( ( ph /\ z e. R ) -> ( # ` { z } ) = 1 )
108 107 oveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( # ` { z } ) + ( # ` ( `' Q " { 0 } ) ) ) = ( 1 + ( # ` ( `' Q " { 0 } ) ) ) )
109 99 105 108 3brtr3d 
 |-  ( ( ph /\ z e. R ) -> ( 1 + D ) <_ ( 1 + ( # ` ( `' Q " { 0 } ) ) ) )
110 hashcl 
 |-  ( ( `' Q " { 0 } ) e. Fin -> ( # ` ( `' Q " { 0 } ) ) e. NN0 )
111 97 110 syl 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( `' Q " { 0 } ) ) e. NN0 )
112 111 nn0red 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( `' Q " { 0 } ) ) e. RR )
113 1red 
 |-  ( ( ph /\ z e. R ) -> 1 e. RR )
114 36 112 113 leadd2d 
 |-  ( ( ph /\ z e. R ) -> ( D <_ ( # ` ( `' Q " { 0 } ) ) <-> ( 1 + D ) <_ ( 1 + ( # ` ( `' Q " { 0 } ) ) ) ) )
115 109 114 mpbird 
 |-  ( ( ph /\ z e. R ) -> D <_ ( # ` ( `' Q " { 0 } ) ) )
116 112 36 letri3d 
 |-  ( ( ph /\ z e. R ) -> ( ( # ` ( `' Q " { 0 } ) ) = D <-> ( ( # ` ( `' Q " { 0 } ) ) <_ D /\ D <_ ( # ` ( `' Q " { 0 } ) ) ) ) )
117 95 115 116 mpbir2and 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( `' Q " { 0 } ) ) = D )
118 81 117 eqeq12d 
 |-  ( ( ph /\ z e. R ) -> ( ( # ` ( { z } u. ( `' Q " { 0 } ) ) ) = ( # ` ( `' Q " { 0 } ) ) <-> ( D + 1 ) = D ) )
119 42 118 imbitrid 
 |-  ( ( ph /\ z e. R ) -> ( z e. ( `' Q " { 0 } ) -> ( D + 1 ) = D ) )
120 119 necon3ad 
 |-  ( ( ph /\ z e. R ) -> ( ( D + 1 ) =/= D -> -. z e. ( `' Q " { 0 } ) ) )
121 38 120 mpd 
 |-  ( ( ph /\ z e. R ) -> -. z e. ( `' Q " { 0 } ) )
122 disjsn 
 |-  ( ( ( `' Q " { 0 } ) i^i { z } ) = (/) <-> -. z e. ( `' Q " { 0 } ) )
123 121 122 sylibr 
 |-  ( ( ph /\ z e. R ) -> ( ( `' Q " { 0 } ) i^i { z } ) = (/) )
124 29 123 eqtrid 
 |-  ( ( ph /\ z e. R ) -> ( { z } i^i ( `' Q " { 0 } ) ) = (/) )
125 22 adantr 
 |-  ( ( ph /\ z e. R ) -> R e. Fin )
126 49 adantr 
 |-  ( ( ph /\ z e. R ) -> R C_ CC )
127 126 sselda 
 |-  ( ( ( ph /\ z e. R ) /\ x e. R ) -> x e. CC )
128 124 77 125 127 fsumsplit 
 |-  ( ( ph /\ z e. R ) -> sum_ x e. R x = ( sum_ x e. { z } x + sum_ x e. ( `' Q " { 0 } ) x ) )
129 id 
 |-  ( x = z -> x = z )
130 129 sumsn 
 |-  ( ( z e. CC /\ z e. CC ) -> sum_ x e. { z } x = z )
131 50 50 130 syl2anc 
 |-  ( ( ph /\ z e. R ) -> sum_ x e. { z } x = z )
132 50 negnegd 
 |-  ( ( ph /\ z e. R ) -> -u -u z = z )
133 131 132 eqtr4d 
 |-  ( ( ph /\ z e. R ) -> sum_ x e. { z } x = -u -u z )
134 117 31 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( # ` ( `' Q " { 0 } ) ) = ( deg ` Q ) )
135 fveq2 
 |-  ( f = Q -> ( deg ` f ) = ( deg ` Q ) )
136 135 eqeq2d 
 |-  ( f = Q -> ( D = ( deg ` f ) <-> D = ( deg ` Q ) ) )
137 cnveq 
 |-  ( f = Q -> `' f = `' Q )
138 137 imaeq1d 
 |-  ( f = Q -> ( `' f " { 0 } ) = ( `' Q " { 0 } ) )
139 138 fveq2d 
 |-  ( f = Q -> ( # ` ( `' f " { 0 } ) ) = ( # ` ( `' Q " { 0 } ) ) )
140 139 135 eqeq12d 
 |-  ( f = Q -> ( ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) <-> ( # ` ( `' Q " { 0 } ) ) = ( deg ` Q ) ) )
141 136 140 anbi12d 
 |-  ( f = Q -> ( ( D = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( D = ( deg ` Q ) /\ ( # ` ( `' Q " { 0 } ) ) = ( deg ` Q ) ) ) )
142 138 sumeq1d 
 |-  ( f = Q -> sum_ x e. ( `' f " { 0 } ) x = sum_ x e. ( `' Q " { 0 } ) x )
143 fveq2 
 |-  ( f = Q -> ( coeff ` f ) = ( coeff ` Q ) )
144 135 oveq1d 
 |-  ( f = Q -> ( ( deg ` f ) - 1 ) = ( ( deg ` Q ) - 1 ) )
145 143 144 fveq12d 
 |-  ( f = Q -> ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) = ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) )
146 143 135 fveq12d 
 |-  ( f = Q -> ( ( coeff ` f ) ` ( deg ` f ) ) = ( ( coeff ` Q ) ` ( deg ` Q ) ) )
147 145 146 oveq12d 
 |-  ( f = Q -> ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) = ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
148 147 negeqd 
 |-  ( f = Q -> -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) = -u ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
149 142 148 eqeq12d 
 |-  ( f = Q -> ( sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) <-> sum_ x e. ( `' Q " { 0 } ) x = -u ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) ) )
150 141 149 imbi12d 
 |-  ( f = Q -> ( ( ( D = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( D = ( deg ` Q ) /\ ( # ` ( `' Q " { 0 } ) ) = ( deg ` Q ) ) -> sum_ x e. ( `' Q " { 0 } ) x = -u ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) ) ) )
151 8 adantr 
 |-  ( ( ph /\ z e. R ) -> A. f e. ( Poly ` CC ) ( ( D = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
152 150 151 32 rspcdva 
 |-  ( ( ph /\ z e. R ) -> ( ( D = ( deg ` Q ) /\ ( # ` ( `' Q " { 0 } ) ) = ( deg ` Q ) ) -> sum_ x e. ( `' Q " { 0 } ) x = -u ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) ) )
153 31 134 152 mp2and 
 |-  ( ( ph /\ z e. R ) -> sum_ x e. ( `' Q " { 0 } ) x = -u ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
154 31 fvoveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` Q ) ` ( D - 1 ) ) = ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) )
155 61 fveq2d 
 |-  ( ( ph /\ z e. R ) -> ( coeff ` F ) = ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) )
156 1 155 eqtrid 
 |-  ( ( ph /\ z e. R ) -> A = ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) )
157 61 fveq2d 
 |-  ( ( ph /\ z e. R ) -> ( deg ` F ) = ( deg ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) )
158 67 simp2d 
 |-  ( ( ph /\ z e. R ) -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = 1 )
159 ax-1ne0 
 |-  1 =/= 0
160 159 a1i 
 |-  ( ( ph /\ z e. R ) -> 1 =/= 0 )
161 158 160 eqnetrd 
 |-  ( ( ph /\ z e. R ) -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) =/= 0 )
162 fveq2 
 |-  ( ( Xp oF - ( CC X. { z } ) ) = 0p -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = ( deg ` 0p ) )
163 162 16 eqtrdi 
 |-  ( ( Xp oF - ( CC X. { z } ) ) = 0p -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = 0 )
164 163 necon3i 
 |-  ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) =/= 0 -> ( Xp oF - ( CC X. { z } ) ) =/= 0p )
165 161 164 syl 
 |-  ( ( ph /\ z e. R ) -> ( Xp oF - ( CC X. { z } ) ) =/= 0p )
166 eqid 
 |-  ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = ( deg ` ( Xp oF - ( CC X. { z } ) ) )
167 eqid 
 |-  ( deg ` Q ) = ( deg ` Q )
168 166 167 dgrmul 
 |-  ( ( ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ ( Xp oF - ( CC X. { z } ) ) =/= 0p ) /\ ( Q e. ( Poly ` CC ) /\ Q =/= 0p ) ) -> ( deg ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) = ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) )
169 68 165 32 90 168 syl22anc 
 |-  ( ( ph /\ z e. R ) -> ( deg ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) = ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) )
170 157 169 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( deg ` F ) = ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) )
171 2 170 eqtrid 
 |-  ( ( ph /\ z e. R ) -> N = ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) )
172 156 171 fveq12d 
 |-  ( ( ph /\ z e. R ) -> ( A ` N ) = ( ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) ` ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) ) )
173 eqid 
 |-  ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) = ( coeff ` ( Xp oF - ( CC X. { z } ) ) )
174 eqid 
 |-  ( coeff ` Q ) = ( coeff ` Q )
175 173 174 166 167 coemulhi 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ Q e. ( Poly ` CC ) ) -> ( ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) ` ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) ) = ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) x. ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
176 68 32 175 syl2anc 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) ` ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) ) = ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) x. ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
177 158 fveq2d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) = ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) )
178 ssid 
 |-  CC C_ CC
179 plyid 
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> Xp e. ( Poly ` CC ) )
180 178 100 179 mp2an 
 |-  Xp e. ( Poly ` CC )
181 plyconst 
 |-  ( ( CC C_ CC /\ z e. CC ) -> ( CC X. { z } ) e. ( Poly ` CC ) )
182 178 50 181 sylancr 
 |-  ( ( ph /\ z e. R ) -> ( CC X. { z } ) e. ( Poly ` CC ) )
183 eqid 
 |-  ( coeff ` Xp ) = ( coeff ` Xp )
184 eqid 
 |-  ( coeff ` ( CC X. { z } ) ) = ( coeff ` ( CC X. { z } ) )
185 183 184 coesub 
 |-  ( ( Xp e. ( Poly ` CC ) /\ ( CC X. { z } ) e. ( Poly ` CC ) ) -> ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) = ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) )
186 180 182 185 sylancr 
 |-  ( ( ph /\ z e. R ) -> ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) = ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) )
187 186 fveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) = ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 1 ) )
188 1nn0 
 |-  1 e. NN0
189 183 coef3 
 |-  ( Xp e. ( Poly ` CC ) -> ( coeff ` Xp ) : NN0 --> CC )
190 ffn 
 |-  ( ( coeff ` Xp ) : NN0 --> CC -> ( coeff ` Xp ) Fn NN0 )
191 180 189 190 mp2b 
 |-  ( coeff ` Xp ) Fn NN0
192 191 a1i 
 |-  ( ( ph /\ z e. R ) -> ( coeff ` Xp ) Fn NN0 )
193 184 coef3 
 |-  ( ( CC X. { z } ) e. ( Poly ` CC ) -> ( coeff ` ( CC X. { z } ) ) : NN0 --> CC )
194 ffn 
 |-  ( ( coeff ` ( CC X. { z } ) ) : NN0 --> CC -> ( coeff ` ( CC X. { z } ) ) Fn NN0 )
195 182 193 194 3syl 
 |-  ( ( ph /\ z e. R ) -> ( coeff ` ( CC X. { z } ) ) Fn NN0 )
196 nn0ex 
 |-  NN0 e. _V
197 196 a1i 
 |-  ( ( ph /\ z e. R ) -> NN0 e. _V )
198 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
199 coeidp 
 |-  ( 1 e. NN0 -> ( ( coeff ` Xp ) ` 1 ) = if ( 1 = 1 , 1 , 0 ) )
200 199 adantl 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( ( coeff ` Xp ) ` 1 ) = if ( 1 = 1 , 1 , 0 ) )
201 eqid 
 |-  1 = 1
202 201 iftruei 
 |-  if ( 1 = 1 , 1 , 0 ) = 1
203 200 202 eqtrdi 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( ( coeff ` Xp ) ` 1 ) = 1 )
204 0lt1 
 |-  0 < 1
205 0re 
 |-  0 e. RR
206 1re 
 |-  1 e. RR
207 205 206 ltnlei 
 |-  ( 0 < 1 <-> -. 1 <_ 0 )
208 204 207 mpbi 
 |-  -. 1 <_ 0
209 50 adantr 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> z e. CC )
210 0dgr 
 |-  ( z e. CC -> ( deg ` ( CC X. { z } ) ) = 0 )
211 209 210 syl 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( deg ` ( CC X. { z } ) ) = 0 )
212 211 breq2d 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( 1 <_ ( deg ` ( CC X. { z } ) ) <-> 1 <_ 0 ) )
213 208 212 mtbiri 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> -. 1 <_ ( deg ` ( CC X. { z } ) ) )
214 eqid 
 |-  ( deg ` ( CC X. { z } ) ) = ( deg ` ( CC X. { z } ) )
215 184 214 dgrub 
 |-  ( ( ( CC X. { z } ) e. ( Poly ` CC ) /\ 1 e. NN0 /\ ( ( coeff ` ( CC X. { z } ) ) ` 1 ) =/= 0 ) -> 1 <_ ( deg ` ( CC X. { z } ) ) )
216 215 3expia 
 |-  ( ( ( CC X. { z } ) e. ( Poly ` CC ) /\ 1 e. NN0 ) -> ( ( ( coeff ` ( CC X. { z } ) ) ` 1 ) =/= 0 -> 1 <_ ( deg ` ( CC X. { z } ) ) ) )
217 182 216 sylan 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( ( ( coeff ` ( CC X. { z } ) ) ` 1 ) =/= 0 -> 1 <_ ( deg ` ( CC X. { z } ) ) ) )
218 217 necon1bd 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( -. 1 <_ ( deg ` ( CC X. { z } ) ) -> ( ( coeff ` ( CC X. { z } ) ) ` 1 ) = 0 ) )
219 213 218 mpd 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( ( coeff ` ( CC X. { z } ) ) ` 1 ) = 0 )
220 192 195 197 197 198 203 219 ofval 
 |-  ( ( ( ph /\ z e. R ) /\ 1 e. NN0 ) -> ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 1 ) = ( 1 - 0 ) )
221 188 220 mpan2 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 1 ) = ( 1 - 0 ) )
222 1m0e1 
 |-  ( 1 - 0 ) = 1
223 221 222 eqtrdi 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 1 ) = 1 )
224 187 223 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) = 1 )
225 177 224 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) = 1 )
226 225 oveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) x. ( ( coeff ` Q ) ` ( deg ` Q ) ) ) = ( 1 x. ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
227 174 coef3 
 |-  ( Q e. ( Poly ` CC ) -> ( coeff ` Q ) : NN0 --> CC )
228 32 227 syl 
 |-  ( ( ph /\ z e. R ) -> ( coeff ` Q ) : NN0 --> CC )
229 228 34 ffvelcdmd 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` Q ) ` ( deg ` Q ) ) e. CC )
230 229 mullidd 
 |-  ( ( ph /\ z e. R ) -> ( 1 x. ( ( coeff ` Q ) ` ( deg ` Q ) ) ) = ( ( coeff ` Q ) ` ( deg ` Q ) ) )
231 226 230 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) x. ( ( coeff ` Q ) ` ( deg ` Q ) ) ) = ( ( coeff ` Q ) ` ( deg ` Q ) ) )
232 172 176 231 3eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( A ` N ) = ( ( coeff ` Q ) ` ( deg ` Q ) ) )
233 154 232 oveq12d 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) = ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
234 233 negeqd 
 |-  ( ( ph /\ z e. R ) -> -u ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) = -u ( ( ( coeff ` Q ) ` ( ( deg ` Q ) - 1 ) ) / ( ( coeff ` Q ) ` ( deg ` Q ) ) ) )
235 153 234 eqtr4d 
 |-  ( ( ph /\ z e. R ) -> sum_ x e. ( `' Q " { 0 } ) x = -u ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) )
236 133 235 oveq12d 
 |-  ( ( ph /\ z e. R ) -> ( sum_ x e. { z } x + sum_ x e. ( `' Q " { 0 } ) x ) = ( -u -u z + -u ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) )
237 50 negcld 
 |-  ( ( ph /\ z e. R ) -> -u z e. CC )
238 nnm1nn0 
 |-  ( D e. NN -> ( D - 1 ) e. NN0 )
239 6 238 syl 
 |-  ( ph -> ( D - 1 ) e. NN0 )
240 239 adantr 
 |-  ( ( ph /\ z e. R ) -> ( D - 1 ) e. NN0 )
241 228 240 ffvelcdmd 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` Q ) ` ( D - 1 ) ) e. CC )
242 232 229 eqeltrd 
 |-  ( ( ph /\ z e. R ) -> ( A ` N ) e. CC )
243 2 1 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
244 43 243 syl 
 |-  ( ( ph /\ z e. R ) -> ( F = 0p <-> ( A ` N ) = 0 ) )
245 244 necon3bid 
 |-  ( ( ph /\ z e. R ) -> ( F =/= 0p <-> ( A ` N ) =/= 0 ) )
246 82 245 mpbid 
 |-  ( ( ph /\ z e. R ) -> ( A ` N ) =/= 0 )
247 241 242 246 divcld 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) e. CC )
248 237 247 negdid 
 |-  ( ( ph /\ z e. R ) -> -u ( -u z + ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) = ( -u -u z + -u ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) )
249 237 242 mulcld 
 |-  ( ( ph /\ z e. R ) -> ( -u z x. ( A ` N ) ) e. CC )
250 249 241 242 246 divdird 
 |-  ( ( ph /\ z e. R ) -> ( ( ( -u z x. ( A ` N ) ) + ( ( coeff ` Q ) ` ( D - 1 ) ) ) / ( A ` N ) ) = ( ( ( -u z x. ( A ` N ) ) / ( A ` N ) ) + ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) )
251 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
252 11 251 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
253 252 adantr 
 |-  ( ( ph /\ z e. R ) -> ( N - 1 ) e. NN0 )
254 173 174 coemul 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ Q e. ( Poly ` CC ) /\ ( N - 1 ) e. NN0 ) -> ( ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) ` ( N - 1 ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) )
255 68 32 253 254 syl3anc 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) ` ( N - 1 ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) )
256 156 fveq1d 
 |-  ( ( ph /\ z e. R ) -> ( A ` ( N - 1 ) ) = ( ( coeff ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) ` ( N - 1 ) ) )
257 1e0p1 
 |-  1 = ( 0 + 1 )
258 257 oveq2i 
 |-  ( 0 ... 1 ) = ( 0 ... ( 0 + 1 ) )
259 258 sumeq1i 
 |-  sum_ k e. ( 0 ... 1 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) )
260 0nn0 
 |-  0 e. NN0
261 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
262 260 261 eleqtri 
 |-  0 e. ( ZZ>= ` 0 )
263 262 a1i 
 |-  ( ( ph /\ z e. R ) -> 0 e. ( ZZ>= ` 0 ) )
264 258 eleq2i 
 |-  ( k e. ( 0 ... 1 ) <-> k e. ( 0 ... ( 0 + 1 ) ) )
265 173 coef3 
 |-  ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) -> ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) : NN0 --> CC )
266 68 265 syl 
 |-  ( ( ph /\ z e. R ) -> ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) : NN0 --> CC )
267 elfznn0 
 |-  ( k e. ( 0 ... 1 ) -> k e. NN0 )
268 ffvelcdm 
 |-  ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) : NN0 --> CC /\ k e. NN0 ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) e. CC )
269 266 267 268 syl2an 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( 0 ... 1 ) ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) e. CC )
270 7 oveq1d 
 |-  ( ph -> ( ( D + 1 ) - 1 ) = ( N - 1 ) )
271 pncan 
 |-  ( ( D e. CC /\ 1 e. CC ) -> ( ( D + 1 ) - 1 ) = D )
272 101 100 271 sylancl 
 |-  ( ph -> ( ( D + 1 ) - 1 ) = D )
273 270 272 eqtr3d 
 |-  ( ph -> ( N - 1 ) = D )
274 273 adantr 
 |-  ( ( ph /\ z e. R ) -> ( N - 1 ) = D )
275 6 adantr 
 |-  ( ( ph /\ z e. R ) -> D e. NN )
276 274 275 eqeltrd 
 |-  ( ( ph /\ z e. R ) -> ( N - 1 ) e. NN )
277 nnuz 
 |-  NN = ( ZZ>= ` 1 )
278 276 277 eleqtrdi 
 |-  ( ( ph /\ z e. R ) -> ( N - 1 ) e. ( ZZ>= ` 1 ) )
279 fzss2 
 |-  ( ( N - 1 ) e. ( ZZ>= ` 1 ) -> ( 0 ... 1 ) C_ ( 0 ... ( N - 1 ) ) )
280 278 279 syl 
 |-  ( ( ph /\ z e. R ) -> ( 0 ... 1 ) C_ ( 0 ... ( N - 1 ) ) )
281 280 sselda 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( 0 ... 1 ) ) -> k e. ( 0 ... ( N - 1 ) ) )
282 fznn0sub 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) - k ) e. NN0 )
283 ffvelcdm 
 |-  ( ( ( coeff ` Q ) : NN0 --> CC /\ ( ( N - 1 ) - k ) e. NN0 ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) e. CC )
284 228 282 283 syl2an 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) e. CC )
285 281 284 syldan 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( 0 ... 1 ) ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) e. CC )
286 269 285 mulcld 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( 0 ... 1 ) ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) e. CC )
287 264 286 sylan2br 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( 0 ... ( 0 + 1 ) ) ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) e. CC )
288 id 
 |-  ( k = ( 0 + 1 ) -> k = ( 0 + 1 ) )
289 288 257 eqtr4di 
 |-  ( k = ( 0 + 1 ) -> k = 1 )
290 289 fveq2d 
 |-  ( k = ( 0 + 1 ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) = ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) )
291 289 oveq2d 
 |-  ( k = ( 0 + 1 ) -> ( ( N - 1 ) - k ) = ( ( N - 1 ) - 1 ) )
292 291 fveq2d 
 |-  ( k = ( 0 + 1 ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) = ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) )
293 290 292 oveq12d 
 |-  ( k = ( 0 + 1 ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) ) )
294 263 287 293 fsump1 
 |-  ( ( ph /\ z e. R ) -> sum_ k e. ( 0 ... ( 0 + 1 ) ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) + ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) ) ) )
295 259 294 eqtrid 
 |-  ( ( ph /\ z e. R ) -> sum_ k e. ( 0 ... 1 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) + ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) ) ) )
296 eldifn 
 |-  ( k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) -> -. k e. ( 0 ... 1 ) )
297 296 adantl 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> -. k e. ( 0 ... 1 ) )
298 eldifi 
 |-  ( k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) -> k e. ( 0 ... ( N - 1 ) ) )
299 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
300 298 299 syl 
 |-  ( k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) -> k e. NN0 )
301 173 166 dgrub 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ k e. NN0 /\ ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) =/= 0 ) -> k <_ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) )
302 301 3expia 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ k e. NN0 ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) =/= 0 -> k <_ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) )
303 68 300 302 syl2an 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) =/= 0 -> k <_ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) )
304 elfzuz 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. ( ZZ>= ` 0 ) )
305 298 304 syl 
 |-  ( k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) -> k e. ( ZZ>= ` 0 ) )
306 305 adantl 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> k e. ( ZZ>= ` 0 ) )
307 1z 
 |-  1 e. ZZ
308 elfz5 
 |-  ( ( k e. ( ZZ>= ` 0 ) /\ 1 e. ZZ ) -> ( k e. ( 0 ... 1 ) <-> k <_ 1 ) )
309 306 307 308 sylancl 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( k e. ( 0 ... 1 ) <-> k <_ 1 ) )
310 158 breq2d 
 |-  ( ( ph /\ z e. R ) -> ( k <_ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) <-> k <_ 1 ) )
311 310 adantr 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( k <_ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) <-> k <_ 1 ) )
312 309 311 bitr4d 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( k e. ( 0 ... 1 ) <-> k <_ ( deg ` ( Xp oF - ( CC X. { z } ) ) ) ) )
313 303 312 sylibrd 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) =/= 0 -> k e. ( 0 ... 1 ) ) )
314 313 necon1bd 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( -. k e. ( 0 ... 1 ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) = 0 ) )
315 297 314 mpd 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) = 0 )
316 315 oveq1d 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( 0 x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) )
317 298 284 sylan2 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) e. CC )
318 317 mul02d 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( 0 x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = 0 )
319 316 318 eqtrd 
 |-  ( ( ( ph /\ z e. R ) /\ k e. ( ( 0 ... ( N - 1 ) ) \ ( 0 ... 1 ) ) ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = 0 )
320 fzfid 
 |-  ( ( ph /\ z e. R ) -> ( 0 ... ( N - 1 ) ) e. Fin )
321 280 286 319 320 fsumss 
 |-  ( ( ph /\ z e. R ) -> sum_ k e. ( 0 ... 1 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) )
322 0z 
 |-  0 e. ZZ
323 186 fveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) = ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 0 ) )
324 coeidp 
 |-  ( 0 e. NN0 -> ( ( coeff ` Xp ) ` 0 ) = if ( 0 = 1 , 1 , 0 ) )
325 159 nesymi 
 |-  -. 0 = 1
326 325 iffalsei 
 |-  if ( 0 = 1 , 1 , 0 ) = 0
327 324 326 eqtrdi 
 |-  ( 0 e. NN0 -> ( ( coeff ` Xp ) ` 0 ) = 0 )
328 327 adantl 
 |-  ( ( ( ph /\ z e. R ) /\ 0 e. NN0 ) -> ( ( coeff ` Xp ) ` 0 ) = 0 )
329 184 coefv0 
 |-  ( ( CC X. { z } ) e. ( Poly ` CC ) -> ( ( CC X. { z } ) ` 0 ) = ( ( coeff ` ( CC X. { z } ) ) ` 0 ) )
330 182 329 syl 
 |-  ( ( ph /\ z e. R ) -> ( ( CC X. { z } ) ` 0 ) = ( ( coeff ` ( CC X. { z } ) ) ` 0 ) )
331 0cn 
 |-  0 e. CC
332 vex 
 |-  z e. _V
333 332 fvconst2 
 |-  ( 0 e. CC -> ( ( CC X. { z } ) ` 0 ) = z )
334 331 333 ax-mp 
 |-  ( ( CC X. { z } ) ` 0 ) = z
335 330 334 eqtr3di 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( CC X. { z } ) ) ` 0 ) = z )
336 335 adantr 
 |-  ( ( ( ph /\ z e. R ) /\ 0 e. NN0 ) -> ( ( coeff ` ( CC X. { z } ) ) ` 0 ) = z )
337 192 195 197 197 198 328 336 ofval 
 |-  ( ( ( ph /\ z e. R ) /\ 0 e. NN0 ) -> ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 0 ) = ( 0 - z ) )
338 260 337 mpan2 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 0 ) = ( 0 - z ) )
339 df-neg 
 |-  -u z = ( 0 - z )
340 338 339 eqtr4di 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` Xp ) oF - ( coeff ` ( CC X. { z } ) ) ) ` 0 ) = -u z )
341 323 340 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) = -u z )
342 274 oveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( N - 1 ) - 0 ) = ( D - 0 ) )
343 102 subid1d 
 |-  ( ( ph /\ z e. R ) -> ( D - 0 ) = D )
344 342 343 31 3eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( ( N - 1 ) - 0 ) = ( deg ` Q ) )
345 344 fveq2d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) = ( ( coeff ` Q ) ` ( deg ` Q ) ) )
346 345 232 eqtr4d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) = ( A ` N ) )
347 341 346 oveq12d 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) ) = ( -u z x. ( A ` N ) ) )
348 347 249 eqeltrd 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) ) e. CC )
349 fveq2 
 |-  ( k = 0 -> ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) = ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) )
350 oveq2 
 |-  ( k = 0 -> ( ( N - 1 ) - k ) = ( ( N - 1 ) - 0 ) )
351 350 fveq2d 
 |-  ( k = 0 -> ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) = ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) )
352 349 351 oveq12d 
 |-  ( k = 0 -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) ) )
353 352 fsum1 
 |-  ( ( 0 e. ZZ /\ ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) ) )
354 322 348 353 sylancr 
 |-  ( ( ph /\ z e. R ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 0 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 0 ) ) ) )
355 354 347 eqtrd 
 |-  ( ( ph /\ z e. R ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) = ( -u z x. ( A ` N ) ) )
356 274 fvoveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) = ( ( coeff ` Q ) ` ( D - 1 ) ) )
357 224 356 oveq12d 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) ) = ( 1 x. ( ( coeff ` Q ) ` ( D - 1 ) ) ) )
358 241 mullidd 
 |-  ( ( ph /\ z e. R ) -> ( 1 x. ( ( coeff ` Q ) ` ( D - 1 ) ) ) = ( ( coeff ` Q ) ` ( D - 1 ) ) )
359 357 358 eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) ) = ( ( coeff ` Q ) ` ( D - 1 ) ) )
360 355 359 oveq12d 
 |-  ( ( ph /\ z e. R ) -> ( sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) + ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` 1 ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - 1 ) ) ) ) = ( ( -u z x. ( A ` N ) ) + ( ( coeff ` Q ) ` ( D - 1 ) ) ) )
361 295 321 360 3eqtr3rd 
 |-  ( ( ph /\ z e. R ) -> ( ( -u z x. ( A ` N ) ) + ( ( coeff ` Q ) ` ( D - 1 ) ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( ( coeff ` ( Xp oF - ( CC X. { z } ) ) ) ` k ) x. ( ( coeff ` Q ) ` ( ( N - 1 ) - k ) ) ) )
362 255 256 361 3eqtr4rd 
 |-  ( ( ph /\ z e. R ) -> ( ( -u z x. ( A ` N ) ) + ( ( coeff ` Q ) ` ( D - 1 ) ) ) = ( A ` ( N - 1 ) ) )
363 362 oveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( ( -u z x. ( A ` N ) ) + ( ( coeff ` Q ) ` ( D - 1 ) ) ) / ( A ` N ) ) = ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
364 237 242 246 divcan4d 
 |-  ( ( ph /\ z e. R ) -> ( ( -u z x. ( A ` N ) ) / ( A ` N ) ) = -u z )
365 364 oveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( ( -u z x. ( A ` N ) ) / ( A ` N ) ) + ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) = ( -u z + ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) )
366 250 363 365 3eqtr3rd 
 |-  ( ( ph /\ z e. R ) -> ( -u z + ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) = ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
367 366 negeqd 
 |-  ( ( ph /\ z e. R ) -> -u ( -u z + ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
368 248 367 eqtr3d 
 |-  ( ( ph /\ z e. R ) -> ( -u -u z + -u ( ( ( coeff ` Q ) ` ( D - 1 ) ) / ( A ` N ) ) ) = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
369 128 236 368 3eqtrd 
 |-  ( ( ph /\ z e. R ) -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
370 28 369 exlimddv 
 |-  ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )