Step | Hyp | Ref
| Expression |
1 | | plyssc 23154 |
. . 3
Poly  Poly   |
2 | | dgrco.3 |
. . 3
 Poly    |
3 | 1, 2 | sseldi 3430 |
. 2
 Poly    |
4 | | dgrco.1 |
. . . 4
deg   |
5 | | dgrcl 23187 |
. . . . 5
 Poly 
deg    |
6 | 2, 5 | syl 17 |
. . . 4
 deg    |
7 | 4, 6 | syl5eqel 2533 |
. . 3
   |
8 | | breq2 4406 |
. . . . . . 7
  deg  deg     |
9 | 8 | imbi1d 319 |
. . . . . 6
   deg 
deg     deg     deg  deg     deg       |
10 | 9 | ralbidv 2827 |
. . . . 5
  
Poly    deg  deg     deg   
 Poly    deg 
deg     deg       |
11 | 10 | imbi2d 318 |
. . . 4
  
 Poly    deg 
deg     deg    
  Poly    deg 
deg     deg        |
12 | | breq2 4406 |
. . . . . . 7
  deg  deg     |
13 | 12 | imbi1d 319 |
. . . . . 6
   deg 
deg     deg     deg  deg     deg       |
14 | 13 | ralbidv 2827 |
. . . . 5
  
Poly    deg  deg     deg   
 Poly    deg 
deg     deg       |
15 | 14 | imbi2d 318 |
. . . 4
  
 Poly    deg 
deg     deg    
  Poly    deg 
deg     deg        |
16 | | breq2 4406 |
. . . . . . 7
    deg  deg       |
17 | 16 | imbi1d 319 |
. . . . . 6
     deg 
deg     deg     deg    deg     deg       |
18 | 17 | ralbidv 2827 |
. . . . 5
    
Poly    deg  deg     deg   
 Poly    deg 
  deg     deg       |
19 | 18 | imbi2d 318 |
. . . 4
    
 Poly    deg 
deg     deg    
  Poly    deg   
deg     deg        |
20 | | breq2 4406 |
. . . . . . 7
  deg  deg     |
21 | 20 | imbi1d 319 |
. . . . . 6
   deg 
deg     deg     deg  deg     deg       |
22 | 21 | ralbidv 2827 |
. . . . 5
  
Poly    deg  deg     deg   
 Poly    deg 
deg     deg       |
23 | 22 | imbi2d 318 |
. . . 4
  
 Poly    deg 
deg     deg    
  Poly    deg  deg     deg        |
24 | | dgrco.2 |
. . . . . . . . . . . 12
deg   |
25 | | dgrco.4 |
. . . . . . . . . . . . 13
 Poly    |
26 | | dgrcl 23187 |
. . . . . . . . . . . . 13
 Poly 
deg    |
27 | 25, 26 | syl 17 |
. . . . . . . . . . . 12
 deg    |
28 | 24, 27 | syl5eqel 2533 |
. . . . . . . . . . 11
   |
29 | 28 | nn0cnd 10927 |
. . . . . . . . . 10
   |
30 | 29 | adantr 467 |
. . . . . . . . 9
 
 Poly  deg   
  |
31 | 30 | mul02d 9831 |
. . . . . . . 8
 
 Poly  deg        |
32 | | simprr 766 |
. . . . . . . . . 10
 
 Poly  deg    deg    |
33 | | dgrcl 23187 |
. . . . . . . . . . . 12
 Poly  deg    |
34 | 33 | ad2antrl 734 |
. . . . . . . . . . 11
 
 Poly  deg    deg    |
35 | 34 | nn0ge0d 10928 |
. . . . . . . . . 10
 
 Poly  deg   
deg    |
36 | 34 | nn0red 10926 |
. . . . . . . . . . 11
 
 Poly  deg    deg    |
37 | | 0re 9643 |
. . . . . . . . . . 11
 |
38 | | letri3 9719 |
. . . . . . . . . . 11
  deg    deg 
 deg 
deg      |
39 | 36, 37, 38 | sylancl 668 |
. . . . . . . . . 10
 
 Poly  deg     deg   deg  deg      |
40 | 32, 35, 39 | mpbir2and 933 |
. . . . . . . . 9
 
 Poly  deg    deg    |
41 | 40 | oveq1d 6305 |
. . . . . . . 8
 
 Poly  deg     deg       |
42 | 31, 41, 40 | 3eqtr4d 2495 |
. . . . . . 7
 
 Poly  deg     deg   deg    |
43 | | fconstmpt 4878 |
. . . . . . . . 9
               |
44 | | 0dgrb 23200 |
. . . . . . . . . . 11
 Poly   deg             |
45 | 44 | ad2antrl 734 |
. . . . . . . . . 10
 
 Poly  deg     deg             |
