Step | Hyp | Ref
| Expression |
1 | | breq2 4007 |
. . . . . . . . . 10
        
                                |
2 | 1 | imbi2d 230 |
. . . . . . . . 9
        
   #                     #                              |
3 | 2 | rexralbidv 2503 |
. . . . . . . 8
        
 

  #                  
    #       
                      |
4 | | limcflf.f |
. . . . . . . . . . . . 13
       |
5 | | limcflf.a |
. . . . . . . . . . . . 13

  |
6 | | limcimo.b |
. . . . . . . . . . . . 13
   |
7 | 4, 5, 6 | ellimc3ap 14100 |
. . . . . . . . . . . 12
   lim     
  #                       |
8 | 7 | biimpa 296 |
. . . . . . . . . . 11
 

lim  
      #                      |
9 | 8 | adantrr 479 |
. . . . . . . . . 10
 
  lim 

lim          #       
              |
10 | 9 | simprd 114 |
. . . . . . . . 9
 
  lim 

lim         #                     |
11 | 10 | adantr 276 |
. . . . . . . 8
     lim 
 lim    #    
  #                     |
12 | 9 | simpld 112 |
. . . . . . . . . . . 12
 
  lim 

lim      |
13 | 12 | adantr 276 |
. . . . . . . . . . 11
     lim 
 lim    #    |
14 | 4, 5, 6 | ellimc3ap 14100 |
. . . . . . . . . . . . . . 15
   lim     
  #                       |
15 | 14 | biimpa 296 |
. . . . . . . . . . . . . 14
 

lim  
      #                      |
16 | 15 | adantrl 478 |
. . . . . . . . . . . . 13
 
  lim 

lim          #       
              |
17 | 16 | simpld 112 |
. . . . . . . . . . . 12
 
  lim 

lim      |
18 | 17 | adantr 276 |
. . . . . . . . . . 11
     lim 
 lim    #    |
19 | 13, 18 | subcld 8267 |
. . . . . . . . . 10
     lim 
 lim    #      |
20 | | simpr 110 |
. . . . . . . . . . 11
     lim 
 lim    #  #   |
21 | 13, 18, 20 | subap0d 8600 |
. . . . . . . . . 10
     lim 
 lim    #    #
  |
22 | 19, 21 | absrpclapd 11196 |
. . . . . . . . 9
     lim 
 lim    #          |
23 | 22 | rphalfcld 9708 |
. . . . . . . 8
     lim 
 lim    #            |
24 | 3, 11, 23 | rspcdva 2846 |
. . . . . . 7
     lim 
 lim    #      #                             |
25 | | breq2 4007 |
. . . . . . . . . . . 12
        
                                |
26 | 25 | imbi2d 230 |
. . . . . . . . . . 11
        
   #                     #                              |
27 | 26 | rexralbidv 2503 |
. . . . . . . . . 10
        
 

  #                  
    #       
                      |
28 | 16 | simprd 114 |
. . . . . . . . . . 11
 
  lim 

lim         #                     |
29 | 28 | adantr 276 |
. . . . . . . . . 10
     lim 
 lim    #    
  #                     |
30 | 27, 29, 23 | rspcdva 2846 |
. . . . . . . . 9
     lim 
 lim    #      #                             |
31 | 30 | adantr 276 |
. . . . . . . 8
    
 lim 
 lim    #      #       
                     

  #                             |
32 | 4 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                                   |
33 | 5 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                               |
34 | 6 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                               |
35 | | limcimo.bc |
. . . . . . . . . 10
   |
36 | 35 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                               |
37 | | limcimo.bs |
. . . . . . . . . 10
   |
38 | 37 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                               |
39 | | limcimo.c |
. . . . . . . . . 10
  ↾t    |
40 | 39 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                             
↾t    |
41 | | limcimo.s |
. . . . . . . . . 10
      |
42 | 41 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                                  |
43 | | limcimo.ca |
. . . . . . . . . 10
  #
   |
44 | 43 | ad4antr 494 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                              #    |
45 | | limcflfcntop.k |
. . . . . . . . 9
      |
46 | | simplrl 535 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                               |
47 | | simprl 529 |
. . . . . . . . . 10
 
  lim 

lim     lim    |
48 | 47 | ad3antrrr 492 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                              lim    |
49 | | simprr 531 |
. . . . . . . . . 10
 
  lim 

lim     lim    |
50 | 49 | ad3antrrr 492 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                              lim    |
51 | | simplrr 536 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                             
  #                             |
52 | | simprl 529 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                               |
53 | | simprr 531 |
. . . . . . . . 9
       lim   lim    #   
  #                              
  #                             
  #                             |
54 | 32, 33, 34, 36, 38, 40, 42, 44, 45, 46, 48, 50, 51, 52, 53 | limcimolemlt 14103 |
. . . . . . . 8
       lim   lim    #   
  #                              
  #                                           |
55 | 31, 54 | rexlimddv 2599 |
. . . . . . 7
    
 lim 
 lim    #      #       
                                   |
56 | 24, 55 | rexlimddv 2599 |
. . . . . 6
     lim 
 lim    #                |
57 | 22 | rpred 9695 |
. . . . . . 7
     lim 
 lim    #          |
58 | 57 | ltnrd 8068 |
. . . . . 6
     lim 
 lim    # 
              |
59 | 56, 58 | pm2.65da 661 |
. . . . 5
 
  lim 

lim    #   |
60 | | apti 8578 |
. . . . . 6
 
 
#    |
61 | 12, 17, 60 | syl2anc 411 |
. . . . 5
 
  lim 

lim    
#    |
62 | 59, 61 | mpbird 167 |
. . . 4
 
  lim 

lim      |
63 | 62 | ex 115 |
. . 3
    lim 

lim  
   |
64 | 63 | alrimivv 1875 |
. 2
        lim 

lim  
   |
65 | | eleq1w 2238 |
. . 3
   lim 

lim     |
66 | 65 | mo4 2087 |
. 2
   lim         lim   lim  
   |
67 | 64, 66 | sylibr 134 |
1
   lim    |