This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem vieta1

Description: The first-order Vieta's formula (see http://en.wikipedia.org/wiki/Vieta%27s_formulas ). If a polynomial of degree N has N distinct roots, then the sum over these roots can be calculated as -u A ( N - 1 ) / A ( N ) . (If the roots are not distinct, then this formula is still true but must double-count some of the roots according to their multiplicities.) See also vieta for the case of polynomials over a generic ring. (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 )
vieta1.6 
|- ( ph -> N e. NN )
Assertion vieta1 
|- ( 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 vieta1.6 
 |-  ( ph -> N e. NN )
7 fveq2 
 |-  ( f = F -> ( deg ` f ) = ( deg ` F ) )
8 7 eqeq2d 
 |-  ( f = F -> ( N = ( deg ` f ) <-> N = ( deg ` F ) ) )
9 cnveq 
 |-  ( f = F -> `' f = `' F )
10 9 imaeq1d 
 |-  ( f = F -> ( `' f " { 0 } ) = ( `' F " { 0 } ) )
11 10 3 eqtr4di 
 |-  ( f = F -> ( `' f " { 0 } ) = R )
12 11 fveq2d 
 |-  ( f = F -> ( # ` ( `' f " { 0 } ) ) = ( # ` R ) )
13 7 2 eqtr4di 
 |-  ( f = F -> ( deg ` f ) = N )
14 12 13 eqeq12d 
 |-  ( f = F -> ( ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) <-> ( # ` R ) = N ) )
15 8 14 anbi12d 
 |-  ( f = F -> ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( N = ( deg ` F ) /\ ( # ` R ) = N ) ) )
16 2 biantrur 
 |-  ( ( # ` R ) = N <-> ( N = ( deg ` F ) /\ ( # ` R ) = N ) )
17 15 16 bitr4di 
 |-  ( f = F -> ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( # ` R ) = N ) )
18 11 sumeq1d 
 |-  ( f = F -> sum_ x e. ( `' f " { 0 } ) x = sum_ x e. R x )
19 fveq2 
 |-  ( f = F -> ( coeff ` f ) = ( coeff ` F ) )
20 19 1 eqtr4di 
 |-  ( f = F -> ( coeff ` f ) = A )
21 13 oveq1d 
 |-  ( f = F -> ( ( deg ` f ) - 1 ) = ( N - 1 ) )
22 20 21 fveq12d 
 |-  ( f = F -> ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) = ( A ` ( N - 1 ) ) )
23 20 13 fveq12d 
 |-  ( f = F -> ( ( coeff ` f ) ` ( deg ` f ) ) = ( A ` N ) )
24 22 23 oveq12d 
 |-  ( f = F -> ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) = ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
25 24 negeqd 
 |-  ( f = F -> -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
26 18 25 eqeq12d 
 |-  ( f = F -> ( sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) <-> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) ) )
27 17 26 imbi12d 
 |-  ( f = F -> ( ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( # ` R ) = N -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) ) ) )
28 eqeq1 
 |-  ( y = 1 -> ( y = ( deg ` f ) <-> 1 = ( deg ` f ) ) )
29 28 anbi1d 
 |-  ( y = 1 -> ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) )
30 29 imbi1d 
 |-  ( y = 1 -> ( ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
31 30 ralbidv 
 |-  ( y = 1 -> ( A. f e. ( Poly ` CC ) ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> A. f e. ( Poly ` CC ) ( ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
32 eqeq1 
 |-  ( y = d -> ( y = ( deg ` f ) <-> d = ( deg ` f ) ) )
33 32 anbi1d 
 |-  ( y = d -> ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) )
34 33 imbi1d 
 |-  ( y = d -> ( ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
35 34 ralbidv 
 |-  ( y = d -> ( A. f e. ( Poly ` CC ) ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> 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 ) ) ) ) ) )
36 eqeq1 
 |-  ( y = ( d + 1 ) -> ( y = ( deg ` f ) <-> ( d + 1 ) = ( deg ` f ) ) )
37 36 anbi1d 
 |-  ( y = ( d + 1 ) -> ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) )
38 37 imbi1d 
 |-  ( y = ( d + 1 ) -> ( ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
39 38 ralbidv 
 |-  ( y = ( d + 1 ) -> ( A. f e. ( Poly ` CC ) ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> A. f e. ( Poly ` CC ) ( ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
40 eqeq1 
 |-  ( y = N -> ( y = ( deg ` f ) <-> N = ( deg ` f ) ) )
41 40 anbi1d 
 |-  ( y = N -> ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) <-> ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) )
42 41 imbi1d 
 |-  ( y = N -> ( ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
43 42 ralbidv 
 |-  ( y = N -> ( A. f e. ( Poly ` CC ) ( ( y = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> A. f e. ( Poly ` CC ) ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
44 eqid 
 |-  ( coeff ` f ) = ( coeff ` f )
45 44 coef3 
 |-  ( f e. ( Poly ` CC ) -> ( coeff ` f ) : NN0 --> CC )
46 45 adantr 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( coeff ` f ) : NN0 --> CC )
47 0nn0 
 |-  0 e. NN0
48 ffvelcdm 
 |-  ( ( ( coeff ` f ) : NN0 --> CC /\ 0 e. NN0 ) -> ( ( coeff ` f ) ` 0 ) e. CC )
49 46 47 48 sylancl 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( coeff ` f ) ` 0 ) e. CC )
50 1nn0 
 |-  1 e. NN0
51 ffvelcdm 
 |-  ( ( ( coeff ` f ) : NN0 --> CC /\ 1 e. NN0 ) -> ( ( coeff ` f ) ` 1 ) e. CC )
52 46 50 51 sylancl 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( coeff ` f ) ` 1 ) e. CC )
53 simpr 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> 1 = ( deg ` f ) )
54 53 fveq2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( coeff ` f ) ` 1 ) = ( ( coeff ` f ) ` ( deg ` f ) ) )
55 ax-1ne0 
 |-  1 =/= 0
56 55 a1i 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> 1 =/= 0 )
57 53 56 eqnetrrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( deg ` f ) =/= 0 )
58 fveq2 
 |-  ( f = 0p -> ( deg ` f ) = ( deg ` 0p ) )
59 dgr0 
 |-  ( deg ` 0p ) = 0
60 58 59 eqtrdi 
 |-  ( f = 0p -> ( deg ` f ) = 0 )
61 60 necon3i 
 |-  ( ( deg ` f ) =/= 0 -> f =/= 0p )
62 57 61 syl 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> f =/= 0p )
63 eqid 
 |-  ( deg ` f ) = ( deg ` f )
64 63 44 dgreq0 
 |-  ( f e. ( Poly ` CC ) -> ( f = 0p <-> ( ( coeff ` f ) ` ( deg ` f ) ) = 0 ) )
65 64 necon3bid 
 |-  ( f e. ( Poly ` CC ) -> ( f =/= 0p <-> ( ( coeff ` f ) ` ( deg ` f ) ) =/= 0 ) )
66 65 adantr 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( f =/= 0p <-> ( ( coeff ` f ) ` ( deg ` f ) ) =/= 0 ) )
67 62 66 mpbid 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( coeff ` f ) ` ( deg ` f ) ) =/= 0 )
68 54 67 eqnetrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( coeff ` f ) ` 1 ) =/= 0 )
69 49 52 68 divcld 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC )
70 69 negcld 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC )
71 id 
 |-  ( x = -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) -> x = -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) )
72 71 sumsn 
 |-  ( ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC /\ -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC ) -> sum_ x e. { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } x = -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) )
