Step | Hyp | Ref
| Expression |
1 | | limccnp.j |
. . . . 5

↾t   |
2 | | limccnpcntop.k |
. . . . . . 7
      |
3 | 2 | cntoptopon 13699 |
. . . . . 6
TopOn   |
4 | | limccnp.d |
. . . . . 6

  |
5 | | resttopon 13338 |
. . . . . 6
  TopOn 

 ↾t  TopOn    |
6 | 3, 4, 5 | sylancr 414 |
. . . . 5
 
↾t  TopOn    |
7 | 1, 6 | eqeltrid 2264 |
. . . 4
 TopOn    |
8 | 3 | a1i 9 |
. . . 4
 TopOn    |
9 | | limccnp.b |
. . . 4
         |
10 | | cnpf2 13374 |
. . . 4
  TopOn  TopOn 
      
      |
11 | 7, 8, 9, 10 | syl3anc 1238 |
. . 3
       |
12 | 2 | cntoptop 13700 |
. . . . 5
 |
13 | 12 | a1i 9 |
. . . 4
   |
14 | | cnprcl2k 13373 |
. . . 4
  TopOn        
  |
15 | 7, 13, 9, 14 | syl3anc 1238 |
. . 3
   |
16 | 11, 15 | ffvelcdmd 5648 |
. 2
       |
17 | | cnxmet 13698 |
. . . . . . . 8

      |
18 | | eqid 2177 |
. . . . . . . . 9
           |
19 | | eqid 2177 |
. . . . . . . . 9
    
        
     |
20 | 18, 2, 19 | metrest 13673 |
. . . . . . . 8
  
      
↾t      
      |
21 | 17, 4, 20 | sylancr 414 |
. . . . . . 7
 
↾t      
      |
22 | 1, 21 | eqtrid 2222 |
. . . . . 6
     
      |
23 | 2 | a1i 9 |
. . . . . 6
        |
24 | | xmetres2 13546 |
. . . . . . 7
  
       
          |
25 | 17, 4, 24 | sylancr 414 |
. . . . . 6
  
          |
26 | 17 | a1i 9 |
. . . . . 6
 
       |
27 | 22, 23, 25, 26, 15 | metcnpd 13687 |
. . . . 5
                    
           
     
     |
28 | 9, 27 | mpbid 147 |
. . . 4
                                    |
29 | 28 | simprd 114 |
. . 3
   
    
           
     
   |
30 | | simplll 533 |
. . . . . . 7
   

                             |
31 | | simplr 528 |
. . . . . . 7
   

                             |
32 | | limccnp.c |
. . . . . . . . . 10
  lim    |
33 | | limccnp.f |
. . . . . . . . . . . 12
       |
34 | 33, 4 | fssd 5374 |
. . . . . . . . . . 11
       |
35 | 33 | fdmd 5368 |
. . . . . . . . . . . 12
   |
36 | | limcrcl 13794 |
. . . . . . . . . . . . . 14
  lim      
   |
37 | 32, 36 | syl 14 |
. . . . . . . . . . . . 13
         |
38 | 37 | simp2d 1010 |
. . . . . . . . . . . 12
   |
39 | 35, 38 | eqsstrrd 3192 |
. . . . . . . . . . 11

  |
40 | 37 | simp3d 1011 |
. . . . . . . . . . 11
   |
41 | 34, 39, 40 | ellimc3ap 13797 |
. . . . . . . . . 10
   lim     
  #                       |
42 | 32, 41 | mpbid 147 |
. . . . . . . . 9
    
  #                      |
43 | 42 | simprd 114 |
. . . . . . . 8
   
  #                     |
44 | 43 | r19.21bi 2565 |
. . . . . . 7
 

    #       
             |
45 | 30, 31, 44 | syl2anc 411 |
. . . . . 6
   

                               #                     |
46 | | oveq2 5877 |
. . . . . . . . . . . . 13
        
        
           |
47 | 46 | breq1d 4010 |
. . . . . . . . . . . 12
              
   
            |
48 | | fveq2 5511 |
. . . . . . . . . . . . . 14
                   |
49 | 48 | oveq2d 5885 |
. . . . . . . . . . . . 13
                                     |
50 | 49 | breq1d 4010 |
. . . . . . . . . . . 12
            
     
      
             |
51 | 47, 50 | imbi12d 234 |
. . . . . . . . . . 11
                      
     
                                    |
