Metamath Proof Explorer

Theorem fta1

Description: The easy direction of the Fundamental Theorem of Algebra: A nonzero polynomial has at most deg ( F ) roots. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypothesis fta1.1 
|- R = ( `' F " { 0 } )
Assertion fta1 
|- ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) )

Proof

Step Hyp Ref Expression
1 fta1.1 
 |-  R = ( `' F " { 0 } )
2 eqid 
 |-  ( deg ` F ) = ( deg ` F )
3 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
4 3 adantr 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( deg ` F ) e. NN0 )
5 eqeq2 
 |-  ( x = 0 -> ( ( deg ` f ) = x <-> ( deg ` f ) = 0 ) )
6 5 imbi1d 
 |-  ( x = 0 -> ( ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> ( ( deg ` f ) = 0 -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
7 6 ralbidv 
 |-  ( x = 0 -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = 0 -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
8 eqeq2 
 |-  ( x = d -> ( ( deg ` f ) = x <-> ( deg ` f ) = d ) )
9 8 imbi1d 
 |-  ( x = d -> ( ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> ( ( deg ` f ) = d -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
10 9 ralbidv 
 |-  ( x = d -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = d -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
11 eqeq2 
 |-  ( x = ( d + 1 ) -> ( ( deg ` f ) = x <-> ( deg ` f ) = ( d + 1 ) ) )
12 11 imbi1d 
 |-  ( x = ( d + 1 ) -> ( ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> ( ( deg ` f ) = ( d + 1 ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
13 12 ralbidv 
 |-  ( x = ( d + 1 ) -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( d + 1 ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
14 eqeq2 
 |-  ( x = ( deg ` F ) -> ( ( deg ` f ) = x <-> ( deg ` f ) = ( deg ` F ) ) )
15 14 imbi1d 
 |-  ( x = ( deg ` F ) -> ( ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
16 15 ralbidv 
 |-  ( x = ( deg ` F ) -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = x -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
17 eldifsni 
 |-  ( f e. ( ( Poly ` CC ) \ { 0p } ) -> f =/= 0p )
18 17 adantr 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> f =/= 0p )
19 simplr 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( deg ` f ) = 0 )
20 eldifi 
 |-  ( f e. ( ( Poly ` CC ) \ { 0p } ) -> f e. ( Poly ` CC ) )
21 20 ad2antrr 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> f e. ( Poly ` CC ) )
22 0dgrb 
 |-  ( f e. ( Poly ` CC ) -> ( ( deg ` f ) = 0 <-> f = ( CC X. { ( f ` 0 ) } ) ) )
23 21 22 syl 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( ( deg ` f ) = 0 <-> f = ( CC X. { ( f ` 0 ) } ) ) )
24 19 23 mpbid 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> f = ( CC X. { ( f ` 0 ) } ) )
25 24 fveq1d 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( f ` x ) = ( ( CC X. { ( f ` 0 ) } ) ` x ) )
26 20 adantr 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> f e. ( Poly ` CC ) )
27 plyf 
 |-  ( f e. ( Poly ` CC ) -> f : CC --> CC )
28 ffn 
 |-  ( f : CC --> CC -> f Fn CC )
29 fniniseg 
 |-  ( f Fn CC -> ( x e. ( `' f " { 0 } ) <-> ( x e. CC /\ ( f ` x ) = 0 ) ) )
30 26 27 28 29 4syl 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> ( x e. ( `' f " { 0 } ) <-> ( x e. CC /\ ( f ` x ) = 0 ) ) )
31 30 biimpa 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( x e. CC /\ ( f ` x ) = 0 ) )
32 31 simprd 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( f ` x ) = 0 )
33 31 simpld 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> x e. CC )
34 fvex 
 |-  ( f ` 0 ) e. _V
35 34 fvconst2 
 |-  ( x e. CC -> ( ( CC X. { ( f ` 0 ) } ) ` x ) = ( f ` 0 ) )
36 33 35 syl 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( ( CC X. { ( f ` 0 ) } ) ` x ) = ( f ` 0 ) )
37 25 32 36 3eqtr3rd 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( f ` 0 ) = 0 )
38 37 sneqd 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> { ( f ` 0 ) } = { 0 } )
39 38 xpeq2d 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> ( CC X. { ( f ` 0 ) } ) = ( CC X. { 0 } ) )
40 24 39 eqtrd 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> f = ( CC X. { 0 } ) )
41 df-0p 
 |-  0p = ( CC X. { 0 } )
