Metamath Proof Explorer

Theorem plydivlem4

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

Ref Expression
Hypotheses plydiv.pl 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
plydiv.tm 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
plydiv.rc 
|- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
plydiv.m1 
|- ( ph -> -u 1 e. S )
plydiv.f 
|- ( ph -> F e. ( Poly ` S ) )
plydiv.g 
|- ( ph -> G e. ( Poly ` S ) )
plydiv.z 
|- ( ph -> G =/= 0p )
plydiv.r 
|- R = ( F oF - ( G oF x. q ) )
plydiv.d 
|- ( ph -> D e. NN0 )
plydiv.e 
|- ( ph -> ( M - N ) = D )
plydiv.fz 
|- ( ph -> F =/= 0p )
plydiv.u 
|- U = ( f oF - ( G oF x. p ) )
plydiv.h 
|- H = ( z e. CC |-> ( ( ( A ` M ) / ( B ` N ) ) x. ( z ^ D ) ) )
plydiv.al 
|- ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - N ) < D ) -> E. p e. ( Poly ` S ) ( U = 0p \/ ( deg ` U ) < N ) ) )
plydiv.a 
|- A = ( coeff ` F )
plydiv.b 
|- B = ( coeff ` G )
plydiv.m 
|- M = ( deg ` F )
plydiv.n 
|- N = ( deg ` G )
Assertion plydivlem4 
|- ( ph -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < N ) )

Proof

Step Hyp Ref Expression
1 plydiv.pl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
2 plydiv.tm 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
3 plydiv.rc 
 |-  ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
4 plydiv.m1 
 |-  ( ph -> -u 1 e. S )
5 plydiv.f 
 |-  ( ph -> F e. ( Poly ` S ) )
6 plydiv.g 
 |-  ( ph -> G e. ( Poly ` S ) )
7 plydiv.z 
 |-  ( ph -> G =/= 0p )
8 plydiv.r 
 |-  R = ( F oF - ( G oF x. q ) )
9 plydiv.d 
 |-  ( ph -> D e. NN0 )
10 plydiv.e 
 |-  ( ph -> ( M - N ) = D )
11 plydiv.fz 
 |-  ( ph -> F =/= 0p )
12 plydiv.u 
 |-  U = ( f oF - ( G oF x. p ) )
13 plydiv.h 
 |-  H = ( z e. CC |-> ( ( ( A ` M ) / ( B ` N ) ) x. ( z ^ D ) ) )
14 plydiv.al 
 |-  ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - N ) < D ) -> E. p e. ( Poly ` S ) ( U = 0p \/ ( deg ` U ) < N ) ) )
15 plydiv.a 
 |-  A = ( coeff ` F )
16 plydiv.b 
 |-  B = ( coeff ` G )
17 plydiv.m 
 |-  M = ( deg ` F )
18 plydiv.n 
 |-  N = ( deg ` G )
19 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
20 5 19 syl 
 |-  ( ph -> S C_ CC )
21 1 2 3 4 plydivlem1 
 |-  ( ph -> 0 e. S )
22 15 coef2 
 |-  ( ( F e. ( Poly ` S ) /\ 0 e. S ) -> A : NN0 --> S )
23 5 21 22 syl2anc 
 |-  ( ph -> A : NN0 --> S )
24 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
25 5 24 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
26 17 25 eqeltrid 
 |-  ( ph -> M e. NN0 )
27 23 26 ffvelrnd 
 |-  ( ph -> ( A ` M ) e. S )
28 20 27 sseldd 
 |-  ( ph -> ( A ` M ) e. CC )
29 16 coef2 
 |-  ( ( G e. ( Poly ` S ) /\ 0 e. S ) -> B : NN0 --> S )
30 6 21 29 syl2anc 
 |-  ( ph -> B : NN0 --> S )
31 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
32 6 31 syl 
 |-  ( ph -> ( deg ` G ) e. NN0 )
33 18 32 eqeltrid 
 |-  ( ph -> N e. NN0 )
34 30 33 ffvelrnd 
 |-  ( ph -> ( B ` N ) e. S )