46 | 40, 45 | mpbid 214 |
. . . . . . . . 9
 
 Poly  deg              |
47 | 25 | adantr 467 |
. . . . . . . . . . . 12
 
 Poly  deg   
Poly    |
48 | | plyf 23152 |
. . . . . . . . . . . 12
 Poly 
      |
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
 
 Poly  deg          |
50 | 49 | ffvelrnda 6022 |
. . . . . . . . . 10
    Poly 
deg           |
51 | 49 | feqmptd 5918 |
. . . . . . . . . 10
 
 Poly  deg   
        |
52 | | fconstmpt 4878 |
. . . . . . . . . . 11
               |
53 | 46, 52 | syl6eq 2501 |
. . . . . . . . . 10
 
 Poly  deg            |
54 | | eqidd 2452 |
. . . . . . . . . 10
               |
55 | 50, 51, 53, 54 | fmptco 6056 |
. . . . . . . . 9
 
 Poly  deg              |
56 | 43, 46, 55 | 3eqtr4a 2511 |
. . . . . . . 8
 
 Poly  deg        |
57 | 56 | fveq2d 5869 |
. . . . . . 7
 
 Poly  deg    deg  deg      |
58 | 42, 57 | eqtr2d 2486 |
. . . . . 6
 
 Poly  deg    deg     deg     |
59 | 58 | expr 620 |
. . . . 5
 
Poly    deg  deg     deg      |
60 | 59 | ralrimiva 2802 |
. . . 4
  Poly    deg 
deg     deg      |
61 | | fveq2 5865 |
. . . . . . . . . 10
 deg  deg    |
62 | 61 | breq1d 4412 |
. . . . . . . . 9
  deg  deg     |
63 | | coeq1 4992 |
. . . . . . . . . . 11
       |
64 | 63 | fveq2d 5869 |
. . . . . . . . . 10
 deg    deg      |
65 | 61 | oveq1d 6305 |
. . . . . . . . . 10
  deg    deg     |
66 | 64, 65 | eqeq12d 2466 |
. . . . . . . . 9
  deg     deg   deg     deg      |
67 | 62, 66 | imbi12d 322 |
. . . . . . . 8
   deg 
deg     deg     deg  deg     deg       |
68 | 67 | cbvralv 3019 |
. . . . . . 7
 
Poly    deg  deg     deg     Poly    deg 
deg     deg      |
69 | 33 | ad2antrl 734 |
. . . . . . . . . . . 12
     Poly 
 Poly    deg 
deg     deg      deg    |
70 | 69 | nn0red 10926 |
. . . . . . . . . . 11
     Poly 
 Poly    deg 
deg     deg      deg    |
71 | | nn0p1nn 10909 |
. . . . . . . . . . . . 13

    |
72 | 71 | ad2antlr 733 |
. . . . . . . . . . . 12
     Poly 
 Poly    deg 
deg     deg          |
73 | 72 | nnred 10624 |
. . . . . . . . . . 11
     Poly 
 Poly    deg 
deg     deg          |
74 | 70, 73 | leloed 9778 |
. . . . . . . . . 10
     Poly 
 Poly    deg 
deg     deg       deg 
 
 deg    deg        |
75 | | simplr 762 |
. . . . . . . . . . . . 13
     Poly 
 Poly    deg 
deg     deg        |
76 | | nn0leltp1 10995 |
. . . . . . . . . . . . 13
  deg    deg  deg       |
77 | 69, 75, 76 | syl2anc 667 |
. . . . . . . . . . . 12
     Poly 
 Poly    deg 
deg     deg       deg 
deg 
     |
78 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
 deg  deg    |
79 | 78 | breq1d 4412 |
. . . . . . . . . . . . . . 15
  deg  deg     |
80 | | coeq1 4992 |
. . . . . . . . . . . . . . . . 17
       |
81 | 80 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
 deg    deg      |
82 | 78 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
  deg    deg     |
83 | 81, 82 | eqeq12d 2466 |
. . . . . . . . . . . . . . 15
  deg     deg   deg     deg      |
84 | 79, 83 | imbi12d 322 |
. . . . . . . . . . . . . 14
   deg 
deg     deg     deg  deg     deg       |
85 | 84 | rspcva 3148 |
. . . . . . . . . . . . 13
  Poly 
 Poly    deg 
deg     deg      deg 
deg     deg      |
86 | 85 | adantl 468 |
. . . . . . . . . . . 12
     Poly 
 Poly    deg 
deg     deg       deg 
deg     deg      |
87 | 77, 86 | sylbird 239 |
. . . . . . . . . . 11
     Poly 
 Poly    deg 
deg     deg       deg 
  deg     deg      |
