Metamath Proof Explorer

Theorem fta1lem

Description: Lemma for fta1 . (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Hypotheses fta1.1 
|- R = ( `' F " { 0 } )
fta1.2 
|- ( ph -> D e. NN0 )
fta1.3 
|- ( ph -> F e. ( ( Poly ` CC ) \ { 0p } ) )
fta1.4 
|- ( ph -> ( deg ` F ) = ( D + 1 ) )
fta1.5 
|- ( ph -> A e. ( `' F " { 0 } ) )
fta1.6 
|- ( ph -> A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = D -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) )
Assertion fta1lem 
|- ( ph -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) )

Proof

Step Hyp Ref Expression
1 fta1.1 
 |-  R = ( `' F " { 0 } )
2 fta1.2 
 |-  ( ph -> D e. NN0 )
3 fta1.3 
 |-  ( ph -> F e. ( ( Poly ` CC ) \ { 0p } ) )
4 fta1.4 
 |-  ( ph -> ( deg ` F ) = ( D + 1 ) )
5 fta1.5 
 |-  ( ph -> A e. ( `' F " { 0 } ) )
6 fta1.6 
 |-  ( ph -> A. g e. ( ( Poly ` CC ) \ { 0p } ) ( ( deg ` g ) = D -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) )
7 eldifsn 
 |-  ( F e. ( ( Poly ` CC ) \ { 0p } ) <-> ( F e. ( Poly ` CC ) /\ F =/= 0p ) )
8 3 7 sylib 
 |-  ( ph -> ( F e. ( Poly ` CC ) /\ F =/= 0p ) )
9 8 simpld 
 |-  ( ph -> F e. ( Poly ` CC ) )
10 plyf 
 |-  ( F e. ( Poly ` CC ) -> F : CC --> CC )
11 ffn 
 |-  ( F : CC --> CC -> F Fn CC )
12 fniniseg 
 |-  ( F Fn CC -> ( A e. ( `' F " { 0 } ) <-> ( A e. CC /\ ( F ` A ) = 0 ) ) )
13 9 10 11 12 4syl 
 |-  ( ph -> ( A e. ( `' F " { 0 } ) <-> ( A e. CC /\ ( F ` A ) = 0 ) ) )
14 5 13 mpbid 
 |-  ( ph -> ( A e. CC /\ ( F ` A ) = 0 ) )
15 14 simpld 
 |-  ( ph -> A e. CC )
16 14 simprd 
 |-  ( ph -> ( F ` A ) = 0 )
17 eqid 
 |-  ( Xp oF - ( CC X. { A } ) ) = ( Xp oF - ( CC X. { A } ) )
18 17 facth 
 |-  ( ( F e. ( Poly ` CC ) /\ A e. CC /\ ( F ` A ) = 0 ) -> F = ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) )
19 9 15 16 18 syl3anc 
 |-  ( ph -> F = ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) )
20 19 cnveqd 
 |-  ( ph -> `' F = `' ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) )
21 20 imaeq1d 
 |-  ( ph -> ( `' F " { 0 } ) = ( `' ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) " { 0 } ) )
22 cnex 
 |-  CC e. _V
23 22 a1i 
 |-  ( ph -> CC e. _V )
24 ssid 
 |-  CC C_ CC
25 ax-1cn 
 |-  1 e. CC
26 plyid 
 |-  ( ( CC C_ CC /\ 1 e. CC ) -> Xp e. ( Poly ` CC ) )
27 24 25 26 mp2an 
 |-  Xp e. ( Poly ` CC )
28 plyconst 
 |-  ( ( CC C_ CC /\ A e. CC ) -> ( CC X. { A } ) e. ( Poly ` CC ) )
29 24 15 28 sylancr 
 |-  ( ph -> ( CC X. { A } ) e. ( Poly ` CC ) )
30 plysubcl 
 |-  ( ( Xp e. ( Poly ` CC ) /\ ( CC X. { A } ) e. ( Poly ` CC ) ) -> ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) )
31 27 29 30 sylancr 
 |-  ( ph -> ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) )
32 plyf 
 |-  ( ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) -> ( Xp oF - ( CC X. { A } ) ) : CC --> CC )
33 31 32 syl 
 |-  ( ph -> ( Xp oF - ( CC X. { A } ) ) : CC --> CC )
34 17 plyremlem 
 |-  ( A e. CC -> ( ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { A } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { A } ) ) " { 0 } ) = { A } ) )
35 15 34 syl 
 |-  ( ph -> ( ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) /\ ( deg ` ( Xp oF - ( CC X. { A } ) ) ) = 1 /\ ( `' ( Xp oF - ( CC X. { A } ) ) " { 0 } ) = { A } ) )
36 35 simp2d 
 |-  ( ph -> ( deg ` ( Xp oF - ( CC X. { A } ) ) ) = 1 )
37 ax-1ne0 
 |-  1 =/= 0
38 37 a1i 
 |-  ( ph -> 1 =/= 0 )
39 36 38 eqnetrd 
 |-  ( ph -> ( deg ` ( Xp oF - ( CC X. { A } ) ) ) =/= 0 )
40 fveq2 
 |-  ( ( Xp oF - ( CC X. { A } ) ) = 0p -> ( deg ` ( Xp oF - ( CC X. { A } ) ) ) = ( deg ` 0p ) )
41 dgr0 
 |-  ( deg ` 0p ) = 0
42 40 41 eqtrdi 
 |-  ( ( Xp oF - ( CC X. { A } ) ) = 0p -> ( deg ` ( Xp oF - ( CC X. { A } ) ) ) = 0 )
43 42 necon3i 
 |-  ( ( deg ` ( Xp oF - ( CC X. { A } ) ) ) =/= 0 -> ( Xp oF - ( CC X. { A } ) ) =/= 0p )
44 39 43 syl 
 |-  ( ph -> ( Xp oF - ( CC X. { A } ) ) =/= 0p )
45 quotcl2 
 |-  ( ( F e. ( Poly ` CC ) /\ ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) /\ ( Xp oF - ( CC X. { A } ) ) =/= 0p ) -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( Poly ` CC ) )
46 9 31 44 45 syl3anc 
 |-  ( ph -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( Poly ` CC ) )
47 plyf 
 |-  ( ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( Poly ` CC ) -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) : CC --> CC )
48 46 47 syl 
 |-  ( ph -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) : CC --> CC )
49 ofmulrt 
 |-  ( ( CC e. _V /\ ( Xp oF - ( CC X. { A } ) ) : CC --> CC /\ ( F quot ( Xp oF - ( CC X. { A } ) ) ) : CC --> CC ) -> ( `' ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) " { 0 } ) = ( ( `' ( Xp oF - ( CC X. { A } ) ) " { 0 } ) u. ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) )
50 23 33 48 49 syl3anc 
 |-  ( ph -> ( `' ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) " { 0 } ) = ( ( `' ( Xp oF - ( CC X. { A } ) ) " { 0 } ) u. ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) )
51 35 simp3d 
 |-  ( ph -> ( `' ( Xp oF - ( CC X. { A } ) ) " { 0 } ) = { A } )
52 51 uneq1d 
 |-  ( ph -> ( ( `' ( Xp oF - ( CC X. { A } ) ) " { 0 } ) u. ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) = ( { A } u. ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) )
53 21 50 52 3eqtrd 
 |-  ( ph -> ( `' F " { 0 } ) = ( { A } u. ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) )
54 uncom 
 |-  ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) = ( { A } u. ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) )
55 53 1 54 3eqtr4g 
 |-  ( ph -> R = ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) )
56 25 a1i 
 |-  ( ph -> 1 e. CC )
57 dgrcl 
 |-  ( ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( Poly ` CC ) -> ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) e. NN0 )
58 46 57 syl 
 |-  ( ph -> ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) e. NN0 )
59 58 nn0cnd 
 |-  ( ph -> ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) e. CC )
60 2 nn0cnd 
 |-  ( ph -> D e. CC )
61 addcom 
 |-  ( ( 1 e. CC /\ D e. CC ) -> ( 1 + D ) = ( D + 1 ) )
62 25 60 61 sylancr 
 |-  ( ph -> ( 1 + D ) = ( D + 1 ) )
63 19 fveq2d 
 |-  ( ph -> ( deg ` F ) = ( deg ` ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
64 8 simprd 
 |-  ( ph -> F =/= 0p )
65 19 eqcomd 
 |-  ( ph -> ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = F )
66 0cnd 
 |-  ( ph -> 0 e. CC )
67 mul01 
 |-  ( x e. CC -> ( x x. 0 ) = 0 )
68 67 adantl 
 |-  ( ( ph /\ x e. CC ) -> ( x x. 0 ) = 0 )
69 23 33 66 66 68 caofid1 
 |-  ( ph -> ( ( Xp oF - ( CC X. { A } ) ) oF x. ( CC X. { 0 } ) ) = ( CC X. { 0 } ) )
70 df-0p 
 |-  0p = ( CC X. { 0 } )
71 70 oveq2i 
 |-  ( ( Xp oF - ( CC X. { A } ) ) oF x. 0p ) = ( ( Xp oF - ( CC X. { A } ) ) oF x. ( CC X. { 0 } ) )
72 69 71 70 3eqtr4g 
 |-  ( ph -> ( ( Xp oF - ( CC X. { A } ) ) oF x. 0p ) = 0p )
73 64 65 72 3netr4d 
 |-  ( ph -> ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) =/= ( ( Xp oF - ( CC X. { A } ) ) oF x. 0p ) )
74 oveq2 
 |-  ( ( F quot ( Xp oF - ( CC X. { A } ) ) ) = 0p -> ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = ( ( Xp oF - ( CC X. { A } ) ) oF x. 0p ) )
75 74 necon3i 
 |-  ( ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) =/= ( ( Xp oF - ( CC X. { A } ) ) oF x. 0p ) -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) =/= 0p )
76 73 75 syl 
 |-  ( ph -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) =/= 0p )
77 eqid 
 |-  ( deg ` ( Xp oF - ( CC X. { A } ) ) ) = ( deg ` ( Xp oF - ( CC X. { A } ) ) )
78 eqid 
 |-  ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) )
79 77 78 dgrmul 
 |-  ( ( ( ( Xp oF - ( CC X. { A } ) ) e. ( Poly ` CC ) /\ ( Xp oF - ( CC X. { A } ) ) =/= 0p ) /\ ( ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( Poly ` CC ) /\ ( F quot ( Xp oF - ( CC X. { A } ) ) ) =/= 0p ) ) -> ( deg ` ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) = ( ( deg ` ( Xp oF - ( CC X. { A } ) ) ) + ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
80 31 44 46 76 79 syl22anc 
 |-  ( ph -> ( deg ` ( ( Xp oF - ( CC X. { A } ) ) oF x. ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) = ( ( deg ` ( Xp oF - ( CC X. { A } ) ) ) + ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
81 63 4 80 3eqtr3d 
 |-  ( ph -> ( D + 1 ) = ( ( deg ` ( Xp oF - ( CC X. { A } ) ) ) + ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
82 36 oveq1d 
 |-  ( ph -> ( ( deg ` ( Xp oF - ( CC X. { A } ) ) ) + ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) = ( 1 + ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
83 62 81 82 3eqtrrd 
 |-  ( ph -> ( 1 + ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) = ( 1 + D ) )
84 56 59 60 83 addcanad 
 |-  ( ph -> ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = D )
85 fveqeq2 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( ( deg ` g ) = D <-> ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = D ) )
86 cnveq 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> `' g = `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) )
87 86 imaeq1d 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( `' g " { 0 } ) = ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) )
88 87 eleq1d 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( ( `' g " { 0 } ) e. Fin <-> ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin ) )
89 87 fveq2d 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( # ` ( `' g " { 0 } ) ) = ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) )
90 fveq2 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( deg ` g ) = ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) )
91 89 90 breq12d 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) <-> ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
92 88 91 anbi12d 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) <-> ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin /\ ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) ) )
93 85 92 imbi12d 
 |-  ( g = ( F quot ( Xp oF - ( CC X. { A } ) ) ) -> ( ( ( deg ` g ) = D -> ( ( `' g " { 0 } ) e. Fin /\ ( # ` ( `' g " { 0 } ) ) <_ ( deg ` g ) ) ) <-> ( ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = D -> ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin /\ ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) ) ) )
94 eldifsn 
 |-  ( ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( ( Poly ` CC ) \ { 0p } ) <-> ( ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( Poly ` CC ) /\ ( F quot ( Xp oF - ( CC X. { A } ) ) ) =/= 0p ) )
95 46 76 94 sylanbrc 
 |-  ( ph -> ( F quot ( Xp oF - ( CC X. { A } ) ) ) e. ( ( Poly ` CC ) \ { 0p } ) )
96 93 6 95 rspcdva 
 |-  ( ph -> ( ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) = D -> ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin /\ ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) ) )
97 84 96 mpd 
 |-  ( ph -> ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin /\ ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) ) )
98 97 simpld 
 |-  ( ph -> ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin )
99 snfi 
 |-  { A } e. Fin
100 unfi 
 |-  ( ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin /\ { A } e. Fin ) -> ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) e. Fin )
101 98 99 100 sylancl 
 |-  ( ph -> ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) e. Fin )
102 55 101 eqeltrd 
 |-  ( ph -> R e. Fin )
103 55 fveq2d 
 |-  ( ph -> ( # ` R ) = ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) )
104 hashcl 
 |-  ( ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) e. Fin -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) e. NN0 )
105 101 104 syl 
 |-  ( ph -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) e. NN0 )
106 105 nn0red 
 |-  ( ph -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) e. RR )
107 hashcl 
 |-  ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin -> ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) e. NN0 )
108 98 107 syl 
 |-  ( ph -> ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) e. NN0 )