73 70 70 72 syl2anc 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> sum_ x e. { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } x = -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) )
74 73 adantrr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> sum_ x e. { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } x = -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) )
75 eqid 
 |-  ( `' f " { 0 } ) = ( `' f " { 0 } )
76 75 fta1 
 |-  ( ( f e. ( Poly ` CC ) /\ f =/= 0p ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) )
77 62 76 syldan 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) )
78 77 simpld 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( `' f " { 0 } ) e. Fin )
79 78 adantrr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> ( `' f " { 0 } ) e. Fin )
80 44 63 coeid2 
 |-  ( ( f e. ( Poly ` CC ) /\ -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC ) -> ( f ` -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) )
81 70 80 syldan 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( f ` -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) )
82 53 oveq2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( 0 ... 1 ) = ( 0 ... ( deg ` f ) ) )
83 82 sumeq1d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> sum_ k e. ( 0 ... 1 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = sum_ k e. ( 0 ... ( deg ` f ) ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) )
84 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
85 1e0p1 
 |-  1 = ( 0 + 1 )
86 fveq2 
 |-  ( k = 1 -> ( ( coeff ` f ) ` k ) = ( ( coeff ` f ) ` 1 ) )
87 oveq2 
 |-  ( k = 1 -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) = ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) )
88 86 87 oveq12d 
 |-  ( k = 1 -> ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = ( ( ( coeff ` f ) ` 1 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) ) )
89 46 ffvelcdmda 
 |-  ( ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) /\ k e. NN0 ) -> ( ( coeff ` f ) ` k ) e. CC )
90 expcl 
 |-  ( ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC /\ k e. NN0 ) -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) e. CC )
