Step | Hyp | Ref
| Expression |
1 | | dgrcolem1.2 |
. 2
   |
2 | | oveq2 6316 |
. . . . . . 7
                   |
3 | 2 | mpteq2dv 4483 |
. . . . . 6
                       |
4 | 3 | fveq2d 5883 |
. . . . 5
 deg            deg              |
5 | | oveq1 6315 |
. . . . 5
       |
6 | 4, 5 | eqeq12d 2486 |
. . . 4
  deg             
deg                 |
7 | 6 | imbi2d 323 |
. . 3
  
deg 
            
 deg                  |
8 | | oveq2 6316 |
. . . . . . 7
                   |
9 | 8 | mpteq2dv 4483 |
. . . . . 6
                       |
10 | 9 | fveq2d 5883 |
. . . . 5
 deg            deg              |
11 | | oveq1 6315 |
. . . . 5
       |
12 | 10, 11 | eqeq12d 2486 |
. . . 4
  deg             
deg                 |
13 | 12 | imbi2d 323 |
. . 3
  
deg 
            
 deg                  |
14 | | oveq2 6316 |
. . . . . . 7
                       |
15 | 14 | mpteq2dv 4483 |
. . . . . 6
                           |
16 | 15 | fveq2d 5883 |
. . . . 5
   deg            deg                |
17 | | oveq1 6315 |
. . . . 5
           |
18 | 16, 17 | eqeq12d 2486 |
. . . 4
    deg             
deg                     |
19 | 18 | imbi2d 323 |
. . 3
    
deg 
            
 deg                      |
20 | | oveq2 6316 |
. . . . . . 7
                   |
21 | 20 | mpteq2dv 4483 |
. . . . . 6
                       |
22 | 21 | fveq2d 5883 |
. . . . 5
 deg            deg              |
23 | | oveq1 6315 |
. . . . 5
       |
24 | 22, 23 | eqeq12d 2486 |
. . . 4
  deg             
deg                 |
25 | 24 | imbi2d 323 |
. . 3
  
deg 
            
 deg                  |
26 | | dgrcolem1.4 |
. . . . . . . . . . 11
 Poly    |
27 | | plyf 23231 |
. . . . . . . . . . 11
 Poly 
      |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
       |
29 | 28 | ffvelrnda 6037 |
. . . . . . . . 9
 

      |
30 | 29 | exp1d 12449 |
. . . . . . . 8
 

              |
31 | 30 | mpteq2dva 4482 |
. . . . . . 7
                   |
32 | 28 | feqmptd 5932 |
. . . . . . 7
         |
33 | 31, 32 | eqtr4d 2508 |
. . . . . 6
             |
34 | 33 | fveq2d 5883 |
. . . . 5
 deg            deg    |
35 | | dgrcolem1.1 |
. . . . 5
deg   |
36 | 34, 35 | syl6eqr 2523 |
. . . 4
 deg              |
37 | | dgrcolem1.3 |
. . . . . 6
   |
38 | 37 | nncnd 10647 |
. . . . 5
   |
39 | 38 | mulid2d 9679 |
. . . 4
     |
40 | 36, 39 | eqtr4d 2508 |
. . 3
 deg                |
41 | 29 | adantlr 729 |
. . . . . . . . . . . 12
           |
42 | | nnnn0 10900 |
. . . . . . . . . . . . . 14
   |
43 | 42 | adantl 473 |
. . . . . . . . . . . . 13
 

  |
44 | 43 | adantr 472 |
. . . . . . . . . . . 12
       |
45 | 41, 44 | expp1d 12455 |
. . . . . . . . . . 11
                               |
46 | 45 | mpteq2dva 4482 |
. . . . . . . . . 10
 

                              |
47 | | cnex 9638 |
. . . . . . . . . . . 12
 |
48 | 47 | a1i 11 |
. . . . . . . . . . 11
 

  |
49 | | ovex 6336 |
. . . . . . . . . . . 12
         |
50 | 49 | a1i 11 |
. . . . . . . . . . 11
               |
51 | | eqidd 2472 |
. . . . . . . . . . 11
 

                      |
52 | 32 | adantr 472 |
. . . . . . . . . . 11
 

        |
53 | 48, 50, 41, 51, 52 | offval2 6567 |
. . . . . . . . . 10
 

                               |
54 | 46, 53 | eqtr4d 2508 |
. . . . . . . . 9
 

                           |
55 | 54 | fveq2d 5883 |
. . . . . . . 8
 

deg 
            deg                 |
56 | 55 | adantr 472 |
. . . . . . 7
    deg               deg              deg                 |
57 | | nncn 10639 |
. . . . . . . . . . . 12
   |
58 | 57 | adantl 473 |
. . . . . . . . . . 11
 

  |
59 | | 1cnd 9677 |
. . . . . . . . . . 11
 

  |
60 | 38 | adantr 472 |
. . . . . . . . . . 11
 

  |
61 | 58, 59, 60 | adddird 9686 |
. . . . . . . . . 10
 

            |
62 | 60 | mulid2d 9679 |
. . . . . . . . . . 11
 

    |