42 40 41 eqtr4di 
 |-  ( ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) /\ x e. ( `' f " { 0 } ) ) -> f = 0p )
43 42 ex 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> ( x e. ( `' f " { 0 } ) -> f = 0p ) )
44 43 necon3ad 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> ( f =/= 0p -> -. x e. ( `' f " { 0 } ) ) )
45 18 44 mpd 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> -. x e. ( `' f " { 0 } ) )
46 45 eq0rdv 
 |-  ( ( f e. ( ( Poly ` CC ) \ { 0p } ) /\ ( deg ` f ) = 0 ) -> ( `' f " { 0 } ) = (/) )
47 46 ex 
 |-  ( f e. ( ( Poly ` CC ) \ { 0p } ) -> ( ( deg ` f ) = 0 -> ( `' f " { 0 } ) = (/) ) )
48 dgrcl 
 |-  ( f e. ( Poly ` CC ) -> ( deg ` f ) e. NN0 )
49 nn0ge0 
 |-  ( ( deg ` f ) e. NN0 -> 0 <_ ( deg ` f ) )
50 20 48 49 3syl 
 |-  ( f e. ( ( Poly ` CC ) \ { 0p } ) -> 0 <_ ( deg ` f ) )
51 id 
 |-  ( ( `' f " { 0 } ) = (/) -> ( `' f " { 0 } ) = (/) )
52 0fin 
 |-  (/) e. Fin
53 51 52 eqeltrdi 
 |-  ( ( `' f " { 0 } ) = (/) -> ( `' f " { 0 } ) e. Fin )
54 53 biantrurd 
 |-  ( ( `' f " { 0 } ) = (/) -> ( ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) <-> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
55 fveq2 
 |-  ( ( `' f " { 0 } ) = (/) -> ( # ` ( `' f " { 0 } ) ) = ( # ` (/) ) )
56 hash0 
 |-  ( # ` (/) ) = 0
57 55 56 syl6eq 
 |-  ( ( `' f " { 0 } ) = (/) -> ( # ` ( `' f " { 0 } ) ) = 0 )
58 57 breq1d 
 |-  ( ( `' f " { 0 } ) = (/) -> ( ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) <-> 0 <_ ( deg ` f ) ) )
59 54 58 bitr3d 
 |-  ( ( `' f " { 0 } ) = (/) -> ( ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) <-> 0 <_ ( deg ` f ) ) )
60 50 59 syl5ibrcom 
 |-  ( f e. ( ( Poly ` CC ) \ { 0p } ) -> ( ( `' f " { 0 } ) = (/) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
61 47 60 syld 
 |-  ( f e. ( ( Poly ` CC ) \ { 0p } ) -> ( ( deg ` f ) = 0 -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
62 61 rgen 
 |-  A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = 0 -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) )
63 fveqeq2 
 |-  ( f = g -> ( ( deg ` f ) = d <-> ( deg ` g ) = d ) )
64 cnveq 
 |-  ( f = g -> `' f = `' g )
65 64 imaeq1d 
 |-  ( f = g -> ( `' f " { 0 } ) = ( `' g " { 0 } ) )
66 65 eleq1d 
 |-  ( f = g -> ( ( `' f " { 0 } ) e. Fin <-> ( `' g " { 0 } ) e. Fin ) )
67 65 fveq2d 
 |-  ( f = g -> ( # ` ( `' f " { 0 } ) ) = ( # ` ( `' g " { 0 } ) ) )
68 fveq2 
 |-  ( f = g -> ( deg ` f ) = ( deg ` g ) )
69 67 68 breq12d 
 |-  ( f = g -> ( ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) <-> ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) )
70 66 69 anbi12d 
 |-  ( f = g -> ( ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) <-> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) )
71 63 70 imbi12d 
 |-  ( f = g -> ( ( ( deg ` f ) = d -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) )
72 71 cbvralvw 
 |-  ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = d -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) )
73 50 ad2antlr 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> 0 <_ ( deg ` f ) )
74 73 59 syl5ibrcom 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> ( ( `' f " { 0 } ) = (/) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
75 74 a1dd 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> ( ( `' f " { 0 } ) = (/) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
76 n0 
 |-  ( ( `' f " { 0 } ) =/= (/) <-> E. x x e. ( `' f " { 0 } ) )
77 eqid 
 |-  ( `' f " { 0 } ) = ( `' f " { 0 } )
78 simplll 
 |-  ( ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) /\ ( x e. ( `' f " { 0 } ) /\ A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) ) -> d e. NN0 )
79 simpllr 
 |-  ( ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) /\ ( x e. ( `' f " { 0 } ) /\ A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) ) -> f e. ( ( Poly ` CC ) \ { 0p } ) )
80 simplr 
 |-  ( ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) /\ ( x e. ( `' f " { 0 } ) /\ A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) ) -> ( deg ` f ) = ( d + 1 ) )
81 simprl 
 |-  ( ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) /\ ( x e. ( `' f " { 0 } ) /\ A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) ) -> x e. ( `' f " { 0 } ) )
82 simprr 
 |-  ( ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) /\ ( x e. ( `' f " { 0 } ) /\ A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) ) -> A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) )
83 77 78 79 80 81 82 fta1lem 
 |-  ( ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) /\ ( x e. ( `' f " { 0 } ) /\ A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) )
84 83 exp32 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> ( x e. ( `' f " { 0 } ) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
85 84 exlimdv 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> ( E. x x e. ( `' f " { 0 } ) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
86 76 85 syl5bi 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> ( ( `' f " { 0 } ) =/= (/) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
87 75 86 pm2.61dne 
 |-  ( ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) /\ ( deg ` f ) = ( d + 1 ) ) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
88 87 ex 
 |-  ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) -> ( ( deg ` f ) = ( d + 1 ) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
89 88 com23 
 |-  ( ( d e. NN0 /\ f e. ( ( Poly ` CC ) \ { 0p } ) ) -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> ( ( deg ` f ) = ( d + 1 ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
90 89 ralrimdva 
 |-  ( d e. NN0 -> ( A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = d -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) -> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( d + 1 ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
91 72 90 syl5bi 
 |-  ( d e. NN0 -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = d -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) -> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( d + 1 ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) ) )
92 7 10 13 16 62 91 nn0ind 
 |-  ( ( deg ` F ) e. NN0 -> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
93 4 92 syl 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) )
94 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
95 94 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
96 eldifsn 
 |-  ( F e. ( ( Poly ` CC ) \ { 0p } ) <-> ( F e. ( Poly ` CC ) /\ F =/= 0p ) )
97 fveqeq2 
 |-  ( f = F -> ( ( deg ` f ) = ( deg ` F ) <-> ( deg ` F ) = ( deg ` F ) ) )
98 cnveq 
 |-  ( f = F -> `' f = `' F )
99 98 imaeq1d 
 |-  ( f = F -> ( `' f " { 0 } ) = ( `' F " { 0 } ) )
100 99 1 eqtr4di 
 |-  ( f = F -> ( `' f " { 0 } ) = R )
101 100 eleq1d 
 |-  ( f = F -> ( ( `' f " { 0 } ) e. Fin <-> R e. Fin ) )
102 100 fveq2d 
 |-  ( f = F -> ( # ` ( `' f " { 0 } ) ) = ( # ` R ) )
103 fveq2 
 |-  ( f = F -> ( deg ` f ) = ( deg ` F ) )
104 102 103 breq12d 
 |-  ( f = F -> ( ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) <-> ( # ` R ) <_ ( deg ` F ) ) )
105 101 104 anbi12d 
 |-  ( f = F -> ( ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) <-> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) ) )
106 97 105 imbi12d 
 |-  ( f = F -> ( ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) <-> ( ( deg ` F ) = ( deg ` F ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) ) ) )
107 106 rspcv 
 |-  ( F e. ( ( Poly ` CC ) \ { 0p } ) -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) -> ( ( deg ` F ) = ( deg ` F ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) ) ) )
108 96 107 sylbir 
 |-  ( ( F e. ( Poly ` CC ) /\ F =/= 0p ) -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) -> ( ( deg ` F ) = ( deg ` F ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) ) ) )
109 95 108 sylan 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( A. f e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` f ) = ( deg ` F ) -> ( ( `' f " { 0 } ) e. Fin /\ ( # ` ( `' f " { 0 } ) ) <_ ( deg ` f ) ) ) -> ( ( deg ` F ) = ( deg ` F ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) ) ) )
110 93 109 mpd 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( ( deg ` F ) = ( deg ` F ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) ) )
111 2 110 mpi 
 |-  ( ( F e. ( Poly ` S ) /\ F =/= 0p ) -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) )