Theorem vieta1 24067

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.) (Contributed by Mario Carneiro, 28-Jul-2014.)

Hypotheses

Ref	Expression
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

Ref	Expression
vieta1	|- ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )

Distinct variable groups:   x, R   ph, x

Allowed substitution hints:   A( x)   S( x)   F( x)   N( x)

Proof of Theorem vieta1

Dummy variables f k y z d g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		plyssc 23956	. . 3 |- (Poly ` S ) C_ (Poly ` CC )
2		vieta1.4	. . 3 |- ( ph -> F e. (Poly ` S ) )
3	1, 2	sseldi 3601	. 2 |- ( ph -> F e. (Poly ` CC ) )
4		vieta1.6	. . 3 |- ( ph -> N e. NN )
5		eqeq1 2626	. . . . . . 7 |- ( y = 1 -> ( y = (deg ` f ) <-> 1 = (deg ` f ) ) )
6	5	anbi1d 741	. . . . . 6 |- ( y = 1 -> ( ( y = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) <-> ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) )
7	6	imbi1d 331	. . . . 5 |- ( 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 ) ) ) ) ) )
8	7	ralbidv 2986	. . . 4 |- ( 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 ) ) ) ) ) )
9		eqeq1 2626	. . . . . . 7 |- ( y = d -> ( y = (deg ` f ) <-> d = (deg ` f ) ) )
10	9	anbi1d 741	. . . . . 6 |- ( y = d -> ( ( y = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) <-> ( d = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) )
11	10	imbi1d 331	. . . . 5 |- ( 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 ) ) ) ) ) )
12	11	ralbidv 2986	. . . 4 |- ( 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 ) ) ) ) ) )
13		eqeq1 2626	. . . . . . 7 |- ( y = ( d + 1 ) -> ( y = (deg ` f ) <-> ( d + 1 ) = (deg ` f ) ) )
14	13	anbi1d 741	. . . . . 6 |- ( y = ( d + 1 ) -> ( ( y = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) <-> ( ( d + 1 ) = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) )
15	14	imbi1d 331	. . . . 5 |- ( 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 ) ) ) ) ) )
16	15	ralbidv 2986	. . . 4 |- ( 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 ) ) ) ) ) )
17		eqeq1 2626	. . . . . . 7 |- ( y = N -> ( y = (deg ` f ) <-> N = (deg ` f ) ) )
18	17	anbi1d 741	. . . . . 6 |- ( y = N -> ( ( y = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) <-> ( N = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) )
19	18	imbi1d 331	. . . . 5 |- ( 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 ) ) ) ) ) )
20	19	ralbidv 2986	. . . 4 |- ( 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 ) ) ) ) ) )
21		eqid 2622	. . . . . . . . . . . . . 14 |- (coeff ` f ) = (coeff ` f )
22	21	coef3 23988	. . . . . . . . . . . . 13 |- ( f e. (Poly ` CC ) -> (coeff ` f ) : NN0 --> CC )
23	22	adantr 481	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> (coeff ` f ) : NN0 --> CC )
24		0nn0 11307	. . . . . . . . . . . 12 |- 0 e. NN0
25		ffvelrn 6357	. . . . . . . . . . . 12 |- ( ( (coeff ` f ) : NN0 --> CC /\ 0 e. NN0 ) -> ( (coeff ` f ) ` 0 ) e. CC )
26	23, 24, 25	sylancl 694	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( (coeff ` f ) ` 0 ) e. CC )
27		1nn0 11308	. . . . . . . . . . . 12 |- 1 e. NN0
28		ffvelrn 6357	. . . . . . . . . . . 12 |- ( ( (coeff ` f ) : NN0 --> CC /\ 1 e. NN0 ) -> ( (coeff ` f ) ` 1 ) e. CC )
29	23, 27, 28	sylancl 694	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( (coeff ` f ) ` 1 ) e. CC )
30		simpr 477	. . . . . . . . . . . . 13 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> 1 = (deg ` f ) )
31	30	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( (coeff ` f ) ` 1 ) = ( (coeff ` f ) ` (deg ` f ) ) )
32		ax-1ne0 10005	. . . . . . . . . . . . . . . 16 |- 1 =/= 0
33	32	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> 1 =/= 0 )
34	30, 33	eqnetrrd 2862	. . . . . . . . . . . . . 14 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> (deg ` f ) =/= 0 )
35		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( f = 0p -> (deg ` f ) = (deg ` 0p ) )
36		dgr0 24018	. . . . . . . . . . . . . . . 16 |- (deg ` 0p ) = 0
37	35, 36	syl6eq 2672	. . . . . . . . . . . . . . 15 |- ( f = 0p -> (deg ` f ) = 0 )
38	37	necon3i 2826	. . . . . . . . . . . . . 14 |- ( (deg ` f ) =/= 0 -> f =/= 0p )
39	34, 38	syl 17	. . . . . . . . . . . . 13 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> f =/= 0p )
40		eqid 2622	. . . . . . . . . . . . . . . 16 |- (deg ` f ) = (deg ` f )
41	40, 21	dgreq0 24021	. . . . . . . . . . . . . . 15 |- ( f e. (Poly ` CC ) -> ( f = 0p <-> ( (coeff ` f ) ` (deg ` f ) ) = 0 ) )
42	41	necon3bid 2838	. . . . . . . . . . . . . 14 |- ( f e. (Poly ` CC ) -> ( f =/= 0p <-> ( (coeff ` f ) ` (deg ` f ) ) =/= 0 ) )
43	42	adantr 481	. . . . . . . . . . . . 13 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( f =/= 0p <-> ( (coeff ` f ) ` (deg ` f ) ) =/= 0 ) )
44	39, 43	mpbid 222	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( (coeff ` f ) ` (deg ` f ) ) =/= 0 )
45	31, 44	eqnetrd 2861	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( (coeff ` f ) ` 1 ) =/= 0 )
46	26, 29, 45	divcld 10801	. . . . . . . . . 10 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) e. CC )
47	46	negcld 10379	. . . . . . . . 9 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) e. CC )
48		id 22	. . . . . . . . . 10 |- ( x = -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) -> x = -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) )
49	48	sumsn 14475	. . . . . . . . 9 |- ( ( -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 ) ) )
50	47, 47, 49	syl2anc 693	. . . . . . . 8 |- ( ( 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 ) ) )
51	50	adantrr 753	. . . . . . 7 |- ( ( 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 ) ) )
52		eqid 2622	. . . . . . . . . . . . 13 |- ( `' f " { 0 } ) = ( `' f " { 0 } )
53	52	fta1 24063	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ f =/= 0p ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ (deg ` f ) ) )
54	39, 53	syldan 487	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ (deg ` f ) ) )
55	54	simpld 475	. . . . . . . . . 10 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( `' f " { 0 } ) e. Fin )
56	55	adantrr 753	. . . . . . . . 9 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> ( `' f " { 0 } ) e. Fin )
57	21, 40	coeid2 23995	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) )
58	47, 57	syldan 487	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
59	30	oveq2d 6666	. . . . . . . . . . . . . 14 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( 0 ... 1 ) = ( 0 ... (deg ` f ) ) )
60	59	sumeq1d 14431	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
61		nn0uz 11722	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
62		1e0p1 11552	. . . . . . . . . . . . . . 15 |- 1 = ( 0 + 1 )
63		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( k = 1 -> ( (coeff ` f ) ` k ) = ( (coeff ` f ) ` 1 ) )
64		oveq2 6658	. . . . . . . . . . . . . . . 16 |- ( k = 1 -> ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ k ) = ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 1 ) )
65	63, 64	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( 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 ) ) )
66	23	ffvelrnda 6359	. . . . . . . . . . . . . . . 16 |- ( ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) /\ k e. NN0 ) -> ( (coeff ` f ) ` k ) e. CC )
67		expcl 12878	. . . . . . . . . . . . . . . . 17 |- ( ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) e. CC /\ k e. NN0 ) -> ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ k ) e. CC )
68	47, 67	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) /\ k e. NN0 ) -> ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ k ) e. CC )
69	66, 68	mulcld 10060	. . . . . . . . . . . . . . 15 |- ( ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) /\ k e. NN0 ) -> ( ( (coeff ` f ) ` k ) x. ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ k ) ) e. CC )
70		0z 11388	. . . . . . . . . . . . . . . . . 18 |- 0 e. ZZ
71	47	exp0d 13002	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 0 ) = 1 )
72	71	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) x. ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 0 ) ) = ( ( (coeff ` f ) ` 0 ) x. 1 ) )
73	26	mulid1d 10057	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) x. 1 ) = ( (coeff ` f ) ` 0 ) )
74	72, 73	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) x. ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 0 ) ) = ( (coeff ` f ) ` 0 ) )
75	74, 26	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) x. ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 0 ) ) e. CC )
76		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( k = 0 -> ( (coeff ` f ) ` k ) = ( (coeff ` f ) ` 0 ) )
77		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( k = 0 -> ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ k ) = ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 0 ) )
78	76, 77	oveq12d 6668	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) )
79	78	fsum1 14476	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) )
80	70, 75, 79	sylancr 695	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) )
81	80, 74	eqtrd 2656	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) )
82	81, 24	jctil 560	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) )
83	47	exp1d 13003	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 1 ) = -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) )
84	83	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
85	29, 46	mulneg2d 10484	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) )
86	26, 29, 45	divcan2d 10803	. . . . . . . . . . . . . . . . . . 19 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 1 ) x. ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ) = ( (coeff ` f ) ` 0 ) )
87	86	negeqd 10275	. . . . . . . . . . . . . . . . . 18 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> -u ( ( (coeff ` f ) ` 1 ) x. ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ) = -u ( (coeff ` f ) ` 0 ) )
88	84, 85, 87	3eqtrd 2660	. . . . . . . . . . . . . . . . 17 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 1 ) x. ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 1 ) ) = -u ( (coeff ` f ) ` 0 ) )
89	88	oveq2d 6666	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
90	26	negidd 10382	. . . . . . . . . . . . . . . 16 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) + -u ( (coeff ` f ) ` 0 ) ) = 0 )
91	89, 90	eqtrd 2656	. . . . . . . . . . . . . . 15 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) + ( ( (coeff ` f ) ` 1 ) x. ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ^ 1 ) ) ) = 0 )
92	61, 62, 65, 69, 82, 91	fsump1i 14500	. . . . . . . . . . . . . 14 |- ( ( 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 ) )
93	92	simprd 479	. . . . . . . . . . . . 13 |- ( ( 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 )
94	58, 60, 93	3eqtr2d 2662	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( f ` -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) ) = 0 )
95		plyf 23954	. . . . . . . . . . . . . . 15 |- ( f e. (Poly ` CC ) -> f : CC --> CC )
96		ffn 6045	. . . . . . . . . . . . . . 15 |- ( f : CC --> CC -> f Fn CC )
97	95, 96	syl 17	. . . . . . . . . . . . . 14 |- ( f e. (Poly ` CC ) -> f Fn CC )
98	97	adantr 481	. . . . . . . . . . . . 13 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> f Fn CC )
99		fniniseg 6338	. . . . . . . . . . . . 13 |- ( 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 ) ) )
100	98, 99	syl 17	. . . . . . . . . . . 12 |- ( ( 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 ) ) )
101	47, 94, 100	mpbir2and 957	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) e. ( `' f " { 0 } ) )
102	101	snssd 4340	. . . . . . . . . 10 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } C_ ( `' f " { 0 } ) )
103	102	adantrr 753	. . . . . . . . 9 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } C_ ( `' f " { 0 } ) )
104		hashsng 13159	. . . . . . . . . . . . . 14 |- ( -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) e. CC -> ( # ` { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } ) = 1 )
105	47, 104	syl 17	. . . . . . . . . . . . 13 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( # ` { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } ) = 1 )
106	105, 30	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( # ` { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } ) = (deg ` f ) )
107	106	adantrr 753	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> ( # ` { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } ) = (deg ` f ) )
108		simprr 796	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> ( # ` ( `' f " { 0 } ) ) = (deg ` f ) )
109	107, 108	eqtr4d 2659	. . . . . . . . . 10 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> ( # ` { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } ) = ( # ` ( `' f " { 0 } ) ) )
110		snfi 8038	. . . . . . . . . . . 12 |- { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } e. Fin
111		hashen 13135	. . . . . . . . . . . 12 |- ( ( { -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 } ) ) )
112	110, 55, 111	sylancr 695	. . . . . . . . . . 11 |- ( ( 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 } ) ) )
113	112	adantrr 753	. . . . . . . . . 10 |- ( ( 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 } ) ) )
114	109, 113	mpbid 222	. . . . . . . . 9 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } ~~ ( `' f " { 0 } ) )
115		fisseneq 8171	. . . . . . . . 9 |- ( ( ( `' 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 } ) )
116	56, 103, 114, 115	syl3anc 1326	. . . . . . . 8 |- ( ( f e. (Poly ` CC ) /\ ( 1 = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) -> { -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) } = ( `' f " { 0 } ) )
117	116	sumeq1d 14431	. . . . . . 7 |- ( ( 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 )
118		1m1e0 11089	. . . . . . . . . . . 12 |- ( 1 - 1 ) = 0
119	30	oveq1d 6665	. . . . . . . . . . . 12 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( 1 - 1 ) = ( (deg ` f ) - 1 ) )
120	118, 119	syl5eqr 2670	. . . . . . . . . . 11 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> 0 = ( (deg ` f ) - 1 ) )
121	120	fveq2d 6195	. . . . . . . . . 10 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( (coeff ` f ) ` 0 ) = ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) )
122	121, 31	oveq12d 6668	. . . . . . . . 9 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) = ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) )
123	122	negeqd 10275	. . . . . . . 8 |- ( ( f e. (Poly ` CC ) /\ 1 = (deg ` f ) ) -> -u ( ( (coeff ` f ) ` 0 ) / ( (coeff ` f ) ` 1 ) ) = -u ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) )
124	123	adantrr 753	. . . . . . 7 |- ( ( 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 ) ) ) )
125	51, 117, 124	3eqtr3d 2664	. . . . . 6 |- ( ( 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 ) ) ) )
126	125	ex 450	. . . . 5 |- ( 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 ) ) ) ) )
127	126	rgen 2922	. . . 4 |- 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 ) ) ) )
128		id 22	. . . . . . . . . . 11 |- ( y = x -> y = x )
129	128	cbvsumv 14426	. . . . . . . . . 10 |- sum_ y e. ( `' f " { 0 } ) y = sum_ x e. ( `' f " { 0 } ) x
130	129	eqeq1i 2627	. . . . . . . . 9 |- ( 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 ) ) ) )
131	130	imbi2i 326	. . . . . . . 8 |- ( ( ( 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 ) ) ) ) )
132	131	ralbii 2980	. . . . . . 7 |- ( 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 ) ) ) ) )
133		eqid 2622	. . . . . . . . 9 |- (coeff ` g ) = (coeff ` g )
134		eqid 2622	. . . . . . . . 9 |- (deg ` g ) = (deg ` g )
135		eqid 2622	. . . . . . . . 9 |- ( `' g " { 0 } ) = ( `' g " { 0 } )
136		simp1r 1086	. . . . . . . . 9 |- ( ( ( 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 ) )
137		simp3r 1090	. . . . . . . . 9 |- ( ( ( 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 ) )
138		simp1l 1085	. . . . . . . . 9 |- ( ( ( 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 )
139		simp3l 1089	. . . . . . . . 9 |- ( ( ( 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 ) )
140		simp2 1062	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) )
141	140, 132	sylib 208	. . . . . . . . 9 |- ( ( ( 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 ) ) ) ) )
142		eqid 2622	. . . . . . . . 9 |- ( g quot ( Xp oF - ( CC X. { z } ) ) ) = ( g quot ( Xp oF - ( CC X. { z } ) ) )
143	133, 134, 135, 136, 137, 138, 139, 141, 142	vieta1lem2 24066	. . . . . . . 8 |- ( ( ( 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 ) ) ) )
144	143	3exp 1264	. . . . . . 7 |- ( ( 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 ) ) ) ) ) )
145	132, 144	syl5bir 233	. . . . . 6 |- ( ( 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 ) ) ) ) ) )
146	145	ralrimdva 2969	. . . . 5 |- ( 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 ) ) ) ) ) )
147		fveq2 6191	. . . . . . . . 9 |- ( g = f -> (deg ` g ) = (deg ` f ) )
148	147	eqeq2d 2632	. . . . . . . 8 |- ( g = f -> ( ( d + 1 ) = (deg ` g ) <-> ( d + 1 ) = (deg ` f ) ) )
149		cnveq 5296	. . . . . . . . . . 11 |- ( g = f -> `' g = `' f )
150	149	imaeq1d 5465	. . . . . . . . . 10 |- ( g = f -> ( `' g " { 0 } ) = ( `' f " { 0 } ) )
151	150	fveq2d 6195	. . . . . . . . 9 |- ( g = f -> ( # ` ( `' g " { 0 } ) ) = ( # ` ( `' f " { 0 } ) ) )
152	151, 147	eqeq12d 2637	. . . . . . . 8 |- ( g = f -> ( ( # ` ( `' g " { 0 } ) ) = (deg ` g ) <-> ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) )
153	148, 152	anbi12d 747	. . . . . . 7 |- ( g = f -> ( ( ( d + 1 ) = (deg ` g ) /\ ( # ` ( `' g " { 0 } ) ) = (deg ` g ) ) <-> ( ( d + 1 ) = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) ) )
154	150	sumeq1d 14431	. . . . . . . 8 |- ( g = f -> sum_ x e. ( `' g " { 0 } ) x = sum_ x e. ( `' f " { 0 } ) x )
155		fveq2 6191	. . . . . . . . . . 11 |- ( g = f -> (coeff ` g ) = (coeff ` f ) )
156	147	oveq1d 6665	. . . . . . . . . . 11 |- ( g = f -> ( (deg ` g ) - 1 ) = ( (deg ` f ) - 1 ) )
157	155, 156	fveq12d 6197	. . . . . . . . . 10 |- ( g = f -> ( (coeff ` g ) ` ( (deg ` g ) - 1 ) ) = ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) )
158	155, 147	fveq12d 6197	. . . . . . . . . 10 |- ( g = f -> ( (coeff ` g ) ` (deg ` g ) ) = ( (coeff ` f ) ` (deg ` f ) ) )
159	157, 158	oveq12d 6668	. . . . . . . . 9 |- ( g = f -> ( ( (coeff ` g ) ` ( (deg ` g ) - 1 ) ) / ( (coeff ` g ) ` (deg ` g ) ) ) = ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) )
160	159	negeqd 10275	. . . . . . . 8 |- ( g = f -> -u ( ( (coeff ` g ) ` ( (deg ` g ) - 1 ) ) / ( (coeff ` g ) ` (deg ` g ) ) ) = -u ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) )
161	154, 160	eqeq12d 2637	. . . . . . 7 |- ( 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 ) ) ) ) )
162	153, 161	imbi12d 334	. . . . . 6 |- ( 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 ) ) ) ) ) )
163	162	cbvralv 3171	. . . . 5 |- ( 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 ) ) ) ) )
164	146, 163	syl6ib 241	. . . 4 |- ( 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 ) ) ) ) ) )
165	8, 12, 16, 20, 127, 164	nnind 11038	. . 3 |- ( 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 ) ) ) ) )
166	4, 165	syl 17	. 2 |- ( 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 ) ) ) ) )
167		vieta1.5	. 2 |- ( ph -> ( # ` R ) = N )
168		fveq2 6191	. . . . . . 7 |- ( f = F -> (deg ` f ) = (deg ` F ) )
169	168	eqeq2d 2632	. . . . . 6 |- ( f = F -> ( N = (deg ` f ) <-> N = (deg ` F ) ) )
170		cnveq 5296	. . . . . . . . . 10 |- ( f = F -> `' f = `' F )
171	170	imaeq1d 5465	. . . . . . . . 9 |- ( f = F -> ( `' f " { 0 } ) = ( `' F " { 0 } ) )
172		vieta1.3	. . . . . . . . 9 |- R = ( `' F " { 0 } )
173	171, 172	syl6eqr 2674	. . . . . . . 8 |- ( f = F -> ( `' f " { 0 } ) = R )
174	173	fveq2d 6195	. . . . . . 7 |- ( f = F -> ( # ` ( `' f " { 0 } ) ) = ( # ` R ) )
175		vieta1.2	. . . . . . . 8 |- N = (deg ` F )
176	168, 175	syl6eqr 2674	. . . . . . 7 |- ( f = F -> (deg ` f ) = N )
177	174, 176	eqeq12d 2637	. . . . . 6 |- ( f = F -> ( ( # ` ( `' f " { 0 } ) ) = (deg ` f ) <-> ( # ` R ) = N ) )
178	169, 177	anbi12d 747	. . . . 5 |- ( f = F -> ( ( N = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) <-> ( N = (deg ` F ) /\ ( # ` R ) = N ) ) )
179	175	biantrur 527	. . . . 5 |- ( ( # ` R ) = N <-> ( N = (deg ` F ) /\ ( # ` R ) = N ) )
180	178, 179	syl6bbr 278	. . . 4 |- ( f = F -> ( ( N = (deg ` f ) /\ ( # ` ( `' f " { 0 } ) ) = (deg ` f ) ) <-> ( # ` R ) = N ) )
181	173	sumeq1d 14431	. . . . 5 |- ( f = F -> sum_ x e. ( `' f " { 0 } ) x = sum_ x e. R x )
182		fveq2 6191	. . . . . . . . 9 |- ( f = F -> (coeff ` f ) = (coeff ` F ) )
183		vieta1.1	. . . . . . . . 9 |- A = (coeff ` F )
184	182, 183	syl6eqr 2674	. . . . . . . 8 |- ( f = F -> (coeff ` f ) = A )
185	176	oveq1d 6665	. . . . . . . 8 |- ( f = F -> ( (deg ` f ) - 1 ) = ( N - 1 ) )
186	184, 185	fveq12d 6197	. . . . . . 7 |- ( f = F -> ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) = ( A ` ( N - 1 ) ) )
187	184, 176	fveq12d 6197	. . . . . . 7 |- ( f = F -> ( (coeff ` f ) ` (deg ` f ) ) = ( A ` N ) )
188	186, 187	oveq12d 6668	. . . . . 6 |- ( f = F -> ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) = ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
189	188	negeqd 10275	. . . . 5 |- ( f = F -> -u ( ( (coeff ` f ) ` ( (deg ` f ) - 1 ) ) / ( (coeff ` f ) ` (deg ` f ) ) ) = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )
190	181, 189	eqeq12d 2637	. . . 4 |- ( 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 ) ) ) )
191	180, 190	imbi12d 334	. . 3 |- ( 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 ) ) ) ) )
192	191	rspcv 3305	. 2 |- ( F e. (Poly ` CC ) -> ( 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 ) ) ) ) -> ( ( # ` R ) = N -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) ) ) )
193	3, 166, 167, 192	syl3c 66	1 |- ( ph -> sum_ x e. R x = -u ( ( A ` ( N - 1 ) ) / ( A ` N ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   C_ wss 3574   {csn 4177   class class class wbr 4653   X. cxp 5112   `'ccnv 5113   "cima 5117   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   ~~ cen 7952   Fincfn 7955   CCcc 9934   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   <_ cle 10075   - cmin 10266   -ucneg 10267   / cdiv 10684   NNcn 11020   NN0cn0 11292   ZZcz 11377   ...cfz 12326   ^cexp 12860   #chash 13117   sum_csu 14416   0pc0p 23436  Polycply 23940   Xpcidp 23941  coeffccoe 23942  degcdgr 23943   quot cquot 24045

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-rlim 14220  df-sum 14417  df-0p 23437  df-ply 23944  df-idp 23945  df-coe 23946  df-dgr 23947  df-quot 24046

This theorem is referenced by:  basellem5  24811