Step | Hyp | Ref
| Expression |
1 | | 1rp 11296 |
. . . . . . 7
 |
2 | | snssi 4085 |
. . . . . . 7

 
  |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
 
 |
4 | | ssrab2 3482 |
. . . . . 6


              
 |
5 | 3, 4 | unssi 3577 |
. . . . 5
    
                 |
6 | | ltso 9701 |
. . . . . . 7
 |
7 | 6 | a1i 11 |
. . . . . 6
   |
8 | | snfi 7637 |
. . . . . . 7
   |
9 | | aalioulem2.b |
. . . . . . . . . . 11
 Poly    |
10 | | aalioulem2.c |
. . . . . . . . . . . . . 14
   |
11 | 10 | nnne0d 10643 |
. . . . . . . . . . . . 13
   |
12 | | aalioulem2.a |
. . . . . . . . . . . . . 14
deg   |
13 | 12 | eqcomi 2461 |
. . . . . . . . . . . . 13
deg   |
14 | | dgr0 23228 |
. . . . . . . . . . . . 13
deg    |
15 | 11, 13, 14 | 3netr4g 2703 |
. . . . . . . . . . . 12
 deg  deg     |
16 | | fveq2 5848 |
. . . . . . . . . . . . 13
  deg  deg     |
17 | 16 | necon3i 2656 |
. . . . . . . . . . . 12
 deg  deg  
   |
18 | 15, 17 | syl 17 |
. . . . . . . . . . 11
    |
19 | | eqid 2452 |
. . . . . . . . . . . 12
               |
20 | 19 | fta1 23273 |
. . . . . . . . . . 11
  Poly 
                    
deg     |
21 | 9, 18, 20 | syl2anc 671 |
. . . . . . . . . 10
                   
deg     |
22 | 21 | simpld 465 |
. . . . . . . . 9
          |
23 | | abrexfi 7861 |
. . . . . . . . 9
         
                 |
24 | 22, 23 | syl 17 |
. . . . . . . 8
  
                 |
25 | | rabssab 3484 |
. . . . . . . 8


              
             
    |
26 | | ssfi 7779 |
. . . . . . . 8
   
                
              
             
                 
     |
27 | 24, 25, 26 | sylancl 673 |
. . . . . . 7
              
     |
28 | | unfi 7825 |
. . . . . . 7
                     
    
                  |
29 | 8, 27, 28 | sylancr 674 |
. . . . . 6
                        |
30 | | 1ex 9625 |
. . . . . . . . 9
 |
31 | 30 | snid 3964 |
. . . . . . . 8
   |
32 | | elun1 3569 |
. . . . . . . 8
       
                  |
33 | | ne0i 3705 |
. . . . . . . 8
    

                    
                  |
34 | 31, 32, 33 | mp2b 10 |
. . . . . . 7
    
                 |
35 | 34 | a1i 11 |
. . . . . 6
                        |
36 | | rpssre 11302 |
. . . . . . . 8
 |
37 | 5, 36 | sstri 3409 |
. . . . . . 7
    
                 |
38 | 37 | a1i 11 |
. . . . . 6
                        |
39 | | fiinfcl 8004 |
. . . . . 6
     

                                         
                  inf     
                      
                  |
40 | 7, 29, 35, 38, 39 | syl13anc 1273 |
. . . . 5
 inf    

                      
                  |
41 | 5, 40 | sseldi 3398 |
. . . 4
 inf    

                    |
42 | 37 | a1i 11 |
. . . . . . . . 9
               
                  |
43 | | 0re 9630 |
. . . . . . . . . . . 12
 |
44 | | rpge0 11304 |
. . . . . . . . . . . . 13

  |
45 | 44 | rgen 2747 |
. . . . . . . . . . . 12
  |
46 | | breq1 4377 |
. . . . . . . . . . . . . 14
 
   |
47 | 46 | ralbidv 2810 |
. . . . . . . . . . . . 13
  
    |
48 | 47 | rspcev 3118 |
. . . . . . . . . . . 12
     
  |
49 | 43, 45, 48 | mp2an 683 |
. . . . . . . . . . 11
 
 |
50 | | ssralv 3461 |
. . . . . . . . . . . . 13
     
                                        
   |
51 | 5, 50 | ax-mp 5 |
. . . . . . . . . . . 12
 
                      
  |
52 | 51 | reximi 2833 |
. . . . . . . . . . 11
  
                       
  |
53 | 49, 52 | ax-mp 5 |
. . . . . . . . . 10
                       
 |