91 70 90 sylan 
 |-  ( ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) /\ k e. NN0 ) -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) e. CC )
92 89 91 mulcld 
 |-  ( ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) /\ k e. NN0 ) -> ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) e. CC )
93 0z 
 |-  0 e. ZZ
94 70 exp0d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) = 1 )
95 94 oveq2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) = ( ( ( coeff ` f ) ` 0 ) x. 1 ) )
96 49 mulridd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) x. 1 ) = ( ( coeff ` f ) ` 0 ) )
97 95 96 eqtrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) = ( ( coeff ` f ) ` 0 ) )
98 97 49 eqeltrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) e. CC )
99 fveq2 
 |-  ( k = 0 -> ( ( coeff ` f ) ` k ) = ( ( coeff ` f ) ` 0 ) )
100 oveq2 
 |-  ( k = 0 -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) = ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) )
101 99 100 oveq12d 
 |-  ( k = 0 -> ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) )
102 101 fsum1 
 |-  ( ( 0 e. ZZ /\ ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) )
103 93 98 102 sylancr 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = ( ( ( coeff ` f ) ` 0 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 0 ) ) )
104 103 97 eqtrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = ( ( coeff ` f ) ` 0 ) )
105 104 47 jctil 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( 0 e. NN0 /\ sum_ k e. ( 0 ... 0 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = ( ( coeff ` f ) ` 0 ) ) )
106 70 exp1d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) = -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) )
107 106 oveq2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 1 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) ) = ( ( ( coeff ` f ) ` 1 ) x. -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) )
108 52 69 mulneg2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 1 ) x. -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = -u ( ( ( coeff ` f ) ` 1 ) x. ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) )
109 49 52 68 divcan2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 1 ) x. ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = ( ( coeff ` f ) ` 0 ) )
110 109 negeqd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> -u ( ( ( coeff ` f ) ` 1 ) x. ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = -u ( ( coeff ` f ) ` 0 ) )
111 107 108 110 3eqtrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 1 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) ) = -u ( ( coeff ` f ) ` 0 ) )
112 111 oveq2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) + ( ( ( coeff ` f ) ` 1 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) ) ) = ( ( ( coeff ` f ) ` 0 ) + -u ( ( coeff ` f ) ` 0 ) ) )
113 49 negidd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) + -u ( ( coeff ` f ) ` 0 ) ) = 0 )
114 112 113 eqtrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) + ( ( ( coeff ` f ) ` 1 ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ 1 ) ) ) = 0 )
115 84 85 88 92 105 114 fsump1i 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( 1 e. NN0 /\ sum_ k e. ( 0 ... 1 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = 0 ) )
116 115 simprd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> sum_ k e. ( 0 ... 1 ) ( ( ( coeff ` f ) ` k ) x. ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ^ k ) ) = 0 )
117 81 83 116 3eqtr2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( f ` -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = 0 )
118 plyf 
 |-  ( f e. ( Poly ` CC ) -> f : CC --> CC )
