Step | Hyp | Ref
| Expression |
1 | | suplocicc.3 |
. . 3

  ![[,] [,]](_icc.gif)    |
2 | | suplocicc.1 |
. . . 4
   |
3 | | suplocicc.2 |
. . . 4
   |
4 | | iccssre 9955 |
. . . 4
 
   ![[,] [,]](_icc.gif) 
  |
5 | 2, 3, 4 | syl2anc 411 |
. . 3
   ![[,] [,]](_icc.gif) 
  |
6 | 1, 5 | sstrd 3166 |
. 2

  |
7 | | suplocicc.m |
. 2
    |
8 | | peano2re 8093 |
. . . 4
 
   |
9 | 3, 8 | syl 14 |
. . 3
     |
10 | 6 | sselda 3156 |
. . . . 5
 
   |
11 | 3 | adantr 276 |
. . . . 5
 
   |
12 | 9 | adantr 276 |
. . . . 5
 
 
   |
13 | 2 | rexrd 8007 |
. . . . . . 7
   |
14 | 13 | adantr 276 |
. . . . . 6
 
   |
15 | 3 | rexrd 8007 |
. . . . . . 7
   |
16 | 15 | adantr 276 |
. . . . . 6
 
   |
17 | 1 | sselda 3156 |
. . . . . 6
 
   ![[,] [,]](_icc.gif)    |
18 | | iccleub 9931 |
. . . . . 6
    ![[,] [,]](_icc.gif)     |
19 | 14, 16, 17, 18 | syl3anc 1238 |
. . . . 5
 
   |
20 | 11 | ltp1d 8887 |
. . . . 5
 
     |
21 | 10, 11, 12, 19, 20 | lelttrd 8082 |
. . . 4
 
     |
22 | 21 | ralrimiva 2550 |
. . 3
      |
23 | | brralrspcev 4062 |
. . 3
        
   |
24 | 9, 22, 23 | syl2anc 411 |
. 2
     |
25 | 7 | ad5antr 496 |
. . . . . . . . . 10
     

    
  |
26 | | simpr 110 |
. . . . . . . . . . . 12
               |
27 | | simp-4r 542 |
. . . . . . . . . . . . . 14
       

  |
28 | 27 | ad2antrr 488 |
. . . . . . . . . . . . 13
               |
29 | 2 | ad4antr 494 |
. . . . . . . . . . . . . 14
       

  |
30 | 29 | ad2antrr 488 |
. . . . . . . . . . . . 13
               |
31 | 6 | ad6antr 498 |
. . . . . . . . . . . . . 14
               |
32 | 31, 26 | sseldd 3157 |
. . . . . . . . . . . . 13
               |
33 | | simplr 528 |
. . . . . . . . . . . . 13
               |
34 | 13 | ad6antr 498 |
. . . . . . . . . . . . . 14
               |
35 | 15 | ad6antr 498 |
. . . . . . . . . . . . . 14
               |
36 | 1 | ad6antr 498 |
. . . . . . . . . . . . . . 15
               ![[,] [,]](_icc.gif)    |
37 | 36, 26 | sseldd 3157 |
. . . . . . . . . . . . . 14
               ![[,] [,]](_icc.gif)    |
38 | | iccgelb 9932 |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)     |
39 | 34, 35, 37, 38 | syl3anc 1238 |
. . . . . . . . . . . . 13
               |
40 | 28, 30, 32, 33, 39 | ltletrd 8380 |
. . . . . . . . . . . 12
               |
41 | | breq2 4008 |
. . . . . . . . . . . . 13
 
   |
42 | 41 | rspcev 2842 |
. . . . . . . . . . . 12
   
  |
43 | 26, 40, 42 | syl2anc 411 |
. . . . . . . . . . 11
             
  |
44 | 43 | orcd 733 |
. . . . . . . . . 10
              

   |
45 | 25, 44 | exlimddv 1898 |
. . . . . . . . 9
     

     

   |
46 | | simpllr 534 |
. . . . . . . . . . . . 13
     

      |
47 | | simplr 528 |
. . . . . . . . . . . . 13
     

      |
48 | | simp-5r 544 |
. . . . . . . . . . . . . 14
     

      |
49 | | simp-4r 542 |
. . . . . . . . . . . . . 14
     

      |