54 | 53 | a1i 11 |
. . . . . . . . 9
                                  
  |
55 | | aalioulem2.d |
. . . . . . . . . . . . . . 15
   |
56 | 55 | ad2antrr 737 |
. . . . . . . . . . . . . 14
             |
57 | | simplr 767 |
. . . . . . . . . . . . . 14
             |
58 | 56, 57 | resubcld 10036 |
. . . . . . . . . . . . 13
           
   |
59 | 58 | recnd 9656 |
. . . . . . . . . . . 12
           
   |
60 | 55 | ad2antrr 737 |
. . . . . . . . . . . . . . . . 17
        
  |
61 | 60 | recnd 9656 |
. . . . . . . . . . . . . . . 16
        
  |
62 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
           |
63 | 62 | recnd 9656 |
. . . . . . . . . . . . . . . 16
           |
64 | 61, 63 | subeq0ad 9983 |
. . . . . . . . . . . . . . 15
               |
65 | 64 | necon3abid 2660 |
. . . . . . . . . . . . . 14
               |
66 | 65 | biimprd 231 |
. . . . . . . . . . . . 13
         
     |
67 | 66 | impr 629 |
. . . . . . . . . . . 12
           
   |
68 | 59, 67 | absrpcld 13521 |
. . . . . . . . . . 11
                   |
69 | 57 | recnd 9656 |
. . . . . . . . . . . . 13
             |
70 | | simprl 769 |
. . . . . . . . . . . . 13
                 |
71 | | plyf 23164 |
. . . . . . . . . . . . . . . . 17
 Poly        |
72 | 9, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
       |
73 | | ffn 5711 |
. . . . . . . . . . . . . . . 16
       |
74 | 72, 73 | syl 17 |
. . . . . . . . . . . . . . 15
   |
75 | 74 | ad2antrr 737 |
. . . . . . . . . . . . . 14
             |
76 | | fniniseg 5987 |
. . . . . . . . . . . . . 14
        
         |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
                  
         |
78 | 69, 70, 77 | mpbir2and 933 |
. . . . . . . . . . . 12
                    |
79 | | eqid 2452 |
. . . . . . . . . . . 12
             |
80 | | oveq2 6284 |
. . . . . . . . . . . . . . 15
 
     |
81 | 80 | fveq2d 5852 |
. . . . . . . . . . . . . 14
          
    |
82 | 81 | eqeq2d 2462 |
. . . . . . . . . . . . 13
     
       
               |
83 | 82 | rspcev 3118 |
. . . . . . . . . . . 12
                  
               
          |
84 | 78, 79, 83 | sylancl 673 |
. . . . . . . . . . 11
                       
          |
85 | | eqeq1 2456 |
. . . . . . . . . . . . 13
    
 
    
     
           |
86 | 85 | rexbidv 2873 |
. . . . . . . . . . . 12
    
 
 
              
                       |
87 | 86 | elrab 3164 |
. . . . . . . . . . 11
                       
                   
           |
88 | 68, 84, 87 | sylanbrc 675 |
. . . . . . . . . 10
                              
     |
89 | | elun2 3570 |
. . . . . . . . . 10
                                 

                  |
90 | 88, 89 | syl 17 |
. . . . . . . . 9
                                        |
91 | | infrelb 10585 |
. . . . . . . . 9
                      
                       
         

                 inf    

                          |
92 | 42, 54, 90, 91 | syl3anc 1271 |
. . . . . . . 8
           inf     
                          |
93 | 92 | expr 624 |
. . . . . . 7
         
inf     
                           |
94 | 93 | orrd 384 |
. . . . . 6
          inf     
                           |
95 | 94 | ex 440 |
. . . . 5
 

     
inf    

                            |
96 | 95 | ralrimiva 2790 |
. . . 4
        inf     
                            |
97 | | breq1 4377 |
. . . . . . . 8
 inf     
                  
     
inf     
                           |
98 | 97 | orbi2d 713 |
. . . . . . 7
 inf     
                            inf     
                            |
99 | 98 | imbi2d 322 |
. . . . . 6
 inf     
                            
   
     
inf    

                             |
100 | 99 | ralbidv 2810 |
. . . . 5
 inf     
                   
         
   
     

inf     
                             |
101 | 100 | rspcev 3118 |
. . . 4
 inf    

                         inf     
                                 

   
      |
102 | 41, 96, 101 | syl2anc 671 |
. . 3
                   |
103 | | znq 11258 |
. . . . . . . 8
 
     |
