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 ) ) )