Step | Hyp | Ref
| Expression |
1 | | nnre 10433 |
. . . . . . . . . . . 12
   |
2 | 1 | ad2antlr 726 |
. . . . . . . . . . 11
                  |
3 | | ltpnf 11206 |
. . . . . . . . . . 11
   |
4 | 2, 3 | syl 16 |
. . . . . . . . . 10
                  |
5 | | iftrue 3898 |
. . . . . . . . . . 11
            
           |
6 | 5 | adantl 466 |
. . . . . . . . . 10
                                   |
7 | | simpr 461 |
. . . . . . . . . 10
                      |
8 | 4, 6, 7 | 3brtr4d 4423 |
. . . . . . . . 9
                                       |
9 | | iffalse 3900 |
. . . . . . . . . . 11
            
                   |
10 | 9 | adantl 466 |
. . . . . . . . . 10
                                           |
11 | | itg2cl 21336 |
. . . . . . . . . . . . . . 15
              |
12 | | xrrebnd 11244 |
. . . . . . . . . . . . . . 15
    
    
   
        |
13 | 11, 12 | syl 16 |
. . . . . . . . . . . . . 14
            
   
        |
14 | | itg2ge0 21339 |
. . . . . . . . . . . . . . . 16
       
      |
15 | | mnflt0 11209 |
. . . . . . . . . . . . . . . . 17
 |
16 | | mnfxr 11198 |
. . . . . . . . . . . . . . . . . . 19
 |
17 | | 0xr 9534 |
. . . . . . . . . . . . . . . . . . 19
 |
18 | | xrltletr 11235 |
. . . . . . . . . . . . . . . . . . 19
           
       |
19 | 16, 17, 18 | mp3an12 1305 |
. . . . . . . . . . . . . . . . . 18
    

            |
20 | 11, 19 | syl 16 |
. . . . . . . . . . . . . . . . 17
             
       |
21 | 15, 20 | mpani 676 |
. . . . . . . . . . . . . . . 16
                    |
22 | 14, 21 | mpd 15 |
. . . . . . . . . . . . . . 15
              |
23 | 22 | biantrurd 508 |
. . . . . . . . . . . . . 14
            
   
        |
24 | | nltpnft 11242 |
. . . . . . . . . . . . . . . 16
    
    
       |
25 | 11, 24 | syl 16 |
. . . . . . . . . . . . . . 15
            
       |
26 | 25 | con2bid 329 |
. . . . . . . . . . . . . 14
            
       |
27 | 13, 23, 26 | 3bitr2rd 282 |
. . . . . . . . . . . . 13
                    |
28 | 27 | biimpa 484 |
. . . . . . . . . . . 12
                    |
29 | 28 | adantlr 714 |
. . . . . . . . . . 11
                      |
30 | | nnrp 11104 |
. . . . . . . . . . . . 13
   |
31 | 30 | rpreccld 11141 |
. . . . . . . . . . . 12
     |
32 | 31 | ad2antlr 726 |
. . . . . . . . . . 11
                    |
33 | 29, 32 | ltsubrpd 11159 |
. . . . . . . . . 10
                              |
34 | 10, 33 | eqbrtrd 4413 |
. . . . . . . . 9
                                       |
35 | 8, 34 | pm2.61dan 789 |
. . . . . . . 8
        
                        |
36 | | nnrecre 10462 |
. . . . . . . . . . . . 13
     |
37 | 36 | ad2antlr 726 |
. . . . . . . . . . . 12
                    |
38 | 29, 37 | resubcld 9880 |
. . . . . . . . . . 11
                          |
39 | 2, 38 | ifclda 3922 |
. . . . . . . . . 10
        
                    |
40 | 39 | rexrd 9537 |
. . . . . . . . 9
        
                    |
41 | 11 | adantr 465 |
. . . . . . . . 9
        
       |
42 | | xrltnle 9547 |
. . . . . . . . 9
                  
             
                
                    |
43 | 40, 41, 42 | syl2anc 661 |
. . . . . . . 8
        
                      
           
            |
44 | 35, 43 | mpbid 210 |
. . . . . . 7
        
    
                   |
45 | | itg2leub 21338 |
. . . . . . . 8
                
                               
   
                         |
46 | 40, 45 | syldan 470 |
. . . . . . 7
        
     
                
   
                         |
47 | 44, 46 | mtbid 300 |
. . . . . 6
        
    
                        |
