Metamath Proof Explorer

Theorem vieta1lem1

Description: Lemma for vieta1 . (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 vieta1lem1 
|- ( ( ph /\ z e. R ) -> ( Q e. ( Poly ` CC ) /\ D = ( deg ` Q ) ) )

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 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
11 4 adantr 
 |-  ( ( ph /\ z e. R ) -> F e. ( Poly ` S ) )
12 10 11 sselid 
 |-  ( ( ph /\ z e. R ) -> F e. ( Poly ` CC ) )
13 cnvimass 
 |-  ( `' F " { 0 } ) C_ dom F
14 3 13 eqsstri 
 |-  R C_ dom F
15 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
16 4 15 syl 
 |-  ( ph -> F : CC --> CC )
17 14 16 fssdm 
 |-  ( ph -> R C_ CC )
18 17 sselda 
 |-  ( ( ph /\ z e. R ) -> z e. CC )
19 eqid 
 |-  ( Xp oF - ( CC X. { z } ) ) = ( Xp oF - ( CC X. { z } ) )
20 19 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 } ) )
21 18 20 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 } ) )
22 21 simp1d 
 |-  ( ( ph /\ z e. R ) -> ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) )
23 21 simp2d 
 |-  ( ( ph /\ z e. R ) -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = 1 )
24 ax-1ne0 
 |-  1 =/= 0
25 24 a1i 
 |-  ( ( ph /\ z e. R ) -> 1 =/= 0 )
26 23 25 eqnetrd 
 |-  ( ( ph /\ z e. R ) -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) =/= 0 )
27 fveq2 
 |-  ( ( Xp oF - ( CC X. { z } ) ) = 0p -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = ( deg ` 0p ) )
28 dgr0 
 |-  ( deg ` 0p ) = 0
29 27 28 eqtrdi 
 |-  ( ( Xp oF - ( CC X. { z } ) ) = 0p -> ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = 0 )
30 29 necon3i 
 |-  ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) =/= 0 -> ( Xp oF - ( CC X. { z } ) ) =/= 0p )
31 26 30 syl 
 |-  ( ( ph /\ z e. R ) -> ( Xp oF - ( CC X. { z } ) ) =/= 0p )
32 quotcl2 
 |-  ( ( F e. ( Poly ` CC ) /\ ( Xp oF - ( CC X. { z } ) ) e. ( Poly ` CC ) /\ ( Xp oF - ( CC X. { z } ) ) =/= 0p ) -> ( F quot ( Xp oF - ( CC X. { z } ) ) ) e. ( Poly ` CC ) )
33 12 22 31 32 syl3anc 
 |-  ( ( ph /\ z e. R ) -> ( F quot ( Xp oF - ( CC X. { z } ) ) ) e. ( Poly ` CC ) )
34 9 33 eqeltrid 
 |-  ( ( ph /\ z e. R ) -> Q e. ( Poly ` CC ) )
35 1cnd 
 |-  ( ( ph /\ z e. R ) -> 1 e. CC )
36 6 nncnd 
 |-  ( ph -> D e. CC )
37 36 adantr 
 |-  ( ( ph /\ z e. R ) -> D e. CC )
38 dgrcl 
 |-  ( Q e. ( Poly ` CC ) -> ( deg ` Q ) e. NN0 )
39 34 38 syl 
 |-  ( ( ph /\ z e. R ) -> ( deg ` Q ) e. NN0 )
40 39 nn0cnd 
 |-  ( ( ph /\ z e. R ) -> ( deg ` Q ) e. CC )
41 ax-1cn 
 |-  1 e. CC
42 addcom 
 |-  ( ( 1 e. CC /\ D e. CC ) -> ( 1 + D ) = ( D + 1 ) )
43 41 37 42 sylancr 
 |-  ( ( ph /\ z e. R ) -> ( 1 + D ) = ( D + 1 ) )
44 7 2 eqtrdi 
 |-  ( ph -> ( D + 1 ) = ( deg ` F ) )
45 44 adantr 
 |-  ( ( ph /\ z e. R ) -> ( D + 1 ) = ( deg ` F ) )