119 118 ffnd 
 |-  ( f e. ( Poly ` CC ) -> f Fn CC )
120 119 adantr 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> f Fn CC )
121 fniniseg 
 |-  ( f Fn CC -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. ( `' f " { 0 } ) <-> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC /\ ( f ` -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = 0 ) ) )
122 120 121 syl 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. ( `' f " { 0 } ) <-> ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC /\ ( f ` -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) ) = 0 ) ) )
123 70 117 122 mpbir2and 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. ( `' f " { 0 } ) )
124 123 snssd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } C_ ( `' f " { 0 } ) )
125 124 adantrr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } C_ ( `' f " { 0 } ) )
126 hashsng 
 |-  ( -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) e. CC -> ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = 1 )
127 70 126 syl 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = 1 )
128 127 53 eqtrd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = ( deg ` f ) )
129 128 adantrr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = ( deg ` f ) )
130 simprr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) )
131 129 130 eqtr4d 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = ( # ` ( `' f " { 0 } ) ) )
132 snfi 
 |-  { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } e. Fin
133 hashen 
 |-  ( ( { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } e. Fin /\ ( `' f " { 0 } ) e. Fin ) -> ( ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = ( # ` ( `' f " { 0 } ) ) <-> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ~~ ( `' f " { 0 } ) ) )
134 132 78 133 sylancr 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = ( # ` ( `' f " { 0 } ) ) <-> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ~~ ( `' f " { 0 } ) ) )
135 134 adantrr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> ( ( # ` { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ) = ( # ` ( `' f " { 0 } ) ) <-> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ~~ ( `' f " { 0 } ) ) )
136 131 135 mpbid 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ~~ ( `' f " { 0 } ) )
137 fisseneq 
 |-  ( ( ( `' f " { 0 } ) e. Fin /\ { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } C_ ( `' f " { 0 } ) /\ { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } ~~ ( `' f " { 0 } ) ) -> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } = ( `' f " { 0 } ) )
138 79 125 136 137 syl3anc 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } = ( `' f " { 0 } ) )
139 138 sumeq1d 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> sum_ x e. { -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) } x = sum_ x e. ( `' f " { 0 } ) x )
140 1m1e0 
 |-  ( 1 - 1 ) = 0
141 53 oveq1d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( 1 - 1 ) = ( ( deg ` f ) - 1 ) )
142 140 141 eqtr3id 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> 0 = ( ( deg ` f ) - 1 ) )
143 142 fveq2d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( coeff ` f ) ` 0 ) = ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) )
144 143 54 oveq12d 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
145 144 negeqd 
 |-  ( ( f e. ( Poly ` CC ) /\ 1 = ( deg ` f ) ) -> -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
146 145 adantrr 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> -u ( ( ( coeff ` f ) ` 0 ) / ( ( coeff ` f ) ` 1 ) ) = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
147 74 139 146 3eqtr3d 
 |-  ( ( f e. ( Poly ` CC ) /\ ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
148 147 ex 
 |-  ( f e. ( Poly ` CC ) -> ( ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
149 148 rgen 
 |-  A. f e. ( Poly ` CC ) ( ( 1 = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
150 id 
 |-  ( y = x -> y = x )
151 150 cbvsumv 
 |-  sum_ y e. ( `' f " { 0 } ) y = sum_ x e. ( `' f " { 0 } ) x
152 151 eqeq1i 
 |-  ( sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) <-> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
153 152 imbi2i 
 |-  ( ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
154 153 ralbii 
 |-  ( A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) <-> 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 ) ) ) ) )
155 eqid 
 |-  ( coeff ` g ) = ( coeff ` g )
156 eqid 
 |-  ( deg ` g ) = ( deg ` g )
157 eqid 
 |-  ( `' g " { 0 } ) = ( `' g " { 0 } )
158 simp1r 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> g e. ( Poly ` CC ) )
159 simp3r 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) )
160 simp1l 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> d e. NN )
161 simp3l 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> ( d + 1 ) = ( deg ` g ) )
162 simp2 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
163 162 154 sylib 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> 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 ) ) ) ) )
164 eqid 
 |-  ( g quot ( Xp oF - ( CC X. { z } ) ) ) = ( g quot ( Xp oF - ( CC X. { z } ) ) )