52 | | simpllr 534 |
. . . . . . . . . . 11
     
 

    
           
     
 
  
    
           
     
   |
53 | 33 | ad5antr 496 |
. . . . . . . . . . . 12
     
 

    
           
     
 
        |
54 | | simpr 110 |
. . . . . . . . . . . 12
     
 

    
           
     
 
    |
55 | 53, 54 | ffvelcdmd 5648 |
. . . . . . . . . . 11
     
 

    
           
     
 
        |
56 | 51, 52, 55 | rspcdva 2846 |
. . . . . . . . . 10
     
 

    
           
     
 
                                    |
57 | 15 | ad5antr 496 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
    |
58 | 57, 55 | ovresd 6009 |
. . . . . . . . . . . 12
     
 

    
           
     
 
     
                    |
59 | 42 | simpld 112 |
. . . . . . . . . . . . . 14
   |
60 | 59 | ad5antr 496 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
    |
61 | 4 | ad5antr 496 |
. . . . . . . . . . . . . 14
     
 

    
           
     
 
    |
62 | 61, 55 | sseldd 3156 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
        |
63 | | eqid 2177 |
. . . . . . . . . . . . . 14

  |
64 | 63 | cnmetdval 13696 |
. . . . . . . . . . . . 13
         
                  |
65 | 60, 62, 64 | syl2anc 411 |
. . . . . . . . . . . 12
     
 

    
           
     
 
              
        |
66 | 60, 62 | abssubd 11186 |
. . . . . . . . . . . 12
     
 

    
           
     
 
                        |
67 | 58, 65, 66 | 3eqtrd 2214 |
. . . . . . . . . . 11
     
 

    
           
     
 
     
                     |
68 | 67 | breq1d 4010 |
. . . . . . . . . 10
     
 

    
           
     
 
               
             |
69 | 16 | ad5antr 496 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
        |
70 | 11 | ad5antr 496 |
. . . . . . . . . . . . . 14
     
 

    
           
     
 
        |
71 | 70, 55 | ffvelcdmd 5648 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
            |
72 | 63 | cnmetdval 13696 |
. . . . . . . . . . . . 13
                     
                              |
73 | 69, 71, 72 | syl2anc 411 |
. . . . . . . . . . . 12
     
 

    
           
     
 
                                       |
74 | | fvco3 5583 |
. . . . . . . . . . . . . . 15
     
                 |
75 | 53, 54, 74 | syl2anc 411 |
. . . . . . . . . . . . . 14
     
 

    
           
     
 
                  |
76 | 75 | oveq2d 5885 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
                              |
77 | 76 | fveq2d 5515 |
. . . . . . . . . . . 12
     
 

    
           
     
 
                                      |
78 | 75, 71 | eqeltrd 2254 |
. . . . . . . . . . . . 13
     
 

    
           
     
 
          |
79 | 69, 78 | abssubd 11186 |
. . . . . . . . . . . 12
     
 

    
           
     
 
                                    |
80 | 73, 77, 79 | 3eqtr2d 2216 |
. . . . . . . . . . 11
     
 

    
           
     
 
                                     |
81 | 80 | breq1d 4010 |
. . . . . . . . . 10
     
 

    
           
     
 
         
         
                   |
82 | 56, 68, 81 | 3imtr3d 202 |
. . . . . . . . 9
     
 

    
           
     
 
                                |
83 | 82 | imim2d 54 |
. . . . . . . 8
     
 

    
           
     
 
     #                     #       
                    |
84 | 83 | ralimdva 2544 |
. . . . . . 7
     
                  
     
 

 
  #                      #                            |
85 | 84 | reximdva 2579 |
. . . . . 6
   

                                #       
          
    #       
                    |
86 | 45, 85 | mpd 13 |
. . . . 5
   

                               #                           |
87 | 86 | rexlimdva2 2597 |
. . . 4
 

 

    
           
     
     #                            |
88 | 87 | ralimdva 2544 |
. . 3
                             
    #       
                    |
89 | 29, 88 | mpd 13 |
. 2
   
  #                           |
90 | | fco 5377 |
. . . 4
                   |
91 | 11, 33, 90 | syl2anc 411 |
. . 3
         |
92 | 91, 39, 40 | ellimc3ap 13797 |
. 2
         lim
           #       
                     |
93 | 16, 89, 92 | mpbir2and 944 |
1
        lim    |