46 3 eleq2i 
 |-  ( z e. R <-> z e. ( `' F " { 0 } ) )
47 16 ffnd 
 |-  ( ph -> F Fn CC )
48 fniniseg 
 |-  ( F Fn CC -> ( z e. ( `' F " { 0 } ) <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
49 47 48 syl 
 |-  ( ph -> ( z e. ( `' F " { 0 } ) <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
50 46 49 syl5bb 
 |-  ( ph -> ( z e. R <-> ( z e. CC /\ ( F ` z ) = 0 ) ) )
51 50 simplbda 
 |-  ( ( ph /\ z e. R ) -> ( F ` z ) = 0 )
52 19 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 } ) ) ) ) )
53 11 18 51 52 syl3anc 
 |-  ( ( ph /\ z e. R ) -> F = ( ( Xp oF - ( CC X. { z } ) ) oF x. ( F quot ( Xp oF - ( CC X. { z } ) ) ) ) )
54 9 oveq2i 
 |-  ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) = ( ( Xp oF - ( CC X. { z } ) ) oF x. ( F quot ( Xp oF - ( CC X. { z } ) ) ) )
55 53 54 eqtr4di 
 |-  ( ( ph /\ z e. R ) -> F = ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) )
56 55 fveq2d 
 |-  ( ( ph /\ z e. R ) -> ( deg ` F ) = ( deg ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) )
57 6 peano2nnd 
 |-  ( ph -> ( D + 1 ) e. NN )
58 7 57 eqeltrrd 
 |-  ( ph -> N e. NN )
59 58 nnne0d 
 |-  ( ph -> N =/= 0 )
60 2 59 eqnetrrid 
 |-  ( ph -> ( deg ` F ) =/= 0 )
61 fveq2 
 |-  ( F = 0p -> ( deg ` F ) = ( deg ` 0p ) )
62 61 28 eqtrdi 
 |-  ( F = 0p -> ( deg ` F ) = 0 )
63 62 necon3i 
 |-  ( ( deg ` F ) =/= 0 -> F =/= 0p )
64 60 63 syl 
 |-  ( ph -> F =/= 0p )
65 64 adantr 
 |-  ( ( ph /\ z e. R ) -> F =/= 0p )
66 55 65 eqnetrrd 
 |-  ( ( ph /\ z e. R ) -> ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) =/= 0p )
67 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 ) ) )
68 22 34 67 syl2anc 
 |-  ( ( ph /\ z e. R ) -> ( ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) = 0p <-> ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) ) )
69 68 necon3abid 
 |-  ( ( ph /\ z e. R ) -> ( ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) =/= 0p <-> -. ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) ) )
70 66 69 mpbid 
 |-  ( ( ph /\ z e. R ) -> -. ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) )
71 neanior 
 |-  ( ( ( Xp oF - ( CC X. { z } ) ) =/= 0p /\ Q =/= 0p ) <-> -. ( ( Xp oF - ( CC X. { z } ) ) = 0p \/ Q = 0p ) )
72 70 71 sylibr 
 |-  ( ( ph /\ z e. R ) -> ( ( Xp oF - ( CC X. { z } ) ) =/= 0p /\ Q =/= 0p ) )
73 72 simprd 
 |-  ( ( ph /\ z e. R ) -> Q =/= 0p )
74 eqid 
 |-  ( deg ` ( Xp oF - ( CC X. { z } ) ) ) = ( deg ` ( Xp oF - ( CC X. { z } ) ) )
75 eqid 
 |-  ( deg ` Q ) = ( deg ` Q )
76 74 75 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 ) ) )
77 22 31 34 73 76 syl22anc 
 |-  ( ( ph /\ z e. R ) -> ( deg ` ( ( Xp oF - ( CC X. { z } ) ) oF x. Q ) ) = ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) )
78 45 56 77 3eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( D + 1 ) = ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) )
79 23 oveq1d 
 |-  ( ( ph /\ z e. R ) -> ( ( deg ` ( Xp oF - ( CC X. { z } ) ) ) + ( deg ` Q ) ) = ( 1 + ( deg ` Q ) ) )
80 43 78 79 3eqtrd 
 |-  ( ( ph /\ z e. R ) -> ( 1 + D ) = ( 1 + ( deg ` Q ) ) )
81 35 37 40 80 addcanad 
 |-  ( ( ph /\ z e. R ) -> D = ( deg ` Q ) )
82 34 81 jca 
 |-  ( ( ph /\ z e. R ) -> ( Q e. ( Poly ` CC ) /\ D = ( deg ` Q ) ) )