35 20 34 sseldd 
 |-  ( ph -> ( B ` N ) e. CC )
36 18 16 dgreq0 
 |-  ( G e. ( Poly ` S ) -> ( G = 0p <-> ( B ` N ) = 0 ) )
37 6 36 syl 
 |-  ( ph -> ( G = 0p <-> ( B ` N ) = 0 ) )
38 37 necon3bid 
 |-  ( ph -> ( G =/= 0p <-> ( B ` N ) =/= 0 ) )
39 7 38 mpbid 
 |-  ( ph -> ( B ` N ) =/= 0 )
40 28 35 39 divrecd 
 |-  ( ph -> ( ( A ` M ) / ( B ` N ) ) = ( ( A ` M ) x. ( 1 / ( B ` N ) ) ) )
41 fvex 
 |-  ( B ` N ) e. _V
42 eleq1 
 |-  ( x = ( B ` N ) -> ( x e. S <-> ( B ` N ) e. S ) )
43 neeq1 
 |-  ( x = ( B ` N ) -> ( x =/= 0 <-> ( B ` N ) =/= 0 ) )
44 42 43 anbi12d 
 |-  ( x = ( B ` N ) -> ( ( x e. S /\ x =/= 0 ) <-> ( ( B ` N ) e. S /\ ( B ` N ) =/= 0 ) ) )
45 44 anbi2d 
 |-  ( x = ( B ` N ) -> ( ( ph /\ ( x e. S /\ x =/= 0 ) ) <-> ( ph /\ ( ( B ` N ) e. S /\ ( B ` N ) =/= 0 ) ) ) )
46 oveq2 
 |-  ( x = ( B ` N ) -> ( 1 / x ) = ( 1 / ( B ` N ) ) )
47 46 eleq1d 
 |-  ( x = ( B ` N ) -> ( ( 1 / x ) e. S <-> ( 1 / ( B ` N ) ) e. S ) )
48 45 47 imbi12d 
 |-  ( x = ( B ` N ) -> ( ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S ) <-> ( ( ph /\ ( ( B ` N ) e. S /\ ( B ` N ) =/= 0 ) ) -> ( 1 / ( B ` N ) ) e. S ) ) )
49 41 48 3 vtocl 
 |-  ( ( ph /\ ( ( B ` N ) e. S /\ ( B ` N ) =/= 0 ) ) -> ( 1 / ( B ` N ) ) e. S )
50 49 ex 
 |-  ( ph -> ( ( ( B ` N ) e. S /\ ( B ` N ) =/= 0 ) -> ( 1 / ( B ` N ) ) e. S ) )
51 34 39 50 mp2and 
 |-  ( ph -> ( 1 / ( B ` N ) ) e. S )
52 2 27 51 caovcld 
 |-  ( ph -> ( ( A ` M ) x. ( 1 / ( B ` N ) ) ) e. S )
53 40 52 eqeltrd 
 |-  ( ph -> ( ( A ` M ) / ( B ` N ) ) e. S )
54 13 ply1term 
 |-  ( ( S C_ CC /\ ( ( A ` M ) / ( B ` N ) ) e. S /\ D e. NN0 ) -> H e. ( Poly ` S ) )
55 20 53 9 54 syl3anc 
 |-  ( ph -> H e. ( Poly ` S ) )
56 55 adantr 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> H e. ( Poly ` S ) )
57 simpr 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> p e. ( Poly ` S ) )
58 1 adantlr 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
59 56 57 58 plyadd 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( H oF + p ) e. ( Poly ` S ) )
60 cnex 
 |-  CC e. _V
61 60 a1i 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> CC e. _V )
62 5 adantr 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> F e. ( Poly ` S ) )
63 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
64 62 63 syl 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> F : CC --> CC )
65 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
66 65 adantl 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
67 plyf 
 |-  ( H e. ( Poly ` S ) -> H : CC --> CC )
68 56 67 syl 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> H : CC --> CC )
69 6 adantr 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
70 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
71 69 70 syl 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> G : CC --> CC )
72 inidm 
 |-  ( CC i^i CC ) = CC
73 66 68 71 61 61 72 off 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( H oF x. G ) : CC --> CC )
74 plyf 
 |-  ( p e. ( Poly ` S ) -> p : CC --> CC )
75 74 adantl 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> p : CC --> CC )
76 66 71 75 61 61 72 off 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( G oF x. p ) : CC --> CC )
77 subsub4 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x - y ) - z ) = ( x - ( y + z ) ) )
78 77 adantl 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x - y ) - z ) = ( x - ( y + z ) ) )
79 61 64 73 76 78 caofass 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = ( F oF - ( ( H oF x. G ) oF + ( G oF x. p ) ) ) )
80 mulcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
81 80 adantl 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) = ( y x. x ) )
82 61 68 71 81 caofcom 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( H oF x. G ) = ( G oF x. H ) )
83 82 oveq1d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( H oF x. G ) oF + ( G oF x. p ) ) = ( ( G oF x. H ) oF + ( G oF x. p ) ) )
84 adddi 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
85 84 adantl 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( x x. ( y + z ) ) = ( ( x x. y ) + ( x x. z ) ) )
86 61 71 68 75 85 caofdi 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( G oF x. ( H oF + p ) ) = ( ( G oF x. H ) oF + ( G oF x. p ) ) )
87 83 86 eqtr4d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( H oF x. G ) oF + ( G oF x. p ) ) = ( G oF x. ( H oF + p ) ) )
88 87 oveq2d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( F oF - ( ( H oF x. G ) oF + ( G oF x. p ) ) ) = ( F oF - ( G oF x. ( H oF + p ) ) ) )
89 79 88 eqtrd 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = ( F oF - ( G oF x. ( H oF + p ) ) ) )
90 89 eqeq1d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p <-> ( F oF - ( G oF x. ( H oF + p ) ) ) = 0p ) )
91 89 fveq2d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) = ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) )
92 91 breq1d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N <-> ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) < N ) )
93 90 92 orbi12d 
 |-  ( ( ph /\ p e. ( Poly ` S ) ) -> ( ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) <-> ( ( F oF - ( G oF x. ( H oF + p ) ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) < N ) ) )
94 93 biimpa 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) ) -> ( ( F oF - ( G oF x. ( H oF + p ) ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) < N ) )
95 oveq2 
 |-  ( q = ( H oF + p ) -> ( G oF x. q ) = ( G oF x. ( H oF + p ) ) )
96 95 oveq2d 
 |-  ( q = ( H oF + p ) -> ( F oF - ( G oF x. q ) ) = ( F oF - ( G oF x. ( H oF + p ) ) ) )
97 8 96 syl5eq 
 |-  ( q = ( H oF + p ) -> R = ( F oF - ( G oF x. ( H oF + p ) ) ) )
98 97 eqeq1d 
 |-  ( q = ( H oF + p ) -> ( R = 0p <-> ( F oF - ( G oF x. ( H oF + p ) ) ) = 0p ) )
99 97 fveq2d 
 |-  ( q = ( H oF + p ) -> ( deg ` R ) = ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) )