109 108 nn0red 
 |-  ( ph -> ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) e. RR )
110 peano2re 
 |-  ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) e. RR -> ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + 1 ) e. RR )
111 109 110 syl 
 |-  ( ph -> ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + 1 ) e. RR )
112 dgrcl 
 |-  ( F e. ( Poly ` CC ) -> ( deg ` F ) e. NN0 )
113 9 112 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
114 113 nn0red 
 |-  ( ph -> ( deg ` F ) e. RR )
115 hashun2 
 |-  ( ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) e. Fin /\ { A } e. Fin ) -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) <_ ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + ( # ` { A } ) ) )
116 98 99 115 sylancl 
 |-  ( ph -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) <_ ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + ( # ` { A } ) ) )
117 hashsng 
 |-  ( A e. CC -> ( # ` { A } ) = 1 )
118 15 117 syl 
 |-  ( ph -> ( # ` { A } ) = 1 )
119 118 oveq2d 
 |-  ( ph -> ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + ( # ` { A } ) ) = ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + 1 ) )
120 116 119 breqtrd 
 |-  ( ph -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) <_ ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + 1 ) )
121 2 nn0red 
 |-  ( ph -> D e. RR )
122 1red 
 |-  ( ph -> 1 e. RR )
123 97 simprd 
 |-  ( ph -> ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ ( deg ` ( F quot ( Xp oF - ( CC X. { A } ) ) ) ) )
124 123 84 breqtrd 
 |-  ( ph -> ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) <_ D )
125 109 121 122 124 leadd1dd 
 |-  ( ph -> ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + 1 ) <_ ( D + 1 ) )
126 125 4 breqtrrd 
 |-  ( ph -> ( ( # ` ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) ) + 1 ) <_ ( deg ` F ) )
127 106 111 114 120 126 letrd 
 |-  ( ph -> ( # ` ( ( `' ( F quot ( Xp oF - ( CC X. { A } ) ) ) " { 0 } ) u. { A } ) ) <_ ( deg ` F ) )
128 103 127 eqbrtrd 
 |-  ( ph -> ( # ` R ) <_ ( deg ` F ) )
129 102 128 jca 
 |-  ( ph -> ( R e. Fin /\ ( # ` R ) <_ ( deg ` F ) ) )