63 | 62 | oveq2d 6324 |
. . . . . . . . . 10
 

            |
64 | 61, 63 | eqtrd 2505 |
. . . . . . . . 9
 

          |
65 | 64 | adantr 472 |
. . . . . . . 8
    deg                         |
66 | | eqidd 2472 |
. . . . . . . . . . . . 13
 

              |
67 | | oveq1 6315 |
. . . . . . . . . . . . 13
                   |
68 | 41, 52, 66, 67 | fmptco 6072 |
. . . . . . . . . . . 12
 

                    |
69 | | ssid 3437 |
. . . . . . . . . . . . . . 15
 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . 14
 

  |
71 | | plypow 23238 |
. . . . . . . . . . . . . 14
 
       Poly    |
72 | 70, 59, 43, 71 | syl3anc 1292 |
. . . . . . . . . . . . 13
 

      Poly    |
73 | | plyssc 23233 |
. . . . . . . . . . . . . 14
Poly  Poly   |
74 | 26 | adantr 472 |
. . . . . . . . . . . . . 14
 

Poly    |
75 | 73, 74 | sseldi 3416 |
. . . . . . . . . . . . 13
 

Poly    |
76 | | addcl 9639 |
. . . . . . . . . . . . . 14
 
     |
77 | 76 | adantl 473 |
. . . . . . . . . . . . 13
    
 
    |
78 | | mulcl 9641 |
. . . . . . . . . . . . . 14
 
     |
79 | 78 | adantl 473 |
. . . . . . . . . . . . 13
    
 
    |
80 | 72, 75, 77, 79 | plyco 23274 |
. . . . . . . . . . . 12
 

        Poly    |
81 | 68, 80 | eqeltrrd 2550 |
. . . . . . . . . . 11
 

          Poly    |
82 | 81 | adantr 472 |
. . . . . . . . . 10
    deg                         Poly    |
83 | | simpr 468 |
. . . . . . . . . . . 12
    deg               deg                |
84 | | simpr 468 |
. . . . . . . . . . . . . . 15
 

  |
85 | 37 | adantr 472 |
. . . . . . . . . . . . . . 15
 

  |
86 | 84, 85 | nnmulcld 10679 |
. . . . . . . . . . . . . 14
 

    |
87 | 86 | nnne0d 10676 |
. . . . . . . . . . . . 13
 

    |
88 | 87 | adantr 472 |
. . . . . . . . . . . 12
    deg                   |
89 | 83, 88 | eqnetrd 2710 |
. . . . . . . . . . 11
    deg               deg              |
90 | | fveq2 5879 |
. . . . . . . . . . . . 13
            deg            deg     |
91 | | dgr0 23295 |
. . . . . . . . . . . . 13
deg    |
92 | 90, 91 | syl6eq 2521 |
. . . . . . . . . . . 12
            deg              |
93 | 92 | necon3i 2675 |
. . . . . . . . . . 11
 deg                         |
94 | 89, 93 | syl 17 |
. . . . . . . . . 10
    deg                            |
95 | 75 | adantr 472 |
. . . . . . . . . 10
    deg               Poly    |
96 | 37 | nnne0d 10676 |
. . . . . . . . . . . . 13
   |
97 | | fveq2 5879 |
. . . . . . . . . . . . . . . 16
  deg  deg     |
98 | 97, 91 | syl6eq 2521 |
. . . . . . . . . . . . . . 15
  deg    |
99 | 35, 98 | syl5eq 2517 |
. . . . . . . . . . . . . 14
 
  |
100 | 99 | necon3i 2675 |
. . . . . . . . . . . . 13
    |
101 | 96, 100 | syl 17 |
. . . . . . . . . . . 12
    |
102 | 101 | adantr 472 |
. . . . . . . . . . 11
 

   |
103 | 102 | adantr 472 |
. . . . . . . . . 10
    deg                  |
104 | | eqid 2471 |
. . . . . . . . . . 11
deg 
          deg             |
105 | 104, 35 | dgrmul 23303 |
. . . . . . . . . 10
             Poly              
Poly     deg                deg               |
106 | 82, 94, 95, 103, 105 | syl22anc 1293 |
. . . . . . . . 9
    deg               deg                deg               |
107 | | oveq1 6315 |
. . . . . . . . . 10
 deg               deg                   |
108 | 107 | adantl 473 |
. . . . . . . . 9
    deg                deg                   |
109 | 106, 108 | eqtrd 2505 |
. . . . . . . 8
    deg               deg                     |
110 | 65, 109 | eqtr4d 2508 |
. . . . . . 7
    deg                   deg                 |
111 | 56, 110 | eqtr4d 2508 |
. . . . . 6
    deg               deg                    |
112 | 111 | ex 441 |
. . . . 5
 

 deg              deg                     |
113 | 112 | expcom 442 |
. . . 4
   deg 
           
deg                      |
114 | 113 | a2d 28 |
. . 3
  
deg 
              deg                      |
115 | 7, 13, 19, 25, 40, 114 | nnind 10649 |
. 2
  deg                 |
116 | 1, 115 | mpcom 36 |
1
 deg                |