100 99 breq1d 
 |-  ( q = ( H oF + p ) -> ( ( deg ` R ) < N <-> ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) < N ) )
101 98 100 orbi12d 
 |-  ( q = ( H oF + p ) -> ( ( R = 0p \/ ( deg ` R ) < N ) <-> ( ( F oF - ( G oF x. ( H oF + p ) ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) < N ) ) )
102 101 rspcev 
 |-  ( ( ( H oF + p ) e. ( Poly ` S ) /\ ( ( F oF - ( G oF x. ( H oF + p ) ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. ( H oF + p ) ) ) ) < N ) ) -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < N ) )
103 59 94 102 syl2an2r 
 |-  ( ( ( ph /\ p e. ( Poly ` S ) ) /\ ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) ) -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < N ) )
104 55 6 1 2 plymul 
 |-  ( ph -> ( H oF x. G ) e. ( Poly ` S ) )
105 eqid 
 |-  ( deg ` ( H oF x. G ) ) = ( deg ` ( H oF x. G ) )
106 17 105 dgrsub 
 |-  ( ( F e. ( Poly ` S ) /\ ( H oF x. G ) e. ( Poly ` S ) ) -> ( deg ` ( F oF - ( H oF x. G ) ) ) <_ if ( M <_ ( deg ` ( H oF x. G ) ) , ( deg ` ( H oF x. G ) ) , M ) )