50 | 3 | ad5antr 496 |
. . . . . . . . . . . . . 14
     

      |
51 | | ltmininf 11243 |
. . . . . . . . . . . . . 14
 
 
inf           |
52 | 48, 49, 50, 51 | syl3anc 1238 |
. . . . . . . . . . . . 13
     

    
inf           |
53 | 46, 47, 52 | mpbir2and 944 |
. . . . . . . . . . . 12
     

    inf        |
54 | | simpr 110 |
. . . . . . . . . . . . 13
     

      |
55 | | suplocicc.bc |
. . . . . . . . . . . . . 14
   |
56 | 55 | ad5antr 496 |
. . . . . . . . . . . . 13
     

      |
57 | 2 | ad5antr 496 |
. . . . . . . . . . . . . 14
     

      |
58 | | ltmininf 11243 |
. . . . . . . . . . . . . 14
 
  inf     
     |
59 | 57, 49, 50, 58 | syl3anc 1238 |
. . . . . . . . . . . . 13
     

     inf     
     |
60 | 54, 56, 59 | mpbir2and 944 |
. . . . . . . . . . . 12
     

    inf        |
61 | | mincl 11239 |
. . . . . . . . . . . . . 14
 
 inf        |
62 | 49, 50, 61 | syl2anc 411 |
. . . . . . . . . . . . 13
     

    inf        |
63 | | maxltsup 11227 |
. . . . . . . . . . . . 13
 
inf    
        

inf      
inf     
inf          |
64 | 48, 57, 62, 63 | syl3anc 1238 |
. . . . . . . . . . . 12
     

            inf    
  inf    
 inf    
     |
65 | 53, 60, 64 | mpbir2and 944 |
. . . . . . . . . . 11
     

         

inf        |
66 | | breq2 4008 |
. . . . . . . . . . . . 13
 inf     
               inf    
    |
67 | | breq2 4008 |
. . . . . . . . . . . . . . 15
 inf     
 inf     
   |
68 | 67 | ralbidv 2477 |
. . . . . . . . . . . . . 14
 inf     
   inf     
   |
69 | 68 | orbi2d 790 |
. . . . . . . . . . . . 13
 inf     
  
     
  
 
     
  inf     
    |
70 | 66, 69 | imbi12d 234 |
. . . . . . . . . . . 12
 inf     
       
          
 
      

inf               
inf    
      |
71 | | breq1 4007 |
. . . . . . . . . . . . . . 15
                   |
72 | | breq1 4007 |
. . . . . . . . . . . . . . . . 17
                   |
73 | 72 | rexbidv 2478 |
. . . . . . . . . . . . . . . 16
                
    |
74 | 73 | orbi1d 791 |
. . . . . . . . . . . . . . 15
          
   
     
      |
75 | 71, 74 | imbi12d 234 |
. . . . . . . . . . . . . 14
         
 

 
      
          
     |
76 | 75 | ralbidv 2477 |
. . . . . . . . . . . . 13
            ![[,] [,]](_icc.gif)   
 

 
   ![[,] [,]](_icc.gif)         
          
     |
77 | | suplocicc.l |
. . . . . . . . . . . . . 14
    ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)           |
78 | 77 | ad5antr 496 |
. . . . . . . . . . . . 13
     

       ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)   
 

    |
79 | | maxcl 11219 |
. . . . . . . . . . . . . . 15
 
          |
80 | 48, 57, 79 | syl2anc 411 |
. . . . . . . . . . . . . 14
     

         
   |
81 | | maxle2 11221 |
. . . . . . . . . . . . . . 15
 

     
   |
82 | 48, 57, 81 | syl2anc 411 |
. . . . . . . . . . . . . 14
     

             |
83 | | maxltsup 11227 |
. . . . . . . . . . . . . . . . 17
 
              |
84 | 48, 57, 50, 83 | syl3anc 1238 |
. . . . . . . . . . . . . . . 16
     

                 |
85 | 47, 56, 84 | mpbir2and 944 |
. . . . . . . . . . . . . . 15
     

         
   |
86 | 80, 50, 85 | ltled 8076 |
. . . . . . . . . . . . . 14
     

         

  |
87 | | elicc2 9938 |
. . . . . . . . . . . . . . 15
 
           ![[,] [,]](_icc.gif)        
             

    |
