Metamath Proof Explorer

Theorem plydivex

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-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 ) )
Assertion plydivex 
|- ( ph -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )

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 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
10 5 9 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
11 10 nn0red 
 |-  ( ph -> ( deg ` F ) e. RR )
12 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
13 6 12 syl 
 |-  ( ph -> ( deg ` G ) e. NN0 )
14 13 nn0red 
 |-  ( ph -> ( deg ` G ) e. RR )
15 11 14 resubcld 
 |-  ( ph -> ( ( deg ` F ) - ( deg ` G ) ) e. RR )
16 arch 
 |-  ( ( ( deg ` F ) - ( deg ` G ) ) e. RR -> E. d e. NN ( ( deg ` F ) - ( deg ` G ) ) < d )
17 15 16 syl 
 |-  ( ph -> E. d e. NN ( ( deg ` F ) - ( deg ` G ) ) < d )
18 olc 
 |-  ( ( ( deg ` F ) - ( deg ` G ) ) < d -> ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < d ) )
19 eqeq1 
 |-  ( f = F -> ( f = 0p <-> F = 0p ) )
20 fveq2 
 |-  ( f = F -> ( deg ` f ) = ( deg ` F ) )
21 20 oveq1d 
 |-  ( f = F -> ( ( deg ` f ) - ( deg ` G ) ) = ( ( deg ` F ) - ( deg ` G ) ) )
22 21 breq1d 
 |-  ( f = F -> ( ( ( deg ` f ) - ( deg ` G ) ) < d <-> ( ( deg ` F ) - ( deg ` G ) ) < d ) )
23 19 22 orbi12d 
 |-  ( f = F -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) <-> ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < d ) ) )
24 oveq1 
 |-  ( f = F -> ( f oF - ( G oF x. q ) ) = ( F oF - ( G oF x. q ) ) )
25 24 8 eqtr4di 
 |-  ( f = F -> ( f oF - ( G oF x. q ) ) = R )
26 25 eqeq1d 
 |-  ( f = F -> ( ( f oF - ( G oF x. q ) ) = 0p <-> R = 0p ) )
27 25 fveq2d 
 |-  ( f = F -> ( deg ` ( f oF - ( G oF x. q ) ) ) = ( deg ` R ) )
28 27 breq1d 
 |-  ( f = F -> ( ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) <-> ( deg ` R ) < ( deg ` G ) ) )
29 26 28 orbi12d 
 |-  ( f = F -> ( ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
30 29 rexbidv 
 |-  ( f = F -> ( E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
31 23 30 imbi12d 
 |-  ( f = F -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) ) )
32 nnnn0 
 |-  ( d e. NN -> d e. NN0 )
33 breq2 
 |-  ( x = 0 -> ( ( ( deg ` f ) - ( deg ` G ) ) < x <-> ( ( deg ` f ) - ( deg ` G ) ) < 0 ) )
34 33 orbi2d 
 |-  ( x = 0 -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) <-> ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) )
35 34 imbi1d 
 |-  ( x = 0 -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
36 35 ralbidv 
 |-  ( x = 0 -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
37 36 imbi2d 
 |-  ( x = 0 -> ( ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) <-> ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
38 breq2 
 |-  ( x = d -> ( ( ( deg ` f ) - ( deg ` G ) ) < x <-> ( ( deg ` f ) - ( deg ` G ) ) < d ) )
39 38 orbi2d 
 |-  ( x = d -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) <-> ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) ) )
40 39 imbi1d 
 |-  ( x = d -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
41 40 ralbidv 
 |-  ( x = d -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
42 41 imbi2d 
 |-  ( x = d -> ( ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) <-> ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
43 breq2 
 |-  ( x = ( d + 1 ) -> ( ( ( deg ` f ) - ( deg ` G ) ) < x <-> ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) )
44 43 orbi2d 
 |-  ( x = ( d + 1 ) -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) <-> ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) ) )
45 44 imbi1d 
 |-  ( x = ( d + 1 ) -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
46 45 ralbidv 
 |-  ( x = ( d + 1 ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
47 46 imbi2d 
 |-  ( x = ( d + 1 ) -> ( ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < x ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) <-> ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
48 1 adantlr 
 |-  ( ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
49 2 adantlr 
 |-  ( ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
50 3 adantlr 
 |-  ( ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
51 4 adantr 
 |-  ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) -> -u 1 e. S )
52 simprl 
 |-  ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) -> f e. ( Poly ` S ) )
53 6 adantr 
 |-  ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) -> G e. ( Poly ` S ) )
54 7 adantr 
 |-  ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) -> G =/= 0p )
55 eqid 
 |-  ( f oF - ( G oF x. q ) ) = ( f oF - ( G oF x. q ) )
56 simprr 
 |-  ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) -> ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) )
57 48 49 50 51 52 53 54 55 56 plydivlem3 
 |-  ( ( ph /\ ( f e. ( Poly ` S ) /\ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
58 57 expr 
 |-  ( ( ph /\ f e. ( Poly ` S ) ) -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
59 58 ralrimiva 
 |-  ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < 0 ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
60 eqeq1 
 |-  ( f = g -> ( f = 0p <-> g = 0p ) )
61 fveq2 
 |-  ( f = g -> ( deg ` f ) = ( deg ` g ) )
62 61 oveq1d 
 |-  ( f = g -> ( ( deg ` f ) - ( deg ` G ) ) = ( ( deg ` g ) - ( deg ` G ) ) )
63 62 breq1d 
 |-  ( f = g -> ( ( ( deg ` f ) - ( deg ` G ) ) < d <-> ( ( deg ` g ) - ( deg ` G ) ) < d ) )
64 60 63 orbi12d 
 |-  ( f = g -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) <-> ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) ) )
65 oveq1 
 |-  ( f = g -> ( f oF - ( G oF x. q ) ) = ( g oF - ( G oF x. q ) ) )
66 65 eqeq1d 
 |-  ( f = g -> ( ( f oF - ( G oF x. q ) ) = 0p <-> ( g oF - ( G oF x. q ) ) = 0p ) )
67 65 fveq2d 
 |-  ( f = g -> ( deg ` ( f oF - ( G oF x. q ) ) ) = ( deg ` ( g oF - ( G oF x. q ) ) ) )
68 67 breq1d 
 |-  ( f = g -> ( ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) <-> ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
69 66 68 orbi12d 
 |-  ( f = g -> ( ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
70 69 rexbidv 
 |-  ( f = g -> ( E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
71 64 70 imbi12d 
 |-  ( f = g -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
72 71 cbvralvw 
 |-  ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
73 simplll 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> ph )
74 73 1 sylan 
 |-  ( ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
75 73 2 sylan 
 |-  ( ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
76 73 3 sylan 
 |-  ( ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
77 73 4 syl 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> -u 1 e. S )
78 simplr 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> f e. ( Poly ` S ) )
79 73 6 syl 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> G e. ( Poly ` S ) )
80 73 7 syl 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> G =/= 0p )
81 simpllr 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> d e. NN0 )
82 simprrr 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> ( ( deg ` f ) - ( deg ` G ) ) = d )
83 simprrl 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> f =/= 0p )
84 eqid 
 |-  ( g oF - ( G oF x. p ) ) = ( g oF - ( G oF x. p ) )
85 oveq1 
 |-  ( w = z -> ( w ^ d ) = ( z ^ d ) )
86 85 oveq2d 
 |-  ( w = z -> ( ( ( ( coeff ` f ) ` ( deg ` f ) ) / ( ( coeff ` G ) ` ( deg ` G ) ) ) x. ( w ^ d ) ) = ( ( ( ( coeff ` f ) ` ( deg ` f ) ) / ( ( coeff ` G ) ` ( deg ` G ) ) ) x. ( z ^ d ) ) )
87 86 cbvmptv 
 |-  ( w e. CC |-> ( ( ( ( coeff ` f ) ` ( deg ` f ) ) / ( ( coeff ` G ) ` ( deg ` G ) ) ) x. ( w ^ d ) ) ) = ( z e. CC |-> ( ( ( ( coeff ` f ) ` ( deg ` f ) ) / ( ( coeff ` G ) ` ( deg ` G ) ) ) x. ( z ^ d ) ) )
88 simprl 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
89 oveq2 
 |-  ( q = p -> ( G oF x. q ) = ( G oF x. p ) )
90 89 oveq2d 
 |-  ( q = p -> ( g oF - ( G oF x. q ) ) = ( g oF - ( G oF x. p ) ) )
91 90 eqeq1d 
 |-  ( q = p -> ( ( g oF - ( G oF x. q ) ) = 0p <-> ( g oF - ( G oF x. p ) ) = 0p ) )
92 90 fveq2d 
 |-  ( q = p -> ( deg ` ( g oF - ( G oF x. q ) ) ) = ( deg ` ( g oF - ( G oF x. p ) ) ) )
93 92 breq1d 
 |-  ( q = p -> ( ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) <-> ( deg ` ( g oF - ( G oF x. p ) ) ) < ( deg ` G ) ) )
94 91 93 orbi12d 
 |-  ( q = p -> ( ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> ( ( g oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) )
95 94 cbvrexvw 
 |-  ( E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> E. p e. ( Poly ` S ) ( ( g oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. p ) ) ) < ( deg ` G ) ) )
96 95 imbi2i 
 |-  ( ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. p e. ( Poly ` S ) ( ( g oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) )
97 96 ralbii 
 |-  ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. p e. ( Poly ` S ) ( ( g oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) )
98 88 97 sylib 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. p e. ( Poly ` S ) ( ( g oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) )
99 eqid 
 |-  ( coeff ` f ) = ( coeff ` f )
100 eqid 
 |-  ( coeff ` G ) = ( coeff ` G )
101 eqid 
 |-  ( deg ` f ) = ( deg ` f )
102 eqid 
 |-  ( deg ` G ) = ( deg ` G )
103 74 75 76 77 78 79 80 55 81 82 83 84 87 98 99 100 101 102 plydivlem4 
 |-  ( ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) /\ ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
104 103 exp32 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
105 104 ralrimdva 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. g e. ( Poly ` S ) ( ( g = 0p \/ ( ( deg ` g ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( g oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( g oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> A. f e. ( Poly ` S ) ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
106 72 105 biimtrid 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> A. f e. ( Poly ` S ) ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
107 106 ancld 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ A. f e. ( Poly ` S ) ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
108 dgrcl 
 |-  ( f e. ( Poly ` S ) -> ( deg ` f ) e. NN0 )
109 108 adantl 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( deg ` f ) e. NN0 )
110 109 nn0zd 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( deg ` f ) e. ZZ )
111 6 ad2antrr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> G e. ( Poly ` S ) )
112 111 12 syl 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( deg ` G ) e. NN0 )
113 112 nn0zd 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( deg ` G ) e. ZZ )
114 110 113 zsubcld 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( deg ` f ) - ( deg ` G ) ) e. ZZ )
115 nn0z 
 |-  ( d e. NN0 -> d e. ZZ )
116 115 ad2antlr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> d e. ZZ )
117 zleltp1 
 |-  ( ( ( ( deg ` f ) - ( deg ` G ) ) e. ZZ /\ d e. ZZ ) -> ( ( ( deg ` f ) - ( deg ` G ) ) <_ d <-> ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) )
118 114 116 117 syl2anc 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( ( deg ` f ) - ( deg ` G ) ) <_ d <-> ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) )
119 114 zred 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( deg ` f ) - ( deg ` G ) ) e. RR )
120 nn0re 
 |-  ( d e. NN0 -> d e. RR )
121 120 ad2antlr 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> d e. RR )
122 119 121 leloed 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( ( deg ` f ) - ( deg ` G ) ) <_ d <-> ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
123 118 122 bitr3d 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) <-> ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
124 123 orbi2d 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) <-> ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) )
125 pm5.63 
 |-  ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) <-> ( f = 0p \/ ( -. f = 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
126 df-ne 
 |-  ( f =/= 0p <-> -. f = 0p )
127 126 anbi1i 
 |-  ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) <-> ( -. f = 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) )
128 127 orbi2i 
 |-  ( ( f = 0p \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) <-> ( f = 0p \/ ( -. f = 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
129 125 128 bitr4i 
 |-  ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) <-> ( f = 0p \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
130 129 orbi2i 
 |-  ( ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) <-> ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f = 0p \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) )
131 or12 
 |-  ( ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) <-> ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
132 or12 
 |-  ( ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) <-> ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f = 0p \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) )
133 130 131 132 3bitr4i 
 |-  ( ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) <-> ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) )
134 orass 
 |-  ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) <-> ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) )
135 133 134 bitr4i 
 |-  ( ( f = 0p \/ ( ( ( deg ` f ) - ( deg ` G ) ) < d \/ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) <-> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) )
136 124 135 bitrdi 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) <-> ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) ) )
137 136 imbi1d 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
138 jaob 
 |-  ( ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) \/ ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
139 137 138 bitrdi 
 |-  ( ( ( ph /\ d e. NN0 ) /\ f e. ( Poly ` S ) ) -> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
140 139 ralbidva 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> A. f e. ( Poly ` S ) ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
141 r19.26 
 |-  ( A. f e. ( Poly ` S ) ( ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) <-> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ A. f e. ( Poly ` S ) ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
142 140 141 bitrdi 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) <-> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) /\ A. f e. ( Poly ` S ) ( ( f =/= 0p /\ ( ( deg ` f ) - ( deg ` G ) ) = d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
143 107 142 sylibrd 
 |-  ( ( ph /\ d e. NN0 ) -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
144 143 expcom 
 |-  ( d e. NN0 -> ( ph -> ( A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
145 144 a2d 
 |-  ( d e. NN0 -> ( ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) -> ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < ( d + 1 ) ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) ) )
146 37 42 47 42 59 145 nn0ind 
 |-  ( d e. NN0 -> ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
147 32 146 syl 
 |-  ( d e. NN -> ( ph -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) )
148 147 impcom 
 |-  ( ( ph /\ d e. NN ) -> A. f e. ( Poly ` S ) ( ( f = 0p \/ ( ( deg ` f ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( ( f oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( f oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
149 5 adantr 
 |-  ( ( ph /\ d e. NN ) -> F e. ( Poly ` S ) )
150 31 148 149 rspcdva 
 |-  ( ( ph /\ d e. NN ) -> ( ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < d ) -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
151 18 150 syl5 
 |-  ( ( ph /\ d e. NN ) -> ( ( ( deg ` F ) - ( deg ` G ) ) < d -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
152 151 rexlimdva 
 |-  ( ph -> ( E. d e. NN ( ( deg ` F ) - ( deg ` G ) ) < d -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
153 17 152 mpd 
 |-  ( ph -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )