Proof of Theorem supxrgelem
Step | Hyp | Ref
| Expression |
1 | | supxrgelem.b |
. . . . 5
   |
2 | | pnfge 11466 |
. . . . 5

  |
3 | 1, 2 | syl 17 |
. . . 4

  |
4 | 3 | adantr 471 |
. . 3
 
  
    |
5 | | id 22 |
. . . . 5
           |
6 | 5 | eqcomd 2468 |
. . . 4
       
   |
7 | 6 | adantl 472 |
. . 3
 
  
 
  
   |
8 | 4, 7 | breqtrd 4443 |
. 2
 
  
        |
9 | | simpl 463 |
. . 3
 
  
    |
10 | | 1rp 11340 |
. . . . . . . 8
 |
11 | | nfcv 2603 |
. . . . . . . . . 10
   |
12 | | supxrgelem.xph |
. . . . . . . . . . . 12
   |
13 | | nfv 1772 |
. . . . . . . . . . . 12
   |
14 | 12, 13 | nfan 2022 |
. . . . . . . . . . 11
  
  |
15 | | nfv 1772 |
. . . . . . . . . . 11
  
      |
16 | 14, 15 | nfim 2014 |
. . . . . . . . . 10
   
 
       |
17 | | eleq1 2528 |
. . . . . . . . . . . 12
 
   |
18 | 17 | anbi2d 715 |
. . . . . . . . . . 11
  

     |
19 | | oveq2 6328 |
. . . . . . . . . . . . 13
             |
20 | 19 | breq2d 4430 |
. . . . . . . . . . . 12
      
        |
21 | 20 | rexbidv 2913 |
. . . . . . . . . . 11
  
    

        |
22 | 18, 21 | imbi12d 326 |
. . . . . . . . . 10
   
 
       
 
         |
23 | | supxrgelem.y |
. . . . . . . . . 10
 


       |
24 | 11, 16, 22, 23 | vtoclgf 3117 |
. . . . . . . . 9

 


        |
25 | 10, 24 | ax-mp 5 |
. . . . . . . 8
 


       |
26 | 10, 25 | mpan2 682 |
. . . . . . 7
         |
27 | 26 | adantr 471 |
. . . . . 6
 
  
  
       |
28 | | mnfxr 11448 |
. . . . . . . . . . 11
 |
29 | 28 | a1i 11 |
. . . . . . . . . 10
 
        |
30 | | supxrgelem.a |
. . . . . . . . . . . 12

  |
31 | 30 | sselda 3444 |
. . . . . . . . . . 11
 
   |
32 | 31 | 3adant3 1034 |
. . . . . . . . . 10
 
        |
33 | | supxrcl 11634 |
. . . . . . . . . . . 12

  
   |
34 | 30, 33 | syl 17 |
. . . . . . . . . . 11
       |
35 | 34 | 3ad2ant1 1035 |
. . . . . . . . . 10
 
            |
36 | | simpl3 1019 |
. . . . . . . . . . . 12
  
     
        |
37 | | simpr 467 |
. . . . . . . . . . . . . . . 16
    
  |
38 | 31 | adantr 471 |
. . . . . . . . . . . . . . . . 17
       |
39 | | ngtmnft 11496 |
. . . . . . . . . . . . . . . . 17


   |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . 16
         |
41 | 37, 40 | mpbird 240 |
. . . . . . . . . . . . . . 15
       |
42 | 41 | oveq1d 6335 |
. . . . . . . . . . . . . 14
                |
43 | | 1re 9673 |
. . . . . . . . . . . . . . . . 17
 |
44 | 43 | rexri 9724 |
. . . . . . . . . . . . . . . 16
 |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
46 | | renepnf 9719 |
. . . . . . . . . . . . . . . . 17
   |
47 | 43, 46 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
 |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . . 15
       |
49 | | xaddmnf2 11556 |
. . . . . . . . . . . . . . 15
         |
50 | 45, 48, 49 | syl2anc 671 |
. . . . . . . . . . . . . 14
           |
51 | 42, 50 | eqtrd 2496 |
. . . . . . . . . . . . 13
            |
52 | 51 | 3adantl3 1172 |
. . . . . . . . . . . 12
  
     
        |
53 | 36, 52 | breqtrd 4443 |
. . . . . . . . . . 11
  
     
   |
54 | | nltmnf 11465 |
. . . . . . . . . . . . . 14

  |
55 | 1, 54 | syl 17 |
. . . . . . . . . . . . 13
   |
56 | 55 | adantr 471 |
. . . . . . . . . . . 12
 

  |
57 | 56 | 3ad2antl1 1176 |
. . . . . . . . . . 11
  
     
   |
58 | 53, 57 | condan 808 |
. . . . . . . . . 10
 
        |
59 | 30 | adantr 471 |
. . . . . . . . . . . 12
 
   |
60 | | simpr 467 |
. . . . . . . . . . . 12
 
   |
61 | | supxrub 11644 |
. . . . . . . . . . . 12
 
       |
62 | 59, 60, 61 | syl2anc 671 |
. . . . . . . . . . 11
 
       |
63 | 62 | 3adant3 1034 |
. . . . . . . . . 10
 
            |
64 | 29, 32, 35, 58, 63 | xrltletrd 11492 |
. . . . . . . . 9
 
            |
65 | 64 | 3exp 1214 |
. . . . . . . 8
       
        |
66 | 65 | adantr 471 |
. . . . . . 7
 
  
        
        |
67 | 66 | rexlimdv 2889 |
. . . . . 6
 
  
        
       |
68 | 27, 67 | mpd 15 |
. . . . 5
 
  
        |
69 | | simpr 467 |
. . . . . . 7
 
  
        |
70 | | nltpnft 11495 |
. . . . . . . . 9
         
  
    |
71 | 34, 70 | syl 17 |
. . . . . . . 8
     
  
    |
72 | 71 | adantr 471 |
. . . . . . 7
 
  
      
  
    |
73 | 69, 72 | mtbid 306 |
. . . . . 6
 
  
        |
74 | 73 | notnotrd 118 |
. . . . 5
 
  
        |
75 | 68, 74 | jca 539 |
. . . 4
 
  
 
  
        |
76 | 34 | adantr 471 |
. . . . 5
 
  
        |
77 | | xrrebnd 11497 |
. . . . 5
                      |
78 | 76, 77 | syl 17 |
. . . 4
 
  
                   |
79 | 75, 78 | mpbird 240 |
. . 3
 
  
        |
80 | | simpl 463 |
. . . . 5
       
  
 
        |
81 | | simpr 467 |
. . . . . 6
       
  
 
      |
82 | 34 | adantr 471 |
. . . . . . . 8
 
           |
83 | 1 | adantr 471 |
. . . . . . . 8
 
       |
84 | | xrltnle 9732 |
. . . . . . . 8
     

    
       |
85 | 82, 83, 84 | syl2anc 671 |
. . . . . . 7
 
        

       |
86 | 85 | adantlr 726 |
. . . . . 6
       
  
 
    
       |
87 | 81, 86 | mpbird 240 |
. . . . 5
       
  
 
  
   |
88 | | simpll 765 |
. . . . . . 7
            
  |
89 | 28 | a1i 11 |
. . . . . . . . . . . 12
            
  |
90 | 88, 34 | syl 17 |
. . . . . . . . . . . 12
            
  
   |
91 | 88, 1 | syl 17 |
. . . . . . . . . . . 12
            
  |
92 | | mnfle 11469 |
. . . . . . . . . . . . . 14
    
  
   |
93 | 34, 92 | syl 17 |
. . . . . . . . . . . . 13

  
   |
94 | 93 | ad2antrr 737 |
. . . . . . . . . . . 12
            
      |
95 | | simpr 467 |
. . . . . . . . . . . 12
            
  
   |
96 | 89, 90, 91, 94, 95 | xrlelttrd 11491 |
. . . . . . . . . . 11
            
  |
97 | | id 22 |
. . . . . . . . . . . . . 14
   |
98 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
   |
99 | 97, 98, 25 | syl2anc 671 |
. . . . . . . . . . . . 13
         |
100 | 99 | ad2antrr 737 |
. . . . . . . . . . . 12
            

       |
101 | 1 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . 16
 
        |
102 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
 
        |
103 | 32, 102 | jca 539 |
. . . . . . . . . . . . . . . . 17
 
          |
104 | | xaddcl 11564 |
. . . . . . . . . . . . . . . . 17
          |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . 16
 
             |
106 | | pnfxr 11446 |
. . . . . . . . . . . . . . . . 17
 |
107 | 106 | a1i 11 |
. . . . . . . . . . . . . . . 16
 
        |
108 | | simp3 1016 |
. . . . . . . . . . . . . . . 16
 
             |
109 | 31, 44, 104 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
 
        |
110 | | pnfge 11466 |
. . . . . . . . . . . . . . . . . 18
          
  |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
     
  |
112 | 111 | 3adant3 1034 |
. . . . . . . . . . . . . . . 16
 
          
  |
113 | 101, 105,
107, 108, 112 | xrltletrd 11492 |
. . . . . . . . . . . . . . 15
 
        |
114 | 113 | 3exp 1214 |
. . . . . . . . . . . . . 14
       
    |
115 | 114 | rexlimdv 2889 |
. . . . . . . . . . . . 13
       
   |
116 | 88, 115 | syl 17 |
. . . . . . . . . . . 12
            
 
        |
117 | 100, 116 | mpd 15 |
. . . . . . . . . . 11
            
  |
118 | 96, 117 | jca 539 |
. . . . . . . . . 10
            
   |
119 | | xrrebnd 11497 |
. . . . . . . . . . 11


    |
120 | 91, 119 | syl 17 |
. . . . . . . . . 10
            
     |
121 | 118, 120 | mpbird 240 |
. . . . . . . . 9
            
  |
122 | | simpr 467 |
. . . . . . . . . 10
 
  
        |
123 | 122 | adantr 471 |
. . . . . . . . 9
            
  
   |
124 | 121, 123 | resubcld 10080 |
. . . . . . . 8
            
        |
125 | 26, 115 | mpd 15 |
. . . . . . . . . . . . 13
   |
126 | 125 | ad2antrr 737 |
. . . . . . . . . . . 12
            
  |
127 | 96, 126 | jca 539 |
. . . . . . . . . . 11
            
   |
128 | 127, 120 | mpbird 240 |
. . . . . . . . . 10
            
  |
129 | 123, 128 | posdifd 10233 |
. . . . . . . . 9
            
    
   
     |
130 | 95, 129 | mpbid 215 |
. . . . . . . 8
            
   
    |
131 | 124, 130 | elrpd 11372 |
. . . . . . 7
            
        |
132 | | ovex 6348 |
. . . . . . . 8
       |
133 | | nfcv 2603 |
. . . . . . . . 9
         |
134 | | nfv 1772 |
. . . . . . . . . . 11
         |
135 | 12, 134 | nfan 2022 |
. . . . . . . . . 10
  

  
    |
136 | | nfv 1772 |
. . . . . . . . . 10
  
            |
137 | 135, 136 | nfim 2014 |
. . . . . . . . 9
    
                    |
138 | | eleq1 2528 |
. . . . . . . . . . 11
        
  
     |
139 | 138 | anbi2d 715 |
. . . . . . . . . 10
        

           |
140 | | oveq2 6328 |
. . . . . . . . . . . 12
                   
     |
141 | 140 | breq2d 4430 |
. . . . . . . . . . 11
            
              |
142 | 141 | rexbidv 2913 |
. . . . . . . . . 10
                             |
143 | 139, 142 | imbi12d 326 |
. . . . . . . . 9
                    
                      |
144 | 133, 137,
143, 23 | vtoclgf 3117 |
. . . . . . . 8
    
    
  
                  |
145 | 132, 144 | ax-mp 5 |
. . . . . . 7
 
       
       
     |
146 | 88, 131, 145 | syl2anc 671 |
. . . . . 6
            

       
     |
147 | | ltpnf 11456 |
. . . . . . . . . . . . 13
           |
148 | 147 | adantr 471 |
. . . . . . . . . . . 12
             |
149 | | id 22 |
. . . . . . . . . . . . . 14
   |
150 | 149 | eqcomd 2468 |
. . . . . . . . . . . . 13
   |