107 5 104 106 syl2anc 
 |-  ( ph -> ( deg ` ( F oF - ( H oF x. G ) ) ) <_ if ( M <_ ( deg ` ( H oF x. G ) ) , ( deg ` ( H oF x. G ) ) , M ) )
108 17 15 dgreq0 
 |-  ( F e. ( Poly ` S ) -> ( F = 0p <-> ( A ` M ) = 0 ) )
109 5 108 syl 
 |-  ( ph -> ( F = 0p <-> ( A ` M ) = 0 ) )
110 109 necon3bid 
 |-  ( ph -> ( F =/= 0p <-> ( A ` M ) =/= 0 ) )
111 11 110 mpbid 
 |-  ( ph -> ( A ` M ) =/= 0 )
112 28 35 111 39 divne0d 
 |-  ( ph -> ( ( A ` M ) / ( B ` N ) ) =/= 0 )
113 20 53 sseldd 
 |-  ( ph -> ( ( A ` M ) / ( B ` N ) ) e. CC )
114 13 coe1term 
 |-  ( ( ( ( A ` M ) / ( B ` N ) ) e. CC /\ D e. NN0 /\ D e. NN0 ) -> ( ( coeff ` H ) ` D ) = if ( D = D , ( ( A ` M ) / ( B ` N ) ) , 0 ) )
115 113 9 9 114 syl3anc 
 |-  ( ph -> ( ( coeff ` H ) ` D ) = if ( D = D , ( ( A ` M ) / ( B ` N ) ) , 0 ) )
116 eqid 
 |-  D = D
117 116 iftruei 
 |-  if ( D = D , ( ( A ` M ) / ( B ` N ) ) , 0 ) = ( ( A ` M ) / ( B ` N ) )
118 115 117 eqtrdi 
 |-  ( ph -> ( ( coeff ` H ) ` D ) = ( ( A ` M ) / ( B ` N ) ) )
119 c0ex 
 |-  0 e. _V
120 119 fvconst2 
 |-  ( D e. NN0 -> ( ( NN0 X. { 0 } ) ` D ) = 0 )
121 9 120 syl 
 |-  ( ph -> ( ( NN0 X. { 0 } ) ` D ) = 0 )
122 112 118 121 3netr4d 
 |-  ( ph -> ( ( coeff ` H ) ` D ) =/= ( ( NN0 X. { 0 } ) ` D ) )
123 fveq2 
 |-  ( H = 0p -> ( coeff ` H ) = ( coeff ` 0p ) )
124 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
125 123 124 eqtrdi 
 |-  ( H = 0p -> ( coeff ` H ) = ( NN0 X. { 0 } ) )
126 125 fveq1d 
 |-  ( H = 0p -> ( ( coeff ` H ) ` D ) = ( ( NN0 X. { 0 } ) ` D ) )
127 126 necon3i 
 |-  ( ( ( coeff ` H ) ` D ) =/= ( ( NN0 X. { 0 } ) ` D ) -> H =/= 0p )
128 122 127 syl 
 |-  ( ph -> H =/= 0p )
129 eqid 
 |-  ( deg ` H ) = ( deg ` H )
130 129 18 dgrmul 
 |-  ( ( ( H e. ( Poly ` S ) /\ H =/= 0p ) /\ ( G e. ( Poly ` S ) /\ G =/= 0p ) ) -> ( deg ` ( H oF x. G ) ) = ( ( deg ` H ) + N ) )
131 55 128 6 7 130 syl22anc 
 |-  ( ph -> ( deg ` ( H oF x. G ) ) = ( ( deg ` H ) + N ) )
132 13 dgr1term 
 |-  ( ( ( ( A ` M ) / ( B ` N ) ) e. CC /\ ( ( A ` M ) / ( B ` N ) ) =/= 0 /\ D e. NN0 ) -> ( deg ` H ) = D )
133 113 112 9 132 syl3anc 
 |-  ( ph -> ( deg ` H ) = D )
134 133 10 eqtr4d 
 |-  ( ph -> ( deg ` H ) = ( M - N ) )
135 134 oveq1d 
 |-  ( ph -> ( ( deg ` H ) + N ) = ( ( M - N ) + N ) )
136 26 nn0cnd 
 |-  ( ph -> M e. CC )
137 33 nn0cnd 
 |-  ( ph -> N e. CC )
138 136 137 npcand 
 |-  ( ph -> ( ( M - N ) + N ) = M )
139 135 138 eqtrd 
 |-  ( ph -> ( ( deg ` H ) + N ) = M )
140 131 139 eqtrd 
 |-  ( ph -> ( deg ` ( H oF x. G ) ) = M )
141 140 ifeq1d 
 |-  ( ph -> if ( M <_ ( deg ` ( H oF x. G ) ) , ( deg ` ( H oF x. G ) ) , M ) = if ( M <_ ( deg ` ( H oF x. G ) ) , M , M ) )
142 ifid 
 |-  if ( M <_ ( deg ` ( H oF x. G ) ) , M , M ) = M
143 141 142 eqtrdi 
 |-  ( ph -> if ( M <_ ( deg ` ( H oF x. G ) ) , ( deg ` ( H oF x. G ) ) , M ) = M )
144 107 143 breqtrd 
 |-  ( ph -> ( deg ` ( F oF - ( H oF x. G ) ) ) <_ M )
145 eqid 
 |-  ( coeff ` ( H oF x. G ) ) = ( coeff ` ( H oF x. G ) )
146 15 145 coesub 
 |-  ( ( F e. ( Poly ` S ) /\ ( H oF x. G ) e. ( Poly ` S ) ) -> ( coeff ` ( F oF - ( H oF x. G ) ) ) = ( A oF - ( coeff ` ( H oF x. G ) ) ) )
147 5 104 146 syl2anc 
 |-  ( ph -> ( coeff ` ( F oF - ( H oF x. G ) ) ) = ( A oF - ( coeff ` ( H oF x. G ) ) ) )
148 147 fveq1d 
 |-  ( ph -> ( ( coeff ` ( F oF - ( H oF x. G ) ) ) ` M ) = ( ( A oF - ( coeff ` ( H oF x. G ) ) ) ` M ) )
149 15 coef3 
 |-  ( F e. ( Poly ` S ) -> A : NN0 --> CC )
150 ffn 
 |-  ( A : NN0 --> CC -> A Fn NN0 )
151 5 149 150 3syl 
 |-  ( ph -> A Fn NN0 )
152 145 coef3 
 |-  ( ( H oF x. G ) e. ( Poly ` S ) -> ( coeff ` ( H oF x. G ) ) : NN0 --> CC )
153 ffn 
 |-  ( ( coeff ` ( H oF x. G ) ) : NN0 --> CC -> ( coeff ` ( H oF x. G ) ) Fn NN0 )
154 104 152 153 3syl 
 |-  ( ph -> ( coeff ` ( H oF x. G ) ) Fn NN0 )
155 nn0ex 
 |-  NN0 e. _V
156 155 a1i 
 |-  ( ph -> NN0 e. _V )
157 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
158 eqidd 
 |-  ( ( ph /\ M e. NN0 ) -> ( A ` M ) = ( A ` M ) )
159 eqid 
 |-  ( coeff ` H ) = ( coeff ` H )
160 159 16 129 18 coemulhi 
 |-  ( ( H e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( ( coeff ` ( H oF x. G ) ) ` ( ( deg ` H ) + N ) ) = ( ( ( coeff ` H ) ` ( deg ` H ) ) x. ( B ` N ) ) )
161 55 6 160 syl2anc 
 |-  ( ph -> ( ( coeff ` ( H oF x. G ) ) ` ( ( deg ` H ) + N ) ) = ( ( ( coeff ` H ) ` ( deg ` H ) ) x. ( B ` N ) ) )
162 139 fveq2d 
 |-  ( ph -> ( ( coeff ` ( H oF x. G ) ) ` ( ( deg ` H ) + N ) ) = ( ( coeff ` ( H oF x. G ) ) ` M ) )
163 133 fveq2d 
 |-  ( ph -> ( ( coeff ` H ) ` ( deg ` H ) ) = ( ( coeff ` H ) ` D ) )
164 163 118 eqtrd 
 |-  ( ph -> ( ( coeff ` H ) ` ( deg ` H ) ) = ( ( A ` M ) / ( B ` N ) ) )