48 | | rexanali 2875 |
. . . . . 6
                          
   
                        |
49 | 47, 48 | sylibr 212 |
. . . . 5
        
                             |
50 | | itg1cl 21289 |
. . . . . . . 8
       |
51 | | ltnle 9558 |
. . . . . . . 8
                                
                
                    |
52 | 39, 50, 51 | syl2an 477 |
. . . . . . 7
           
        
                
                    |
53 | 52 | anbi2d 703 |
. . . . . 6
           
                                                    |
54 | 53 | rexbidva 2852 |
. . . . 5
        
     
       
                                           |
55 | 49, 54 | mpbird 232 |
. . . 4
        
            
                |
56 | 55 | ralrimiva 2825 |
. . 3
        
           
                |
57 | | ovex 6218 |
. . . . 5
   |
58 | | i1ff 21280 |
. . . . . . 7
       |
59 | | reex 9477 |
. . . . . . . 8
 |
60 | 59, 59 | elmap 7344 |
. . . . . . 7
  
      |
61 | 58, 60 | sylibr 212 |
. . . . . 6
     |
62 | 61 | ssriv 3461 |
. . . . 5
   |
63 | 57, 62 | ssexi 4538 |
. . . 4
 |
64 | | nnenom 11912 |
. . . 4
 |
65 | | breq1 4396 |
. . . . 5
               |
66 | | fveq2 5792 |
. . . . . 6
                   |
67 | 66 | breq2d 4405 |
. . . . 5
             
                                         |
68 | 65, 67 | anbi12d 710 |
. . . 4
               
                   
       
                     |
69 | 63, 64, 68 | axcc4 8712 |
. . 3
 
   
       
             
             
       
                     |
70 | 56, 69 | syl 16 |
. 2
              

                                   |
71 | | simprl 755 |
. . . . 5
                    
       
                          |
72 | | simpl 457 |
. . . . . . 7
                                        |
73 | 72 | ralimi 2814 |
. . . . . 6
 
                                        |
74 | 73 | ad2antll 728 |
. . . . 5
                    
       
                    
       |
75 | | fveq2 5792 |
. . . . . . . . . . . . 13
           |
76 | 75 | fveq2d 5796 |
. . . . . . . . . . . 12
                   |
77 | 76 | cbvmptv 4484 |
. . . . . . . . . . 11
                     |
78 | 77 | rneqi 5167 |
. . . . . . . . . 10
                     |
79 | 78 | supeq1i 7801 |
. . . . . . . . 9
                             |
80 | | ffvelrn 5943 |
. . . . . . . . . . . . . . 15
             |
81 | | itg1cl 21289 |
. . . . . . . . . . . . . . 15
               |
82 | 80, 81 | syl 16 |
. . . . . . . . . . . . . 14
                 |
83 | | eqid 2451 |
. . . . . . . . . . . . . 14
                     |
84 | 82, 83 | fmptd 5969 |
. . . . . . . . . . . . 13
                     |
85 | 84 | ad2antrl 727 |
. . . . . . . . . . . 12
                    
       
                                    |
86 | | frn 5666 |
. . . . . . . . . . . 12
                        
  |
87 | 85, 86 | syl 16 |
. . . . . . . . . . 11
                    
       
                             
  |
88 | | ressxr 9531 |
. . . . . . . . . . 11
 |
89 | 87, 88 | syl6ss 3469 |
. . . . . . . . . 10
                    
       
                             
  |
90 | | supxrcl 11381 |
. . . . . . . . . 10
          
                |
91 | 89, 90 | syl 16 |
. . . . . . . . 9
                    
       
                                 
  |
92 | 79, 91 | syl5eqelr 2544 |
. . . . . . . 8
                    
       
                                 
  |
93 | | elxr 11200 |
. . . . . . . . . . 11

    |
94 | | simplrl 759 |
. . . . . . . . . . . . . . . . . 18
                        |
95 | | arch 10680 |
. . . . . . . . . . . . . . . . . 18
    |
96 | 94, 95 | syl 16 |
. . . . . . . . . . . . . . . . 17
                         |
97 | 5 | adantl 466 |
. . . . . . . . . . . . . . . . . . 19
                             
           |
98 | 97 | breq2d 4405 |
. . . . . . . . . . . . . . . . . 18
                      
                
   |