151 | 150 | adantl 472 |
. . . . . . . . . . . 12
         |
152 | 148, 151 | breqtrd 4443 |
. . . . . . . . . . 11
             |
153 | 152 | adantll 725 |
. . . . . . . . . 10
       
       |
154 | 153 | ad5ant15 1253 |
. . . . . . . . 9
     
  
      
            
       |
155 | | simplll 773 |
. . . . . . . . . 10
     
  
      
            
               |
156 | | simpl 463 |
. . . . . . . . . . . . . . 15
     
  
      
            
    
  
      
               |
157 | 88, 41 | sylanl1 660 |
. . . . . . . . . . . . . . . 16
              
 
  |
158 | 157 | adantlr 726 |
. . . . . . . . . . . . . . 15
     
  
      
            
   |
159 | | simplr 767 |
. . . . . . . . . . . . . . . 16
     
  
      
            
              |
160 | | oveq1 6327 |
. . . . . . . . . . . . . . . . . 18
        
         
     |
161 | 160 | adantl 472 |
. . . . . . . . . . . . . . . . 17
     
  
      
            
                  
     |
162 | 128, 123 | resubcld 10080 |
. . . . . . . . . . . . . . . . . . . 20
            
        |
163 | 162 | rexrd 9721 |
. . . . . . . . . . . . . . . . . . 19
            
        |
164 | 163 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . 18
     
  
      
            
         |
165 | | renepnf 9719 |
. . . . . . . . . . . . . . . . . . . 20
    
     
    |
166 | 124, 165 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
            
        |
167 | 166 | ad3antrrr 741 |
. . . . . . . . . . . . . . . . . 18
     
  
      
            
         |
168 | | xaddmnf2 11556 |
. . . . . . . . . . . . . . . . . 18
        
  
               |
169 | 164, 167,
168 | syl2anc 671 |
. . . . . . . . . . . . . . . . 17
     
  
      
            
             |
170 | 161, 169 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
     
  
      
            
              |
171 | 159, 170 | breqtrd 4443 |
. . . . . . . . . . . . . . 15
     
  
      
            
   |
172 | 156, 158,
171 | syl2anc 671 |
. . . . . . . . . . . . . 14
     
  
      
            
   |
173 | 55 | ad5antr 745 |
. . . . . . . . . . . . . 14
     
  
      
            
   |
174 | 172, 173 | condan 808 |
. . . . . . . . . . . . 13
              

              |
175 | 174 | adantr 471 |
. . . . . . . . . . . 12
     
  
      
            

  |
176 | | simp3 1016 |
. . . . . . . . . . . . . . . 16
 

  |
177 | 31 | 3adant3 1034 |
. . . . . . . . . . . . . . . . 17
 
   |
178 | | nltpnft 11495 |
. . . . . . . . . . . . . . . . 17


   |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . . . . 16
 
 
   |
180 | 176, 179 | mtbid 306 |
. . . . . . . . . . . . . . 15
 

  |
181 | 180 | notnotrd 118 |
. . . . . . . . . . . . . 14
 
   |
182 | 181 | 3adant1r 1269 |
. . . . . . . . . . . . 13
       
   |
183 | 182 | ad5ant135 1264 |
. . . . . . . . . . . 12
     
  
      
            
   |
184 | 175, 183 | jca 539 |
. . . . . . . . . . 11
     
  
      
            
    |
185 | 31 | adantlr 726 |
. . . . . . . . . . . . 13
       
   |
186 | 185 | ad5ant13 1251 |
. . . . . . . . . . . 12
     
  
      
            
   |
187 | | xrrebnd 11497 |
. . . . . . . . . . . 12


    |
188 | 186, 187 | syl 17 |
. . . . . . . . . . 11
     
  
      
            
      |
189 | 184, 188 | mpbird 240 |
. . . . . . . . . 10
     
  
      
            
   |
190 | | simplr 767 |
. . . . . . . . . 10
     
  
      
            
        
     |
191 | 121 | ad2antrr 737 |
. . . . . . . . . . . . 13
              

           
  |
192 | | simpr 467 |
. . . . . . . . . . . . . . . 16
                 |
