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 eqtrdi
 |-  ( ( `' 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 ) ) )