88 | | eqid 2451 |
. . . . . . . . . . . . 13
deg  deg   |
89 | | simprll 772 |
. . . . . . . . . . . . 13
      Poly  
Poly    deg  deg     deg     deg      Poly    |
90 | 1, 25 | sseldi 3430 |
. . . . . . . . . . . . . 14
 Poly    |
91 | 90 | ad2antrr 732 |
. . . . . . . . . . . . 13
      Poly  
Poly    deg  deg     deg     deg      Poly    |
92 | | eqid 2451 |
. . . . . . . . . . . . 13
coeff  coeff   |
93 | | simplr 762 |
. . . . . . . . . . . . 13
      Poly  
Poly    deg  deg     deg     deg        |
94 | | simprr 766 |
. . . . . . . . . . . . 13
      Poly  
Poly    deg  deg     deg     deg      deg      |
95 | | simprlr 773 |
. . . . . . . . . . . . . 14
      Poly  
Poly    deg  deg     deg     deg       Poly    deg 
deg     deg      |
96 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
 deg  deg    |
97 | 96 | breq1d 4412 |
. . . . . . . . . . . . . . . 16
  deg  deg     |
98 | | coeq1 4992 |
. . . . . . . . . . . . . . . . . 18
       |
99 | 98 | fveq2d 5869 |
. . . . . . . . . . . . . . . . 17
 deg    deg      |
100 | 96 | oveq1d 6305 |
. . . . . . . . . . . . . . . . 17
  deg    deg     |
101 | 99, 100 | eqeq12d 2466 |
. . . . . . . . . . . . . . . 16
  deg     deg   deg     deg      |
102 | 97, 101 | imbi12d 322 |
. . . . . . . . . . . . . . 15
   deg 
deg     deg     deg  deg     deg       |
103 | 102 | cbvralv 3019 |
. . . . . . . . . . . . . 14
 
Poly    deg  deg     deg     Poly    deg 
deg     deg      |
104 | 95, 103 | sylib 200 |
. . . . . . . . . . . . 13
      Poly  
Poly    deg  deg     deg     deg       Poly    deg 
deg     deg      |
105 | 88, 24, 89, 91, 92, 93, 94, 104 | dgrcolem2 23228 |
. . . . . . . . . . . 12
      Poly  
Poly    deg  deg     deg     deg      deg     deg     |
106 | 105 | expr 620 |
. . . . . . . . . . 11
     Poly 
 Poly    deg 
deg     deg       deg    deg     deg      |
107 | 87, 106 | jaod 382 |
. . . . . . . . . 10
     Poly 
 Poly    deg 
deg     deg        deg    deg     deg     deg      |
108 | 74, 107 | sylbid 219 |
. . . . . . . . 9
     Poly 
 Poly    deg 
deg     deg       deg 
  deg     deg      |
109 | 108 | expr 620 |
. . . . . . . 8
    Poly  
 
Poly    deg  deg     deg   
 deg    deg     deg       |
110 | 109 | ralrimdva 2806 |
. . . . . . 7
 

 
Poly    deg  deg     deg   
 Poly    deg 
  deg     deg       |
111 | 68, 110 | syl5bi 221 |
. . . . . 6
 

 
Poly    deg  deg     deg   
 Poly    deg 
  deg     deg       |
112 | 111 | expcom 437 |
. . . . 5

   Poly    deg 
deg     deg   
 Poly    deg 
  deg     deg        |
113 | 112 | a2d 29 |
. . . 4

   Poly    deg 
deg     deg       Poly    deg    deg     deg        |
114 | 11, 15, 19, 23, 60, 113 | nn0ind 11030 |
. . 3

  Poly    deg  deg     deg       |
115 | 7, 114 | mpcom 37 |
. 2
  Poly    deg  deg     deg      |
116 | 7 | nn0red 10926 |
. . 3
   |
117 | 116 | leidd 10180 |
. 2

  |
118 | | fveq2 5865 |
. . . . . 6
 deg  deg    |
119 | 118, 4 | syl6eqr 2503 |
. . . . 5
 deg    |
120 | 119 | breq1d 4412 |
. . . 4
  deg 
   |
121 | | coeq1 4992 |
. . . . . 6
       |
122 | 121 | fveq2d 5869 |
. . . . 5
 deg    deg      |
123 | 119 | oveq1d 6305 |
. . . . 5
  deg       |
124 | 122, 123 | eqeq12d 2466 |
. . . 4
  deg     deg   deg         |
125 | 120, 124 | imbi12d 322 |
. . 3
   deg 
deg     deg     deg 
        |
126 | 125 | rspcv 3146 |
. 2
 Poly    Poly    deg 
deg     deg   

deg 
        |
127 | 3, 115, 117, 126 | syl3c 63 |
1
 deg        |