193 | 124 | adantr 471 |
. . . . . . . . . . . . . . . 16
               
  
    |
194 | | rexadd 11559 |
. . . . . . . . . . . . . . . 16
  
                           |
195 | 192, 193,
194 | syl2anc 671 |
. . . . . . . . . . . . . . 15
                      
             |
196 | 192, 193 | readdcld 9701 |
. . . . . . . . . . . . . . 15
                         |
197 | 195, 196 | eqeltrd 2540 |
. . . . . . . . . . . . . 14
                      
     |
198 | 197 | adantr 471 |
. . . . . . . . . . . . 13
              

                         |
199 | | simpr 467 |
. . . . . . . . . . . . 13
              

                         |
200 | 191, 198,
191, 199 | ltsub1dd 10258 |
. . . . . . . . . . . 12
              

             
        
      |
201 | 121 | recnd 9700 |
. . . . . . . . . . . . . . 15
            
  |
202 | 201 | subidd 10005 |
. . . . . . . . . . . . . 14
            
    |
203 | 202 | ad2antrr 737 |
. . . . . . . . . . . . 13
              

                |
204 | 192 | recnd 9700 |
. . . . . . . . . . . . . . . . . 18
                 |
205 | 201 | adantr 471 |
. . . . . . . . . . . . . . . . . 18
                 |
206 | 122 | recnd 9700 |
. . . . . . . . . . . . . . . . . . 19
 
  
        |
207 | 206 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
                     |
208 | 204, 205,
207 | addsub12d 10040 |
. . . . . . . . . . . . . . . . 17
                                 |
209 | 195, 208 | eqtrd 2496 |
. . . . . . . . . . . . . . . 16
                      
             |
210 | 209 | oveq1d 6335 |
. . . . . . . . . . . . . . 15
                                        |
211 | 204, 207 | subcld 10017 |
. . . . . . . . . . . . . . . 16
                  
    |
212 | 205, 211 | pncan2d 10019 |
. . . . . . . . . . . . . . 15
                    
            |
213 | 210, 212 | eqtrd 2496 |
. . . . . . . . . . . . . 14
                                    |
214 | 213 | adantr 471 |
. . . . . . . . . . . . 13
              

                                 |
215 | 203, 214 | breq12d 4431 |
. . . . . . . . . . . 12
              

                               
     |
216 | 200, 215 | mpbid 215 |
. . . . . . . . . . 11
              

           
        |
217 | 123 | ad2antrr 737 |
. . . . . . . . . . . 12
              

                  |
218 | | simplr 767 |
. . . . . . . . . . . 12
              

              |
219 | 217, 218 | posdifd 10233 |
. . . . . . . . . . 11
              

                    
     |
220 | 216, 219 | mpbird 240 |
. . . . . . . . . 10
              

                  |
221 | 155, 189,
190, 220 | syl21anc 1275 |
. . . . . . . . 9
     
  
      
            
       |
222 | 154, 221 | pm2.61dan 805 |
. . . . . . . 8
              

                  |
223 | 222 | ex 440 |
. . . . . . 7
                                  |
224 | 223 | reximdva 2874 |
. . . . . 6
            
 
           
  
    |
225 | 146, 224 | mpd 15 |
. . . . 5
            

  
   |
226 | 80, 87, 225 | syl2anc 671 |
. . . 4
       
  
 

  
   |
227 | 59, 33 | syl 17 |
. . . . . . . . 9
 
       |
228 | 31, 227 | xrlenltd 9731 |
. . . . . . . 8
 
 
  
        |
229 | 62, 228 | mpbid 215 |
. . . . . . 7
 
       |
230 | 229 | ralrimiva 2814 |
. . . . . 6
        |
231 | | ralnex 2846 |
. . . . . 6
 
           |
232 | 230, 231 | sylib 201 |
. . . . 5
        |
233 | 232 | ad2antrr 737 |
. . . 4
       
  
 

  
   |
234 | 226, 233 | condan 808 |
. . 3
 
  
        |
235 | 9, 79, 234 | syl2anc 671 |
. 2
 
  
        |
236 | 8, 235 | pm2.61dan 805 |
1

  
   |