99 | 98 | rexbidv 2855 |
. . . . . . . . . . . . . . . . 17
                       
                
    |
100 | 96, 99 | mpbird 232 |
. . . . . . . . . . . . . . . 16
                              
           |
101 | 28 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
                            |
102 | | simplrl 759 |
. . . . . . . . . . . . . . . . . . 19
                     
  |
103 | 101, 102 | resubcld 9880 |
. . . . . . . . . . . . . . . . . 18
                              |
104 | | simplrr 760 |
. . . . . . . . . . . . . . . . . . 19
                            |
105 | 102, 101 | posdifd 10030 |
. . . . . . . . . . . . . . . . . . 19
                          
         |
106 | 104, 105 | mpbid 210 |
. . . . . . . . . . . . . . . . . 18
                     
        |
107 | | nnrecl 10681 |
. . . . . . . . . . . . . . . . . 18
              
           |
108 | 103, 106,
107 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
                      
 
        |
109 | 36 | adantl 466 |
. . . . . . . . . . . . . . . . . . . 20
                      
     |
110 | 101 | adantr 465 |
. . . . . . . . . . . . . . . . . . . 20
                      
       |
111 | 102 | adantr 465 |
. . . . . . . . . . . . . . . . . . . 20
                      
   |
112 | | ltsub13 9924 |
. . . . . . . . . . . . . . . . . . . 20
           
     
           |
113 | 109, 110,
111, 112 | syl3anc 1219 |
. . . . . . . . . . . . . . . . . . 19
                      
         
           |
114 | 9 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
                      
                            |
115 | 114 | breq2d 4405 |
. . . . . . . . . . . . . . . . . . 19
                      
         
        
           |
116 | 113, 115 | bitr4d 256 |
. . . . . . . . . . . . . . . . . 18
                      
         
       
            |
117 | 116 | rexbidva 2852 |
. . . . . . . . . . . . . . . . 17
                               
        
            |
118 | 108, 117 | mpbid 210 |
. . . . . . . . . . . . . . . 16
                      
                   |
119 | 100, 118 | pm2.61dan 789 |
. . . . . . . . . . . . . . 15
         
                          |
120 | 119 | expr 615 |
. . . . . . . . . . . . . 14
        
      
                    |
121 | | rexr 9533 |
. . . . . . . . . . . . . . 15
   |
122 | | xrltnle 9547 |
. . . . . . . . . . . . . . 15
       
   
       |
123 | 121, 11, 122 | syl2anr 478 |
. . . . . . . . . . . . . 14
        
     
       |
124 | 121 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
              |
125 | 40 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
                               |
126 | | xrltnle 9547 |
. . . . . . . . . . . . . . . . 17
         
          
                
       
            |
127 | 124, 125,
126 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
                                                  |
128 | 127 | rexbidva 2852 |
. . . . . . . . . . . . . . 15
        
          
        
        
            |
129 | | rexnal 2847 |
. . . . . . . . . . . . . . 15
         
                             |
130 | 128, 129 | syl6bb 261 |
. . . . . . . . . . . . . 14
        
          
        
                     |
131 | 120, 123,
130 | 3imtr3d 267 |
. . . . . . . . . . . . 13
        
                           |
132 | 131 | con4d 105 |
. . . . . . . . . . . 12
        
                       
   |
133 | 11 | adantr 465 |
. . . . . . . . . . . . . . 15
        
       |
134 | | pnfge 11214 |
. . . . . . . . . . . . . . 15
    
      |
135 | 133, 134 | syl 16 |
. . . . . . . . . . . . . 14
        
    
  |
136 | | simpr 461 |
. . . . . . . . . . . . . 14
        
   |
137 | 135, 136 | breqtrrd 4419 |
. . . . . . . . . . . . 13
        
    
  |
138 | 137 | a1d 25 |
. . . . . . . . . . . 12
        
                       
   |
139 | | 1nn 10437 |
. . . . . . . . . . . . . . 15
 |
140 | | ne0i 3744 |
. . . . . . . . . . . . . . 15
   |
141 | 139, 140 | ax-mp 5 |
. . . . . . . . . . . . . 14
 |
142 | | r19.2z 3870 |
. . . . . . . . . . . . . 14
  
       
                              |
143 | 141, 142 | mpan 670 |
. . . . . . . . . . . . 13
 
       
                 
           |
144 | 39 | adantlr 714 |
. . . . . . . . . . . . . . . . 17
                               |
145 | | mnflt 11208 |
. . . . . . . . . . . . . . . . . 18
        
        
       
           |
146 | | rexr 9533 |
. . . . . . . . . . . . . . . . . . 19
        
        
                   |
147 | | xrltnle 9547 |
. . . . . . . . . . . . . . . . . . 19
        
                          
       
            |
148 | 16, 146, 147 | sylancr 663 |
. . . . . . . . . . . . . . . . . 18
        
        
                                     |
149 | 145, 148 | mpbid 210 |
. . . . . . . . . . . . . . . . 17
        
        
       
           |
150 | 144, 149 | syl 16 |
. . . . . . . . . . . . . . . 16
           
                   |
151 | | simplr 754 |
. . . . . . . . . . . . . . . . 17
              |
152 | 151 | breq2d 4405 |
. . . . . . . . . . . . . . . 16
                    
                             |
153 | 150, 152 | mtbird 301 |
. . . . . . . . . . . . . . 15
           
                   |
154 | 153 | nrexdv 2918 |
. . . . . . . . . . . . . 14
        
                     |
155 | 154 | pm2.21d 106 |
. . . . . . . . . . . . 13
        
                       
   |
156 | 143, 155 | syl5 32 |
. . . . . . . . . . . 12
        
                       
   |
157 | 132, 138,
156 | 3jaodan 1285 |
. . . . . . . . . . 11
         
   
       
            
   |
158 | 93, 157 | sylan2b 475 |
. . . . . . . . . 10
        
                       
   |
159 | 158 | ralrimiva 2825 |
. . . . . . . . 9
        
 
       
            
   |
160 | 159 | adantr 465 |
. . . . . . . 8
                    
       
                    
 
       
            
   |
161 | 40 | adantlr 714 |
. . . . . . . . . . . . 13
                       
           |
162 | 82 | adantll 713 |
. . . . . . . . . . . . . 14
                          |
163 | 162 | rexrd 9537 |
. . . . . . . . . . . . 13
                          |
164 | | xrltle 11230 |
. . . . . . . . . . . . 13
                  
                 
                                             |
165 | 161, 163,
164 | syl2anc 661 |
. . . . . . . . . . . 12
                        
                                             |
166 | 84 | adantl 466 |
. . . . . . . . . . . . . . . . . 18
                              |
167 | 166, 86 | syl 16 |
. . . . . . . . . . . . . . . . 17
             
            |
168 | 167, 88 | syl6ss 3469 |
. . . . . . . . . . . . . . . 16
             
            |
169 | 168 | adantr 465 |
. . . . . . . . . . . . . . 15
                
        
  |
170 | 78, 169 | syl5eqssr 3502 |
. . . . . . . . . . . . . 14
                
        
  |
171 | | fveq2 5792 |
. . . . . . . . . . . . . . . . . 18
           |
172 | 171 | fveq2d 5796 |
. . . . . . . . . . . . . . . . 17
                   |
173 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
                     |
174 | | fvex 5802 |
. . . . . . . . . . . . . . . . 17
         |
175 | 172, 173,
174 | fvmpt 5876 |
. . . . . . . . . . . . . . . 16
                         |
176 | | fvex 5802 |
. . . . . . . . . . . . . . . . . 18
         |
177 | 176, 173 | fnmpti 5640 |
. . . . . . . . . . . . . . . . 17
           |
178 | | fnfvelrn 5942 |
. . . . . . . . . . . . . . . . 17
           
                           |
179 | 177, 178 | mpan 670 |
. . . . . . . . . . . . . . . 16
                           |
180 | 175, 179 | eqeltrrd 2540 |
. . . . . . . . . . . . . . 15
                     |
181 | 180 | adantl 466 |
. . . . . . . . . . . . . 14
                                    |
182 | | supxrub 11391 |
. . . . . . . . . . . . . 14
                                                       |
183 | 170, 181,
182 | syl2anc 661 |
. . . . . . . . . . . . 13
                                     
  |
184 | 169, 90 | syl 16 |
. . . . . . . . . . . . . . 15
                                |
185 | 79, 184 | syl5eqelr 2544 |
. . . . . . . . . . . . . 14
                                |
186 | | xrletr 11236 |
. . . . . . . . . . . . . 14
                  
       
                                                                
                                  |