104 | | qre 11259 |
. . . . . . . 8
       |
105 | 103, 104 | syl 17 |
. . . . . . 7
 
     |
106 | | fveq2 5848 |
. . . . . . . . . 10
          
    |
107 | 106 | eqeq1d 2454 |
. . . . . . . . 9
                 |
108 | | eqeq2 2463 |
. . . . . . . . . 10
   

    |
109 | | oveq2 6284 |
. . . . . . . . . . . 12
   
  
    |
110 | 109 | fveq2d 5852 |
. . . . . . . . . . 11
            
      |
111 | 110 | breq2d 4386 |
. . . . . . . . . 10
   
     
           |
112 | 108, 111 | orbi12d 721 |
. . . . . . . . 9
                   
       |
113 | 107, 112 | imbi12d 326 |
. . . . . . . 8
             
   
       
 
             |
114 | 113 | rspcv 3114 |
. . . . . . 7
    
         
        
        
         |
115 | 105, 114 | syl 17 |
. . . . . 6
 
       

   
        
        
         |
116 | 115 | com12 32 |
. . . . 5
 
             
 
     
        
         |
117 | 116 | ralrimivv 2794 |
. . . 4
 
             
        
      
        |
118 | 117 | reximi 2833 |
. . 3
       

   
    
        
      
        |
119 | 102, 118 | syl 17 |
. 2
   
              
       |
120 | | simplr 767 |
. . . . . . . . . . 11
    
 
  |
121 | | simprr 771 |
. . . . . . . . . . . . 13
    
 
  |
122 | 10 | nnnn0d 10915 |
. . . . . . . . . . . . . 14
   |
123 | 122 | ad2antrr 737 |
. . . . . . . . . . . . 13
    
 
  |
124 | 121, 123 | nnexpcld 12431 |
. . . . . . . . . . . 12
    
 
      |
125 | 124 | nnrpd 11329 |
. . . . . . . . . . 11
    
 
      |
126 | 120, 125 | rpdivcld 11348 |
. . . . . . . . . 10
    
 
        |
127 | 126 | rpred 11331 |
. . . . . . . . 9
    
 
        |
128 | 127 | adantr 471 |
. . . . . . . 8
   
 
     
             |
129 | | simpllr 774 |
. . . . . . . . 9
   
 
     
       |
130 | 129 | rpred 11331 |
. . . . . . . 8
   
 
     
       |
131 | 55 | ad2antrr 737 |
. . . . . . . . . . . 12
    
 
  |
132 | 105 | adantl 472 |
. . . . . . . . . . . 12
    
 
    |
133 | 131, 132 | resubcld 10036 |
. . . . . . . . . . 11
    
 
      |
134 | 133 | recnd 9656 |
. . . . . . . . . 10
    
 
      |
135 | 134 | abscld 13509 |
. . . . . . . . 9
    
 
          |
136 | 135 | adantr 471 |
. . . . . . . 8
   
 
     
         
     |
137 | | rpre 11298 |
. . . . . . . . . . 11

  |
138 | 137 | ad2antlr 738 |
. . . . . . . . . 10
    
 
  |
139 | 120 | rpcnne0d 11340 |
. . . . . . . . . . . 12
    
 
    |
140 | | divid 10286 |
. . . . . . . . . . . 12
       |
141 | 139, 140 | syl 17 |
. . . . . . . . . . 11
    
 
    |
142 | 124 | nnge1d 10641 |
. . . . . . . . . . 11
    
 
      |
143 | 141, 142 | eqbrtrd 4395 |
. . . . . . . . . 10
    
 
        |
144 | 138, 120,
125, 143 | lediv23d 11394 |
. . . . . . . . 9
    
 
        |
145 | 144 | adantr 471 |
. . . . . . . 8
   
 
     
             |
146 | | simpr 467 |
. . . . . . . 8
   
 
     
        
      |
147 | 128, 130,
136, 145, 146 | letrd 9779 |
. . . . . . 7
   
 
     
              
      |
148 | 147 | ex 440 |
. . . . . 6
    
 
    
   
         
       |
149 | 148 | orim2d 855 |
. . . . 5
    
 
 
 
                      
       |
150 | 149 | imim2d 54 |
. . . 4
    
 
               
    
       
       
             |
151 | 150 | ralimdvva 2788 |
. . 3
 

 
       
      
      
                     
        |
152 | 151 | reximdva 2839 |
. 2
                   
    
         
            
         |
153 | 119, 152 | mpd 15 |
1
   
                    
       |