165 155 156 157 158 159 160 161 163 164 vieta1lem2 
 |-  ( ( ( d e. NN /\ g e. ( Poly ` CC ) ) /\ A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) /\ ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) ) -> sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) )
166 165 3exp 
 |-  ( ( d e. NN /\ g e. ( Poly ` CC ) ) -> ( A. f e. ( Poly ` CC ) ( ( d = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ y e. ( `' f " { 0 } ) y = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) -> ( ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) -> sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) ) ) )
167 154 166 biimtrrid 
 |-  ( ( d e. NN /\ g e. ( Poly ` CC ) ) -> ( 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 ) ) ) ) -> ( ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) -> sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) ) ) )
168 167 ralrimdva 
 |-  ( d e. NN -> ( 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 ) ) ) ) -> A. g e. ( Poly ` CC ) ( ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) -> sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) ) ) )
169 fveq2 
 |-  ( g = f -> ( deg ` g ) = ( deg ` f ) )
170 169 eqeq2d 
 |-  ( g = f -> ( ( d + 1 ) = ( deg ` g ) <-> ( d + 1 ) = ( deg ` f ) ) )
171 cnveq 
 |-  ( g = f -> `' g = `' f )
172 171 imaeq1d 
 |-  ( g = f -> ( `' g " { 0 } ) = ( `' f " { 0 } ) )
173 172 fveq2d 
 |-  ( g = f -> ( # ` ( `' g " { 0 } ) ) = ( # ` ( `' f " { 0 } ) ) )
174 173 169 eqeq12d 
 |-  ( g = f -> ( ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) <-> ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) )
175 170 174 anbi12d 
 |-  ( g = f -> ( ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) <-> ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) ) )
176 172 sumeq1d 
 |-  ( g = f -> sum_ x e. ( `' g " { 0 } ) x = sum_ x e. ( `' f " { 0 } ) x )
177 fveq2 
 |-  ( g = f -> ( coeff ` g ) = ( coeff ` f ) )
178 169 oveq1d 
 |-  ( g = f -> ( ( deg ` g ) - 1 ) = ( ( deg ` f ) - 1 ) )
179 177 178 fveq12d 
 |-  ( g = f -> ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) = ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) )
180 177 169 fveq12d 
 |-  ( g = f -> ( ( coeff ` g ) ` ( deg ` g ) ) = ( ( coeff ` f ) ` ( deg ` f ) ) )
181 179 180 oveq12d 
 |-  ( g = f -> ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) = ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
182 181 negeqd 
 |-  ( g = f -> -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) )
183 176 182 eqeq12d 
 |-  ( g = f -> ( sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) <-> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
184 175 183 imbi12d 
 |-  ( g = f -> ( ( ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) -> sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) ) <-> ( ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
185 184 cbvralvw 
 |-  ( A. g e. ( Poly ` CC ) ( ( ( d + 1 ) = ( deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = ( deg ` g ) ) -> sum_ x e. ( `' g " { 0 } ) x = -u ( ( ( coeff ` g ) ` ( ( deg ` g ) - 1 ) ) / ( ( coeff ` g ) ` ( deg ` g ) ) ) ) <-> A. f e. ( Poly ` CC ) ( ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
186 168 185 imbitrdi 
 |-  ( d e. NN -> ( 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 ) ) ) ) -> A. f e. ( Poly ` CC ) ( ( ( d + 1 ) = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) ) )
187 31 35 39 43 149 186 nnind 
 |-  ( N e. NN -> A. f e. ( Poly ` CC ) ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
188 6 187 syl 
 |-  ( ph -> A. f e. ( Poly ` CC ) ( ( N = ( deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = ( deg ` f ) ) -> sum_ x e. ( `' f " { 0 } ) x = -u ( ( ( coeff ` f ) ` ( ( deg ` f ) - 1 ) ) / ( ( coeff ` f ) ` ( deg ` f ) ) ) ) )
189 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
190 189 4 sselid 
 |-  ( ph -> F e. ( Poly ` CC ) )
191 27 188 190 rspcdva 
 |-  ( ph -> ( ( # ` R ) = N -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) ) )
192 5 191 mpd 
 |-  ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )