Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . . . . 6
 Poly    |
2 | | dgrcl 23180 |
. . . . . 6
 Poly 
deg    |
3 | 1, 2 | syl 17 |
. . . . 5
 deg    |
4 | 3 | nn0red 10923 |
. . . 4
 deg    |
5 | | plydiv.g |
. . . . . 6
 Poly    |
6 | | dgrcl 23180 |
. . . . . 6
 Poly 
deg    |
7 | 5, 6 | syl 17 |
. . . . 5
 deg    |
8 | 7 | nn0red 10923 |
. . . 4
 deg    |
9 | 4, 8 | resubcld 10044 |
. . 3
  deg  deg     |
10 | | arch 10863 |
. . 3
  deg  deg     deg  deg  
  |
11 | 9, 10 | syl 17 |
. 2
   deg  deg  
  |
12 | | olc 386 |
. . . 4
  deg  deg  
   deg  deg      |
13 | 1 | adantr 467 |
. . . . 5
 

Poly    |
14 | | nnnn0 10873 |
. . . . . . 7
   |
15 | | breq2 4405 |
. . . . . . . . . . . 12
   deg  deg    deg  deg      |
16 | 15 | orbi2d 707 |
. . . . . . . . . . 11
     deg  deg   
   deg  deg       |
17 | 16 | imbi1d 319 |
. . . . . . . . . 10
      deg  deg  
  Poly      
    deg    
   deg        deg  deg  
  Poly      
    deg    
   deg       |
18 | 17 | ralbidv 2826 |
. . . . . . . . 9
  
Poly       deg  deg     Poly           deg    
   deg    
Poly       deg  deg     Poly           deg    
   deg       |
19 | 18 | imbi2d 318 |
. . . . . . . 8
  
 Poly       deg  deg  
  Poly      
    deg    
   deg       Poly       deg  deg     Poly           deg    
   deg        |
20 | | breq2 4405 |
. . . . . . . . . . . 12
   deg  deg    deg  deg      |
21 | 20 | orbi2d 707 |
. . . . . . . . . . 11
     deg  deg   
   deg  deg       |
22 | 21 | imbi1d 319 |
. . . . . . . . . 10
      deg  deg  
  Poly      
    deg    
   deg        deg  deg  
  Poly      
    deg    
   deg       |
23 | 22 | ralbidv 2826 |
. . . . . . . . 9
  
Poly       deg  deg     Poly           deg    
   deg    
Poly       deg  deg     Poly           deg    
   deg       |
24 | 23 | imbi2d 318 |
. . . . . . . 8
  
 Poly       deg  deg  
  Poly      
    deg    
   deg       Poly       deg  deg     Poly           deg    
   deg        |
25 | | breq2 4405 |
. . . . . . . . . . . 12
     deg  deg    deg  deg        |
26 | 25 | orbi2d 707 |
. . . . . . . . . . 11
       deg  deg   
   deg  deg         |
27 | 26 | imbi1d 319 |
. . . . . . . . . 10
        deg  deg  
  Poly      
    deg    
   deg        deg  deg  
    Poly      
    deg    
   deg       |
28 | 27 | ralbidv 2826 |
. . . . . . . . 9
    
Poly       deg  deg     Poly           deg    
   deg    
Poly       deg  deg       Poly           deg    
   deg       |
29 | 28 | imbi2d 318 |
. . . . . . . 8
    
 Poly       deg  deg  
  Poly      
    deg    
   deg       Poly       deg  deg       Poly           deg    
   deg        |
30 | | plydiv.pl |
. . . . . . . . . . . 12
 

      |
31 | 30 | adantlr 720 |
. . . . . . . . . . 11
    Poly     deg  deg             |
32 | | plydiv.tm |
. . . . . . . . . . . 12
 

      |
33 | 32 | adantlr 720 |
. . . . . . . . . . 11
    Poly     deg  deg             |
34 | | plydiv.rc |
. . . . . . . . . . . 12
 

      |
35 | 34 | adantlr 720 |
. . . . . . . . . . 11
    Poly     deg  deg             |
36 | | plydiv.m1 |
. . . . . . . . . . . 12
    |
37 | 36 | adantr 467 |
. . . . . . . . . . 11
 
 Poly     deg  deg     
   |
38 | | simprl 763 |
. . . . . . . . . . 11
 
 Poly     deg  deg     
Poly    |
39 | 5 | adantr 467 |
. . . . . . . . . . 11
 
 Poly     deg  deg     
Poly    |
40 | | plydiv.z |
. . . . . . . . . . . 12
    |
41 | 40 | adantr 467 |
. . . . . . . . . . 11
 
 Poly     deg  deg     
   |
42 | | eqid 2450 |
. . . . . . . . . . 11
        
    |
43 | | simprr 765 |
. . . . . . . . . . 11
 
 Poly     deg  deg     
   deg  deg      |
44 | 31, 33, 35, 37, 38, 39, 41, 42, 43 | plydivlem3 23241 |
. . . . . . . . . 10
 
 Poly     deg  deg     
 Poly           deg    
   deg     |
45 | 44 | expr 619 |
. . . . . . . . 9
 
Poly       deg  deg     Poly           deg    
   deg      |
46 | 45 | ralrimiva 2801 |
. . . . . . . 8
  Poly       deg  deg     Poly           deg    
   deg      |
47 | | eqeq1 2454 |
. . . . . . . . . . . . . . . 16
       |
48 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . 18
 deg  deg    |
49 | 48 | oveq1d 6303 |
. . . . . . . . . . . . . . . . 17
  deg  deg    deg  deg     |
50 | 49 | breq1d 4411 |
. . . . . . . . . . . . . . . 16
   deg  deg    deg  deg      |
51 | 47, 50 | orbi12d 715 |
. . . . . . . . . . . . . . 15
     deg  deg   
   deg  deg       |
52 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . 18
   
      
    |
53 | 52 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . 17
     
      
      |
54 | 52 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . 18
 deg    
   deg          |
55 | 54 | breq1d 4411 |
. . . . . . . . . . . . . . . . 17
  deg  
     deg  deg        deg     |
56 | 53, 55 | orbi12d 715 |
. . . . . . . . . . . . . . . 16
          deg    
   deg  
   
    deg    
   deg      |
57 | 56 | rexbidv 2900 |
. . . . . . . . . . . . . . 15
  
Poly      
    deg    
   deg  
 Poly           deg    
   deg      |
58 | 51, 57 | imbi12d 322 |
. . . . . . . . . . . . . 14
      deg  deg  
  Poly      
    deg    
   deg        deg  deg  
  Poly      
    deg    
   deg       |
59 | 58 | cbvralv 3018 |
. . . . . . . . . . . . 13
 
Poly       deg  deg     Poly           deg    
   deg    
Poly       deg  deg     Poly           deg    
   deg      |
60 | | simplll 767 |
. . . . . . . . . . . . . . . . 17
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg        |
61 | 60, 30 | sylan 474 |
. . . . . . . . . . . . . . . 16
     
Poly     Poly       deg  deg     Poly           deg    
   deg       deg  deg      
 
    |
62 | 60, 32 | sylan 474 |
. . . . . . . . . . . . . . . 16
     
Poly     Poly       deg  deg     Poly           deg    
   deg       deg  deg      
 
    |
63 | 60, 34 | sylan 474 |
. . . . . . . . . . . . . . . 16
     
Poly     Poly       deg  deg     Poly           deg    
   deg       deg  deg             |
64 | 60, 36 | syl 17 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg         |
65 | | simplr 761 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg      Poly    |
66 | 60, 5 | syl 17 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg      Poly    |
67 | 60, 40 | syl 17 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg         |
68 | | simpllr 768 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg        |
69 | | simprrr 774 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg       deg  deg     |
70 | | simprrl 773 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg         |
71 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
        
    |
72 | | oveq1 6295 |
. . . . . . . . . . . . . . . . . 18
           |
73 | 72 | oveq2d 6304 |
. . . . . . . . . . . . . . . . 17
    coeff    deg    coeff    deg            coeff    deg    coeff    deg           |
74 | 73 | cbvmptv 4494 |
. . . . . . . . . . . . . . . 16
    coeff    deg    coeff    deg              coeff    deg    coeff    deg           |
75 | | simprl 763 |
. . . . . . . . . . . . . . . . 17
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg       Poly       deg  deg  
  Poly      
    deg    
   deg      |
76 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . . . . 23
         |
77 | 76 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . . . 22
   
      
    |
78 | 77 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . . . 21
     
      
      |
79 | 77 | fveq2d 5867 |
. . . . . . . . . . . . . . . . . . . . . 22
 deg    
   deg          |
80 | 79 | breq1d 4411 |
. . . . . . . . . . . . . . . . . . . . 21
  deg  
     deg  deg        deg     |
81 | 78, 80 | orbi12d 715 |
. . . . . . . . . . . . . . . . . . . 20
          deg    
   deg  
   
    deg    
   deg      |
82 | 81 | cbvrexv 3019 |
. . . . . . . . . . . . . . . . . . 19
  Poly      
    deg    
   deg  
 Poly           deg    
   deg     |
83 | 82 | imbi2i 314 |
. . . . . . . . . . . . . . . . . 18
     deg  deg    
Poly      
    deg    
   deg        deg  deg  
  Poly      
    deg    
   deg      |
84 | 83 | ralbii 2818 |
. . . . . . . . . . . . . . . . 17
 
Poly       deg  deg     Poly           deg    
   deg    
Poly       deg  deg     Poly           deg    
   deg      |
85 | 75, 84 | sylib 200 |
. . . . . . . . . . . . . . . 16
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg       Poly       deg  deg  
  Poly      
    deg    
   deg      |
86 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
coeff  coeff   |
87 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
coeff  coeff   |
88 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
deg  deg   |
89 | | eqid 2450 |
. . . . . . . . . . . . . . . 16
deg  deg   |
90 | 61, 62, 63, 64, 65, 66, 67, 42, 68, 69, 70, 71, 74, 85, 86, 87, 88, 89 | plydivlem4 23242 |
. . . . . . . . . . . . . . 15
   

Poly    
Poly       deg  deg     Poly           deg    
   deg       deg  deg       Poly           deg    
   deg     |
91 | 90 | exp32 609 |
. . . . . . . . . . . . . 14
    Poly  
 
Poly       deg  deg     Poly           deg    
   deg        deg  deg     Poly      
    deg    
   deg       |
92 | 91 | ralrimdva 2805 |
. . . . . . . . . . . . 13
 

 
Poly       deg  deg     Poly           deg    
   deg     Poly       deg  deg     Poly           deg    
   deg       |
93 | 59, 92 | syl5bi 221 |
. . . . . . . . . . . 12
 

 
Poly       deg  deg     Poly           deg    
   deg     Poly       deg  deg     Poly           deg    
   deg       |
94 | 93 | ancld 556 |
. . . . . . . . . . 11
 

 
Poly       deg  deg     Poly           deg    
   deg      Poly       deg  deg  
  Poly      
    deg    
   deg     Poly       deg  deg     Poly      
    deg    
   deg        |
95 | | dgrcl 23180 |
. . . . . . . . . . . . . . . . . . . . . 22
 Poly 
deg    |
96 | 95 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . 21
    Poly  
deg    |
97 | 96 | nn0zd 11035 |
. . . . . . . . . . . . . . . . . . . 20
    Poly  
deg    |
98 | 5 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . . . . . 22
    Poly  
Poly    |
99 | 98, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
    Poly  
deg    |
100 | 99 | nn0zd 11035 |
. . . . . . . . . . . . . . . . . . . 20
    Poly  
deg    |
101 | 97, 100 | zsubcld 11042 |
. . . . . . . . . . . . . . . . . . 19
    Poly  
 deg  deg     |
102 | | nn0z 10957 |
. . . . . . . . . . . . . . . . . . . 20

  |
103 | 102 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . 19
    Poly  
  |
104 | | zleltp1 10984 |
. . . . . . . . . . . . . . . . . . 19
   deg  deg      deg  deg    deg  deg        |
105 | 101, 103,
104 | syl2anc 666 |
. . . . . . . . . . . . . . . . . 18
    Poly  
  deg  deg  
 deg  deg        |
106 | 101 | zred 11037 |
. . . . . . . . . . . . . . . . . . 19
    Poly  
 deg  deg     |
107 | | nn0re 10875 |
. . . . . . . . . . . . . . . . . . . 20

  |
108 | 107 | ad2antlr 732 |
. . . . . . . . . . . . . . . . . . 19
    Poly  
  |
109 | 106, 108 | leloed 9775 |
. . . . . . . . . . . . . . . . . 18
    Poly  
  deg  deg  
  deg  deg  
 deg  deg       |
110 | 105, 109 | bitr3d 259 |
. . . . . . . . . . . . . . . . 17
    Poly  
  deg  deg  
 
  deg  deg  
 deg  deg       |
111 | 110 | orbi2d 707 |
. . . . . . . . . . . . . . . 16
    Poly  
    deg  deg     
    deg  deg    deg  deg        |
112 | | pm5.63 934 |
. . . . . . . . . . . . . . . . . . . 20
    deg  deg   
     deg  deg       |
113 | | df-ne 2623 |
. . . . . . . . . . . . . . . . . . . . . 22
 
   |
114 | 113 | anbi1i 700 |
. . . . . . . . . . . . . . . . . . . . 21
    deg  deg   

  deg  deg      |
115 | 114 | orbi2i 522 |
. . . . . . . . . . . . . . . . . . . 20
      deg  deg       
  deg  deg       |
116 | 112, 115 | bitr4i 256 |
. . . . . . . . . . . . . . . . . . 19
    deg  deg   
     deg  deg       |
117 | 116 | orbi2i 522 |
. . . . . . . . . . . . . . . . . 18
   deg  deg      deg  deg    
  deg  deg  
     deg  deg        |
118 | | or12 526 |
. . . . . . . . . . . . . . . . . 18
     deg  deg    deg  deg       deg  deg      deg  deg       |
119 | | or12 526 |
. . . . . . . . . . . . . . . . . 18
     deg  deg      deg  deg        deg  deg        deg  deg        |
120 | 117, 118,
119 | 3bitr4i 281 |
. . . . . . . . . . . . . . . . 17
     deg  deg    deg  deg         deg  deg      deg  deg        |
121 | | orass 527 |
. . . . . . . . . . . . . . . . 17
     deg  deg       deg  deg    
    deg  deg      deg  deg        |
122 | 120, 121 | bitr4i 256 |
. . . . . . . . . . . . . . . 16
     deg  deg    deg  deg         deg  deg       deg  deg       |
123 | 111, 122 | syl6bb 265 |
. . . . . . . . . . . . . . 15
    Poly  
    deg  deg     
    deg  deg       deg  deg        |
124 | 123 | imbi1d 319 |
. . . . . . . . . . . . . 14
    Poly  
     deg  deg      
Poly      
    deg    
   deg         deg  deg       deg  deg     
Poly      
    deg    
   deg       |
125 | | jaob 791 |
. . . . . . . . . . . . . 14
      deg  deg  
    deg  deg     
Poly      
    deg    
   deg         deg  deg     Poly           deg    
   deg        deg  deg     Poly      
    deg    
   deg       |
126 | 124, 125 | syl6bb 265 |
. . . . . . . . . . . . 13
    Poly  
     deg  deg      
Poly      
    deg    
   deg         deg  deg     Poly           deg    
   deg        deg  deg     Poly      
    deg    
   deg        |
127 | 126 | ralbidva 2823 |
. . . . . . . . . . . 12
 

 
Poly       deg  deg       Poly           deg    
   deg    
Poly        deg  deg    
Poly      
    deg    
   deg        deg  deg     Poly      
    deg    
   deg        |
128 | | r19.26 2916 |
. . . . . . . . . . . 12
 
Poly        deg  deg     Poly           deg    
   deg        deg  deg     Poly      
    deg    
   deg       Poly       deg  deg  
  Poly      
    deg    
   deg     Poly       deg  deg     Poly      
    deg    
   deg       |
129 | 127, 128 | syl6bb 265 |
. . . . . . . . . . 11
 

 
Poly       deg  deg       Poly           deg    
   deg      Poly       deg  deg  
  Poly      
    deg    
   deg     Poly       deg  deg     Poly      
    deg    
   deg        |
130 | 94, 129 | sylibrd 238 |
. . . . . . . . . 10
 

 
Poly       deg  deg     Poly           deg    
   deg     Poly       deg  deg       Poly           deg    
   deg       |
131 | 130 | expcom 437 |
. . . . . . . . 9

   Poly       deg  deg  
  Poly      
    deg    
   deg     Poly       deg  deg       Poly           deg    
   deg        |
132 | 131 | a2d 29 |
. . . . . . . 8

   Poly       deg  deg     Poly           deg    
   deg    
  Poly       deg  deg       Poly           deg    
   deg        |
133 | 19, 24, 29, 24, 46, 132 | nn0ind 11027 |
. . . . . . 7

  Poly       deg  deg     Poly           deg    
   deg       |
134 | 14, 133 | syl 17 |
. . . . . 6
   Poly       deg  deg     Poly           deg    
   deg       |
135 | 134 | impcom 432 |
. . . . 5
 

 Poly       deg  deg  
  Poly      
    deg    
   deg      |
136 | | eqeq1 2454 |
. . . . . . . 8
       |
137 | | fveq2 5863 |
. . . . . . . . . 10
 deg  deg    |
138 | 137 | oveq1d 6303 |
. . . . . . . . 9
  deg  deg    deg  deg     |
139 | 138 | breq1d 4411 |
. . . . . . . 8
   deg  deg    deg  deg      |
140 | 136, 139 | orbi12d 715 |
. . . . . . 7
     deg  deg   
   deg  deg       |
141 | | oveq1 6295 |
. . . . . . . . . . 11
   
      
    |
142 | | plydiv.r |
. . . . . . . . . . 11
   
   |
143 | 141, 142 | syl6eqr 2502 |
. . . . . . . . . 10
   
     |
144 | 143 | eqeq1d 2452 |
. . . . . . . . 9
     
       |
145 | 143 | fveq2d 5867 |
. . . . . . . . . 10
 deg    
   deg    |
146 | 145 | breq1d 4411 |
. . . . . . . . 9
  deg  
     deg  deg  deg     |
147 | 144, 146 | orbi12d 715 |
. . . . . . . 8
          deg    
   deg  
  deg  deg      |
148 | 147 | rexbidv 2900 |
. . . . . . 7
  
Poly      
    deg    
   deg  
 Poly     deg  deg      |
149 | 140, 148 | imbi12d 322 |
. . . . . 6
      deg  deg  
  Poly      
    deg    
   deg        deg  deg  
  Poly     deg  deg       |
150 | 149 | rspcv 3145 |
. . . . 5
 Poly 
 
Poly       deg  deg     Poly           deg    
   deg        deg  deg     Poly     deg  deg       |
151 | 13, 135, 150 | sylc 62 |
. . . 4
 

    deg  deg     Poly     deg  deg      |
152 | 12, 151 | syl5 33 |
. . 3
 

  deg  deg  
 Poly     deg  deg      |
153 | 152 | rexlimdva 2878 |
. 2
    deg  deg  
 Poly     deg  deg      |
154 | 11, 153 | mpd 15 |
1
  Poly     deg  deg     |