88 | 57, 50, 87 | syl2anc 411 |
. . . . . . . . . . . . . 14
     

              ![[,] [,]](_icc.gif)                      

    |
89 | 80, 82, 86, 88 | mpbir3and 1180 |
. . . . . . . . . . . . 13
     

         
   ![[,] [,]](_icc.gif)    |
90 | 76, 78, 89 | rspcdva 2847 |
. . . . . . . . . . . 12
     

       ![[,] [,]](_icc.gif)         
          
    |
91 | 57, 62, 60 | ltled 8076 |
. . . . . . . . . . . . 13
     

    inf        |
92 | | min2inf 11241 |
. . . . . . . . . . . . . 14
 
 inf        |
93 | 49, 50, 92 | syl2anc 411 |
. . . . . . . . . . . . 13
     

    inf        |
94 | | elicc2 9938 |
. . . . . . . . . . . . . 14
 
 inf     
  ![[,] [,]](_icc.gif)  inf     
inf    

inf          |
95 | 57, 50, 94 | syl2anc 411 |
. . . . . . . . . . . . 13
     

    inf    
   ![[,] [,]](_icc.gif) 
inf    
 inf     
inf    

    |
96 | 62, 91, 93, 95 | mpbir3and 1180 |
. . . . . . . . . . . 12
     

    inf        ![[,] [,]](_icc.gif)    |
97 | 70, 90, 96 | rspcdva 2847 |
. . . . . . . . . . 11
     

            inf    

 
     
  inf     
    |
98 | 65, 97 | mpd 13 |
. . . . . . . . . 10
     

     
        inf     
   |
99 | 48 | ad2antrr 488 |
. . . . . . . . . . . . . 14
       

 
        
    |
100 | | simplr 528 |
. . . . . . . . . . . . . . . 16
       |
101 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
       |
102 | 100, 101,
79 | syl2anc 411 |
. . . . . . . . . . . . . . 15
          
   |
103 | 102 | ad5antr 496 |
. . . . . . . . . . . . . 14
       

 
        
           |
104 | 6 | ad6antr 498 |
. . . . . . . . . . . . . . . 16
               |
105 | | simpr 110 |
. . . . . . . . . . . . . . . 16
               |
106 | 104, 105 | sseldd 3157 |
. . . . . . . . . . . . . . 15
               |
107 | 106 | adantr 276 |
. . . . . . . . . . . . . 14
       

 
        
    |
108 | 57 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
       

 
        
    |
109 | | maxle1 11220 |
. . . . . . . . . . . . . . 15
 

     
   |
110 | 99, 108, 109 | syl2anc 411 |
. . . . . . . . . . . . . 14
       

 
        
       
   |
111 | | simpr 110 |
. . . . . . . . . . . . . 14
       

 
        
           |
112 | 99, 103, 107, 110, 111 | lelttrd 8082 |
. . . . . . . . . . . . 13
       

 
        
    |
113 | 112 | ex 115 |
. . . . . . . . . . . 12
                        |
114 | 113 | reximdva 2579 |
. . . . . . . . . . 11
     

     
           |
115 | 106 | adantr 276 |
. . . . . . . . . . . . . 14
       

 
   inf         |
116 | 62 | ad2antrr 488 |
. . . . . . . . . . . . . 14
       

 
   inf       inf    
   |
117 | 49 | ad2antrr 488 |
. . . . . . . . . . . . . 14
       

 
   inf         |
118 | | simpr 110 |
. . . . . . . . . . . . . 14
       

 
   inf      
inf        |
119 | | simpr 110 |
. . . . . . . . . . . . . . . 16
       |
120 | 3 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
       |
121 | | min1inf 11240 |
. . . . . . . . . . . . . . . 16
 
 inf        |
122 | 119, 120,
121 | syl2anc 411 |
. . . . . . . . . . . . . . 15
     inf        |
123 | 122 | ad5antr 496 |
. . . . . . . . . . . . . 14
       

 
   inf       inf    

  |
124 | 115, 116,
117, 118, 123 | ltletrd 8380 |
. . . . . . . . . . . . 13
       

 
   inf      
  |
125 | 124 | ex 115 |
. . . . . . . . . . . 12
             
inf         |
126 | 125 | ralimdva 2544 |
. . . . . . . . . . 11
     

     
inf     

   |
