Step | Hyp | Ref
| Expression |
1 | | limcrcl 14130 |
. . . . 5
  lim      
   |
2 | 1 | simp3d 1011 |
. . . 4
  lim    |
3 | 2 | a1i 9 |
. . 3
   lim     |
4 | | limcrcl 14130 |
. . . . 5
    #
  lim
   
#
      #      
#      |
5 | 4 | simp3d 1011 |
. . . 4
    #
  lim
   |
6 | 5 | a1i 9 |
. . 3
    
#   lim 
   |
7 | | breq1 4007 |
. . . . . . . . . . . . . . . . 17
  #
#    |
8 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
   


# 
  |
9 | | simpr 110 |
. . . . . . . . . . . . . . . . 17
   


# 
#   |
10 | 7, 8, 9 | elrabd 2896 |
. . . . . . . . . . . . . . . 16
   


# 
 #    |
11 | | fvres 5540 |
. . . . . . . . . . . . . . . . 17
  #     #
           |
12 | 11 | eqcomd 2183 |
. . . . . . . . . . . . . . . 16
  #        
#        |
13 | 10, 12 | syl 14 |
. . . . . . . . . . . . . . 15
   


# 
      
#        |
14 | 13 | fvoveq1d 5897 |
. . . . . . . . . . . . . 14
   


# 
                
#          |
15 | 14 | breq1d 4014 |
. . . . . . . . . . . . 13
   


# 
                 
#
          |
16 | 15 | imbi2d 230 |
. . . . . . . . . . . 12
   


# 
                                
#
           |
17 | 16 | pm5.74da 443 |
. . . . . . . . . . 11
       #                     #              
#
            |
18 | | impexp 263 |
. . . . . . . . . . 11
   #                    #                      |
19 | | impexp 263 |
. . . . . . . . . . . . 13
   #              
#
       
 #              
#
           |
20 | 19 | imbi2i 226 |
. . . . . . . . . . . 12
  #   #              
#
        
 #  #              
#
            |
21 | | pm5.4 249 |
. . . . . . . . . . . 12
  #  #              
#
           #              
#
           |
22 | 20, 21 | bitri 184 |
. . . . . . . . . . 11
  #   #              
#
        
 #              
#
           |
23 | 17, 18, 22 | 3bitr4g 223 |
. . . . . . . . . 10
        #                    #   #              
#
            |
24 | 23 | ralbidva 2473 |
. . . . . . . . 9
 

 
  #                   
 #
  #              
#
            |
25 | 7 | ralrab 2899 |
. . . . . . . . 9
 

# 
  #             

#         
 #
  #              
#
           |
26 | 24, 25 | bitr4di 198 |
. . . . . . . 8
 

 
  #                   

# 
  #             

#            |
27 | 26 | rexbidv 2478 |
. . . . . . 7
 

  
  #                  
   #
   #              
#
           |
28 | 27 | ralbidv 2477 |
. . . . . 6
 

 
    #       
               #
   #              
#
           |
29 | 28 | anbi2d 464 |
. . . . 5
 

       #       
           
     #    #             

#             |
30 | | limccl.f |
. . . . . . 7
       |
31 | 30 | adantr 276 |
. . . . . 6
 

      |
32 | | limcdifap.a |
. . . . . . 7

  |
33 | 32 | adantr 276 |
. . . . . 6
 

  |
34 | | simpr 110 |
. . . . . 6
 

  |
35 | 31, 33, 34 | ellimc3ap 14133 |
. . . . 5
 

  lim 
      #                       |
36 | | ssrab2 3241 |
. . . . . . 7

# 
 |
37 | | fssres 5392 |
. . . . . . 7
       #  
  #
    
#      |
38 | 31, 36, 37 | sylancl 413 |
. . . . . 6
 

  #
    
#      |
39 | 36, 33 | sstrid 3167 |
. . . . . 6
 


# 
  |
40 | 38, 39, 34 | ellimc3ap 14133 |
. . . . 5
 

    #
  lim
      #
   #              
#
            |
41 | 29, 35, 40 | 3bitr4d 220 |
. . . 4
 

  lim 
  
#
  lim
    |
42 | 41 | ex 115 |
. . 3
    lim   

#   lim      |
43 | 3, 6, 42 | pm5.21ndd 705 |
. 2
   lim   

#   lim     |
44 | 43 | eqrdv 2175 |
1
  lim   

#   lim    |