Step | Hyp | Ref
| Expression |
1 | | limsupbnd2.5 |
. . 3
   
       |
2 | | limsupbnd2.4 |
. . . . . . . . 9
       |
3 | | limsupbnd.1 |
. . . . . . . . . . 11

  |
4 | | ressxr 9689 |
. . . . . . . . . . 11
 |
5 | 3, 4 | syl6ss 3446 |
. . . . . . . . . 10

  |
6 | | supxrunb1 11612 |
. . . . . . . . . 10

 

       |
7 | 5, 6 | syl 17 |
. . . . . . . . 9
           |
8 | 2, 7 | mpbird 236 |
. . . . . . . 8
     |
9 | | ifcl 3925 |
. . . . . . . 8
 
   
    |
10 | | breq1 4408 |
. . . . . . . . . 10
               |
11 | 10 | rexbidv 2903 |
. . . . . . . . 9
                 |
12 | 11 | rspccva 3151 |
. . . . . . . 8
          
       |
13 | 8, 9, 12 | syl2an 480 |
. . . . . . 7
 
   
       |
14 | | r19.29 2927 |
. . . . . . . 8
   
            
 
      
 
    |
15 | | simplrr 772 |
. . . . . . . . . . . . . . 15
   
 
   |
16 | | simprl 765 |
. . . . . . . . . . . . . . . 16
 
  
  |
17 | 16 | adantr 467 |
. . . . . . . . . . . . . . 15
   
 
   |
18 | | max1 11487 |
. . . . . . . . . . . . . . 15
 

 
 
   |
19 | 15, 17, 18 | syl2anc 667 |
. . . . . . . . . . . . . 14
   
 
   
    |
20 | 17, 15, 9 | syl2anc 667 |
. . . . . . . . . . . . . . 15
   
 
        |
21 | 3 | adantr 467 |
. . . . . . . . . . . . . . . 16
 
     |
22 | 21 | sselda 3434 |
. . . . . . . . . . . . . . 15
   
 
   |
23 | | letr 9732 |
. . . . . . . . . . . . . . 15
                        |
24 | 15, 20, 22, 23 | syl3anc 1269 |
. . . . . . . . . . . . . 14
   
 
                 |
25 | 19, 24 | mpand 682 |
. . . . . . . . . . . . 13
   
 
          |
26 | 25 | imim1d 78 |
. . . . . . . . . . . 12
   
 
  
          
        |
27 | 26 | impd 433 |
. . . . . . . . . . 11
   
 
   
      
 
         |
28 | | max2 11489 |
. . . . . . . . . . . . . . 15
 

 
 
   |
29 | 15, 17, 28 | syl2anc 667 |
. . . . . . . . . . . . . 14
   
 
   
    |
30 | | letr 9732 |
. . . . . . . . . . . . . . 15
                        |
31 | 17, 20, 22, 30 | syl3anc 1269 |
. . . . . . . . . . . . . 14
   
 
                 |
32 | 29, 31 | mpand 682 |
. . . . . . . . . . . . 13
   
 
          |
33 | 32 | adantld 469 |
. . . . . . . . . . . 12
   
 
   
      
 
     |
34 | | eqid 2453 |
. . . . . . . . . . . . . . . . . . 19
            
              
   |
35 | 34 | limsupgf 13545 |
. . . . . . . . . . . . . . . . . 18
            
       |
36 | 35 | ffvelrni 6026 |
. . . . . . . . . . . . . . . . 17
              
       |
37 | 36 | adantl 468 |
. . . . . . . . . . . . . . . 16
 

             
       |
38 | | xrleid 11456 |
. . . . . . . . . . . . . . . 16
              
    
             
                  
       |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . 15
 

             
                  
       |
40 | 39 | adantrr 724 |
. . . . . . . . . . . . . 14
 
                                   
       |
41 | | limsupbnd.2 |
. . . . . . . . . . . . . . . 16
       |
42 | 41 | adantr 467 |
. . . . . . . . . . . . . . 15
 
         |
43 | 16, 36 | syl 17 |
. . . . . . . . . . . . . . 15
 
                        |
44 | 34 | limsupgle 13547 |
. . . . . . . . . . . . . . 15
       
                                  
                  
     

   
             
         |
45 | 21, 42, 16, 43, 44 | syl211anc 1275 |
. . . . . . . . . . . . . 14
 
                 
                  
     

   
             
         |
46 | 40, 45 | mpbid 214 |
. . . . . . . . . . . . 13
 
   

   
             
        |
47 | 46 | r19.21bi 2759 |
. . . . . . . . . . . 12
   
 
 
                 
        |
48 | 33, 47 | syld 45 |
. . . . . . . . . . 11
   
 
   
      
 
                            |
49 | 27, 48 | jcad 536 |
. . . . . . . . . 10
   
 
   
      
 
                                  |
50 | | limsupbnd.3 |
. . . . . . . . . . . 12
   |
51 | 50 | ad2antrr 733 |
. . . . . . . . . . 11
   
 
   |
52 | 42 | ffvelrnda 6027 |
. . . . . . . . . . 11
   
 
       |
53 | 43 | adantr 467 |
. . . . . . . . . . 11
   
 
              
       |
54 | | xrletr 11462 |
. . . . . . . . . . 11
                   
               
             
     
             
        |
55 | 51, 52, 53, 54 | syl3anc 1269 |
. . . . . . . . . 10
   
 
          
             
     
             
        |
56 | 49, 55 | syld 45 |
. . . . . . . . 9
   
 
   
      
 
                        |
57 | 56 | rexlimdva 2881 |
. . . . . . . 8
 
                               
        |
58 | 14, 57 | syl5 33 |
. . . . . . 7
 
     

     
 
 
                        |
59 | 13, 58 | mpan2d 681 |
. . . . . 6
 
     
    
             
        |
60 | 59 | anassrs 654 |
. . . . 5
      

                  
        |
61 | 60 | rexlimdva 2881 |
. . . 4
 

  

                  
        |
62 | 61 | ralrimdva 2808 |
. . 3
    
    
              
        |
63 | 1, 62 | mpd 15 |
. 2
               
       |
64 | 34 | limsupleOLD 13549 |
. . 3
 
                        
        |
65 | 3, 41, 50, 64 | syl3anc 1269 |
. 2
     
              
        |
66 | 63, 65 | mpbird 236 |
1

      |