127 | 114, 126 | orim12d 786 |
. . . . . . . . . 10
     

              
inf    
   

    |
128 | 98, 127 | mpd 13 |
. . . . . . . . 9
     

     

   |
129 | | simplr 528 |
. . . . . . . . . 10
       

  |
130 | | simpllr 534 |
. . . . . . . . . . 11
       

  |
131 | | axltwlin 8025 |
. . . . . . . . . . 11
 
 
     |
132 | 27, 130, 29, 131 | syl3anc 1238 |
. . . . . . . . . 10
       


     |
133 | 129, 132 | mpd 13 |
. . . . . . . . 9
       

    |
134 | 45, 128, 133 | mpjaodan 798 |
. . . . . . . 8
       

 

   |
135 | 6 | ad5antr 496 |
. . . . . . . . . . . 12
     

      |
136 | | simpr 110 |
. . . . . . . . . . . 12
     

      |
137 | 135, 136 | sseldd 3157 |
. . . . . . . . . . 11
     

      |
138 | 3 | ad5antr 496 |
. . . . . . . . . . 11
     

      |
139 | | simp-4r 542 |
. . . . . . . . . . 11
     

      |
140 | 13 | ad5antr 496 |
. . . . . . . . . . . 12
     

      |
141 | 15 | ad5antr 496 |
. . . . . . . . . . . 12
     

      |
142 | 1 | ad5antr 496 |
. . . . . . . . . . . . 13
     

      ![[,] [,]](_icc.gif)    |
143 | 142, 136 | sseldd 3157 |
. . . . . . . . . . . 12
     

      ![[,] [,]](_icc.gif)    |
144 | | iccleub 9931 |
. . . . . . . . . . . 12
    ![[,] [,]](_icc.gif)     |
145 | 140, 141,
143, 144 | syl3anc 1238 |
. . . . . . . . . . 11
     

      |
146 | | simplr 528 |
. . . . . . . . . . 11
     

      |
147 | 137, 138,
139, 145, 146 | lelttrd 8082 |
. . . . . . . . . 10
     

      |
148 | 147 | ralrimiva 2550 |
. . . . . . . . 9
       


  |
149 | 148 | olcd 734 |
. . . . . . . 8
       

 

   |
150 | | axltwlin 8025 |
. . . . . . . . . 10
 
 
     |
151 | 100, 119,
120, 150 | syl3anc 1238 |
. . . . . . . . 9
     
     |
152 | 151 | imp 124 |
. . . . . . . 8
   

 
    |
153 | 134, 149,
152 | mpjaodan 798 |
. . . . . . 7
   

 
 

   |
154 | 153 | ex 115 |
. . . . . 6
     
  
    |
155 | 154 | ralrimiva 2550 |
. . . . 5
 

 
 

    |
156 | 155 | ralrimiva 2550 |
. . . 4
   
  
    |
157 | | breq2 4008 |
. . . . . . 7
 
   |
158 | | breq2 4008 |
. . . . . . . . 9
 
   |
159 | 158 | ralbidv 2477 |
. . . . . . . 8
  

   |
160 | 159 | orbi2d 790 |
. . . . . . 7
     
 

    |
161 | 157, 160 | imbi12d 234 |
. . . . . 6
                 |
162 | 161 | cbvralv 2704 |
. . . . 5
 

  
 
 
 

    |
163 | 162 | ralbii 2483 |
. . . 4
 
 
 

 
  
 

    |
164 | 156, 163 | sylib 122 |
. . 3
   
  
    |
165 | | breq1 4007 |
. . . . . 6
 
   |
166 | | breq1 4007 |
. . . . . . . 8
 
   |
167 | 166 | rexbidv 2478 |
. . . . . . 7
  

   |
168 | 167 | orbi1d 791 |
. . . . . 6
     
 

    |
169 | 165, 168 | imbi12d 234 |
. . . . 5
                 |
170 | 169 | ralbidv 2477 |
. . . 4
  

     

        |
171 | 170 | cbvralv 2704 |
. . 3
 
 
 

 
  
 

    |
172 | 164, 171 | sylib 122 |
. 2
   
  
    |
173 | | axsuploc 8030 |
. 2
      
 
 
 

      
 
     |
174 | 6, 7, 24, 172, 173 | syl22anc 1239 |
1
   
 
     |