165 164 oveq1d 
 |-  ( ph -> ( ( ( coeff ` H ) ` ( deg ` H ) ) x. ( B ` N ) ) = ( ( ( A ` M ) / ( B ` N ) ) x. ( B ` N ) ) )
166 28 35 39 divcan1d 
 |-  ( ph -> ( ( ( A ` M ) / ( B ` N ) ) x. ( B ` N ) ) = ( A ` M ) )
167 165 166 eqtrd 
 |-  ( ph -> ( ( ( coeff ` H ) ` ( deg ` H ) ) x. ( B ` N ) ) = ( A ` M ) )
168 161 162 167 3eqtr3d 
 |-  ( ph -> ( ( coeff ` ( H oF x. G ) ) ` M ) = ( A ` M ) )
169 168 adantr 
 |-  ( ( ph /\ M e. NN0 ) -> ( ( coeff ` ( H oF x. G ) ) ` M ) = ( A ` M ) )
170 151 154 156 156 157 158 169 ofval 
 |-  ( ( ph /\ M e. NN0 ) -> ( ( A oF - ( coeff ` ( H oF x. G ) ) ) ` M ) = ( ( A ` M ) - ( A ` M ) ) )
171 26 170 mpdan 
 |-  ( ph -> ( ( A oF - ( coeff ` ( H oF x. G ) ) ) ` M ) = ( ( A ` M ) - ( A ` M ) ) )
172 28 subidd 
 |-  ( ph -> ( ( A ` M ) - ( A ` M ) ) = 0 )
173 148 171 172 3eqtrd 
 |-  ( ph -> ( ( coeff ` ( F oF - ( H oF x. G ) ) ) ` M ) = 0 )
174 5 104 1 2 4 plysub 
 |-  ( ph -> ( F oF - ( H oF x. G ) ) e. ( Poly ` S ) )
175 dgrcl 
 |-  ( ( F oF - ( H oF x. G ) ) e. ( Poly ` S ) -> ( deg ` ( F oF - ( H oF x. G ) ) ) e. NN0 )
176 174 175 syl 
 |-  ( ph -> ( deg ` ( F oF - ( H oF x. G ) ) ) e. NN0 )
177 176 nn0red 
 |-  ( ph -> ( deg ` ( F oF - ( H oF x. G ) ) ) e. RR )
178 26 nn0red 
 |-  ( ph -> M e. RR )
179 33 nn0red 
 |-  ( ph -> N e. RR )
180 177 178 179 ltsub1d 
 |-  ( ph -> ( ( deg ` ( F oF - ( H oF x. G ) ) ) < M <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < ( M - N ) ) )
181 10 breq2d 
 |-  ( ph -> ( ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < ( M - N ) <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) )
182 180 181 bitrd 
 |-  ( ph -> ( ( deg ` ( F oF - ( H oF x. G ) ) ) < M <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) )
183 182 orbi2d 
 |-  ( ph -> ( ( ( F oF - ( H oF x. G ) ) = 0p \/ ( deg ` ( F oF - ( H oF x. G ) ) ) < M ) <-> ( ( F oF - ( H oF x. G ) ) = 0p \/ ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) ) )
184 eqid 
 |-  ( deg ` ( F oF - ( H oF x. G ) ) ) = ( deg ` ( F oF - ( H oF x. G ) ) )
185 eqid 
 |-  ( coeff ` ( F oF - ( H oF x. G ) ) ) = ( coeff ` ( F oF - ( H oF x. G ) ) )
186 184 185 dgrlt 
 |-  ( ( ( F oF - ( H oF x. G ) ) e. ( Poly ` S ) /\ M e. NN0 ) -> ( ( ( F oF - ( H oF x. G ) ) = 0p \/ ( deg ` ( F oF - ( H oF x. G ) ) ) < M ) <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) <_ M /\ ( ( coeff ` ( F oF - ( H oF x. G ) ) ) ` M ) = 0 ) ) )
187 174 26 186 syl2anc 
 |-  ( ph -> ( ( ( F oF - ( H oF x. G ) ) = 0p \/ ( deg ` ( F oF - ( H oF x. G ) ) ) < M ) <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) <_ M /\ ( ( coeff ` ( F oF - ( H oF x. G ) ) ) ` M ) = 0 ) ) )
188 183 187 bitr3d 
 |-  ( ph -> ( ( ( F oF - ( H oF x. G ) ) = 0p \/ ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) <_ M /\ ( ( coeff ` ( F oF - ( H oF x. G ) ) ) ` M ) = 0 ) ) )
189 144 173 188 mpbir2and 
 |-  ( ph -> ( ( F oF - ( H oF x. G ) ) = 0p \/ ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) )
190 eqeq1 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( f = 0p <-> ( F oF - ( H oF x. G ) ) = 0p ) )
191 fveq2 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( deg ` f ) = ( deg ` ( F oF - ( H oF x. G ) ) ) )
192 191 oveq1d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( ( deg ` f ) - N ) = ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) )
193 192 breq1d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( ( ( deg ` f ) - N ) < D <-> ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) )
194 190 193 orbi12d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( ( f = 0p \/ ( ( deg ` f ) - N ) < D ) <-> ( ( F oF - ( H oF x. G ) ) = 0p \/ ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) ) )
195 oveq1 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( f oF - ( G oF x. p ) ) = ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) )
196 12 195 syl5eq 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> U = ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) )
197 196 eqeq1d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( U = 0p <-> ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p ) )
198 196 fveq2d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( deg ` U ) = ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) )
199 198 breq1d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( ( deg ` U ) < N <-> ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) )
200 197 199 orbi12d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( ( U = 0p \/ ( deg ` U ) < N ) <-> ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) ) )
201 200 rexbidv 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( E. p e. ( Poly ` S ) ( U = 0p \/ ( deg ` U ) < N ) <-> E. p e. ( Poly ` S ) ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) ) )
202 194 201 imbi12d 
 |-  ( f = ( F oF - ( H oF x. G ) ) -> ( ( ( f = 0p \/ ( ( deg ` f ) - N ) < D ) -> E. p e. ( Poly ` S ) ( U = 0p \/ ( deg ` U ) < N ) ) <-> ( ( ( F oF - ( H oF x. G ) ) = 0p \/ ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) -> E. p e. ( Poly ` S ) ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) ) ) )
203 202 14 174 rspcdva 
 |-  ( ph -> ( ( ( F oF - ( H oF x. G ) ) = 0p \/ ( ( deg ` ( F oF - ( H oF x. G ) ) ) - N ) < D ) -> E. p e. ( Poly ` S ) ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) ) )
204 189 203 mpd 
 |-  ( ph -> E. p e. ( Poly ` S ) ( ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( ( F oF - ( H oF x. G ) ) oF - ( G oF x. p ) ) ) < N ) )
205 103 204 r19.29a 
 |-  ( ph -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < N ) )