187 | 161, 163,
185, 186 | syl3anc 1219 |
. . . . . . . . . . . . 13
                                                                 
                                  |
188 | 183, 187 | mpan2d 674 |
. . . . . . . . . . . 12
                        
                                                   |
189 | 165, 188 | syld 44 |
. . . . . . . . . . 11
                        
                                                   |
190 | 189 | adantld 467 |
. . . . . . . . . 10
                              
                 
                                  |
191 | 190 | ralimdva 2827 |
. . . . . . . . 9
                     
       
                 
                                   |
192 | 191 | impr 619 |
. . . . . . . 8
                    
       
                    
       
                      
  |
193 | | breq2 4397 |
. . . . . . . . . . 11
                       
                                           |
194 | 193 | ralbidv 2841 |
. . . . . . . . . 10
                                          
                      
   |
195 | | breq2 4397 |
. . . . . . . . . 10
                                         |
196 | 194, 195 | imbi12d 320 |
. . . . . . . . 9
                 
       
            
          
                      
                      |
197 | 196 | rspcv 3168 |
. . . . . . . 8
              
                        
                                                   
    |
198 | 92, 160, 192, 197 | syl3c 61 |
. . . . . . 7
                    
       
                                        |
199 | 198, 79 | syl6breqr 4433 |
. . . . . 6
                    
       
                                        |
200 | | itg2ub 21337 |
. . . . . . . . . . . . . . 15
                                 |
201 | 200 | 3expia 1190 |
. . . . . . . . . . . . . 14
                   
               |
202 | 80, 201 | sylan2 474 |
. . . . . . . . . . . . 13
                                     |
203 | 202 | anassrs 648 |
. . . . . . . . . . . 12
                             
       |
204 | 203 | adantrd 468 |
. . . . . . . . . . 11
                              
                 
               |
205 | 204 | ralimdva 2827 |
. . . . . . . . . 10
                     
       
                 
        
       |
206 | 205 | impr 619 |
. . . . . . . . 9
                    
       
                    
              |
207 | 76, 83, 176 | fvmpt 5876 |
. . . . . . . . . . . 12
                         |
208 | 207 | breq1d 4403 |
. . . . . . . . . . 11
               
   
               |
209 | 208 | ralbiia 2833 |
. . . . . . . . . 10
 
                                 |
210 | 76 | breq1d 4403 |
. . . . . . . . . . 11
                     
       |
211 | 210 | cbvralv 3046 |
. . . . . . . . . 10
 
            
              |
212 | 209, 211 | bitr4i 252 |
. . . . . . . . 9
 
                                 |
213 | 206, 212 | sylibr 212 |
. . . . . . . 8
                    
       
                    
             
      |
214 | | ffn 5660 |
. . . . . . . . 9
                           |
215 | | breq1 4396 |
. . . . . . . . . 10
               
   
                     |
216 | 215 | ralrn 5948 |
. . . . . . . . 9
             
             
                      |
217 | 85, 214, 216 | 3syl 20 |
. . . . . . . 8
                    
       
                                     
             
       |
218 | 213, 217 | mpbird 232 |
. . . . . . 7
                    
       
                    

                |
219 | 11 | adantr 465 |
. . . . . . . 8
                    
       
                          |
220 | | supxrleub 11393 |
. . . . . . . 8
                               
    

                 |
221 | 89, 219, 220 | syl2anc 661 |
. . . . . . 7
                    
       
                                        
                 |
222 | 218, 221 | mpbird 232 |
. . . . . 6
                    
       
                                 
      |
223 | 11 | adantr 465 |
. . . . . . . 8
                    |
224 | 168, 90 | syl 16 |
. . . . . . . 8
                              |
225 | | xrletri3 11233 |
. . . . . . . 8
                                       
                  
             
        |
226 | 223, 224,
225 | syl2anc 661 |
. . . . . . 7
                                
                  
             
        |
227 | 226 | adantrr 716 |
. . . . . 6
                    
       
                                           
                                    |
228 | 199, 222,
227 | mpbir2and 913 |
. . . . 5
                    
       
                                        |
229 | 71, 74, 228 | 3jca 1168 |
. . . 4
                    
       
                                                    |
230 | 229 | ex 434 |
. . 3
             

                                
    

    
                      |
231 | 230 | eximdv 1677 |
. 2
                              
                                                      |
232 | 70, 231 | mpd 15 |
1
              

    
                     |