Step | Hyp | Ref
| Expression |
1 | | limcrecl.4 |
. . 3
  lim    |
2 | 1 | adantr 472 |
. 2
 
  lim    |
3 | | limccl 22909 |
. . . . . . . . . 10
 lim   |
4 | 3, 1 | sseldi 3416 |
. . . . . . . . 9
   |
5 | 4 | adantr 472 |
. . . . . . . 8
 
   |
6 | | simpr 468 |
. . . . . . . 8
 

  |
7 | 5, 6 | eldifd 3401 |
. . . . . . 7
 
     |
8 | 7 | dstregt0 37581 |
. . . . . 6
 
           |
9 | | cnxmet 21871 |
. . . . . . . . . . . . . 14

      |
10 | 9 | a1i 11 |
. . . . . . . . . . . . 13
                
       |
11 | | limcrecl.2 |
. . . . . . . . . . . . . . 15

  |
12 | 11 | ad4antr 746 |
. . . . . . . . . . . . . 14
                  |
13 | 12 | ssdifssd 3560 |
. . . . . . . . . . . . 13
                      |
14 | | limcrecl.3 |
. . . . . . . . . . . . . . 15
       ℂfld      |
15 | | eqid 2471 |
. . . . . . . . . . . . . . . . . 18
  ℂfld   ℂfld |
16 | 15 | cnfldtop 21882 |
. . . . . . . . . . . . . . . . 17
  ℂfld  |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
   ℂfld
  |
18 | | unicntop 37433 |
. . . . . . . . . . . . . . . . 17
   ℂfld |
19 | 11, 18 | syl6sseq 3464 |
. . . . . . . . . . . . . . . 16

   ℂfld  |
20 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
   ℂfld    ℂfld |
21 | 20 | lpdifsn 20236 |
. . . . . . . . . . . . . . . 16
    ℂfld
   ℂfld 
      ℂfld   
      ℂfld           |
22 | 17, 19, 21 | syl2anc 673 |
. . . . . . . . . . . . . . 15
        ℂfld   
      ℂfld           |
23 | 14, 22 | mpbid 215 |
. . . . . . . . . . . . . 14
       ℂfld          |
24 | 23 | ad4antr 746 |
. . . . . . . . . . . . 13
                      ℂfld          |
25 | | simpr 468 |
. . . . . . . . . . . . 13
                  |
26 | 15 | cnfldtopn 21880 |
. . . . . . . . . . . . . 14
  ℂfld       |
27 | 26 | lpbl 21596 |
. . . . . . . . . . . . 13
   
               ℂfld        
 
                |
28 | 10, 13, 24, 25, 27 | syl31anc 1295 |
. . . . . . . . . . . 12
                                 |
29 | | eldif 3400 |
. . . . . . . . . . . . . . 15
    

     |
30 | 29 | anbi1i 709 |
. . . . . . . . . . . . . 14
     
         
 
               |
31 | | anass 661 |
. . . . . . . . . . . . . 14
                                 |
32 | 30, 31 | bitri 257 |
. . . . . . . . . . . . 13
     
         


               |
33 | 32 | rexbii2 2879 |
. . . . . . . . . . . 12
               


              |
34 | 28, 33 | sylib 201 |
. . . . . . . . . . 11
                 
              |
35 | | simprl 772 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
            
    |
36 | | elsn 3973 |
. . . . . . . . . . . . . . . . . 18
     |
37 | 36 | necon3bbii 2690 |
. . . . . . . . . . . . . . . . 17
     |
38 | 35, 37 | sylib 201 |
. . . . . . . . . . . . . . . 16
     
  
   
    
               |
39 | | simp-5l 786 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
               |
40 | | simplr 770 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
               |
41 | | simprr 774 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
                        |
42 | | simp3 1032 |
. . . . . . . . . . . . . . . . . . . . 21
 
                     |
43 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
          
       |
44 | 18 | lpss 20235 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ℂfld
       ℂfld   
  |
45 | 17, 11, 44 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       ℂfld   
  |
46 | 45, 14 | sseldd 3419 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
47 | 46 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         
  |
48 | | rpxr 11332 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
49 | 48 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . . . . 22
 
            |
50 | | elbl 21481 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    
          
          |
51 | 43, 47, 49, 50 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   
          |
52 | 42, 51 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
 
             
 
   |
53 | 52 | simpld 466 |
. . . . . . . . . . . . . . . . . . 19
 
            |
54 | 53, 47 | abssubd 13592 |
. . . . . . . . . . . . . . . . . 18
 
                        |
55 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . . 21

  |
56 | 55 | cnmetdval 21869 |
. . . . . . . . . . . . . . . . . . . 20
 
   
          |
57 | 47, 53, 56 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . 19
 
            
          |
58 | 52 | simprd 470 |
. . . . . . . . . . . . . . . . . . 19
 
            
 
  |
59 | 57, 58 | eqbrtrrd 4418 |
. . . . . . . . . . . . . . . . . 18
 
             
 
  |
60 | 54, 59 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . 17
 
                  |
61 | 39, 40, 41, 60 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
     
  
   
    
                     |
62 | 38, 61 | jca 541 |
. . . . . . . . . . . . . . 15
     
  
   
    
             
         |
63 | 62 | adantlr 729 |
. . . . . . . . . . . . . 14
      

     
     
             
         |
64 | 39 | adantlr 729 |
. . . . . . . . . . . . . . . 16
      

     
     
               |
65 | | simplr 770 |
. . . . . . . . . . . . . . . 16
      

     
     
               |
66 | 64, 65 | jca 541 |
. . . . . . . . . . . . . . 15
      

     
     
             
   |
67 | | simp-5r 787 |
. . . . . . . . . . . . . . 15
      

     
     
               |
68 | | simp-4r 785 |
. . . . . . . . . . . . . . 15
      

     
     
                 
    |
69 | | rpre 11331 |
. . . . . . . . . . . . . . . . 17

  |
70 | 69 | ad2antlr 741 |
. . . . . . . . . . . . . . . 16
   

     
     |
71 | | limcrecl.1 |
. . . . . . . . . . . . . . . . . . . . 21
       |
72 | 71 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
73 | 72 | recnd 9687 |
. . . . . . . . . . . . . . . . . . 19
 
       |
74 | 73 | ad2antrr 740 |
. . . . . . . . . . . . . . . . . 18
   

     
         |
75 | 4 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
   

     
     |
76 | 74, 75 | subcld 10005 |
. . . . . . . . . . . . . . . . 17
   

     
           |
77 | 76 | abscld 13575 |
. . . . . . . . . . . . . . . 16
   

     
               |
78 | 72 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
    
   
         |
79 | | nfv 1769 |
. . . . . . . . . . . . . . . . . . . . 21
   |
80 | | nfra1 2785 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
   |
81 | 79, 80 | nfan 2031 |
. . . . . . . . . . . . . . . . . . . 20
  
         |
82 | | rspa 2774 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 

   
    |
83 | 82 | adantll 728 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   
       
    |
84 | 4 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
85 | | ax-resscn 9614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25

  |
87 | 86 | sselda 3418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

  |
88 | 84, 87 | abssubd 13592 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

              |
89 | 88 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   
                  |
90 | 83, 89 | breqtrd 4420 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
            |
91 | 90 | ex 441 |
. . . . . . . . . . . . . . . . . . . 20
 
        
         |
92 | 81, 91 | ralrimi 2800 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
93 | 92 | adantlr 729 |
. . . . . . . . . . . . . . . . . 18
    
   
            |
94 | | oveq1 6315 |
. . . . . . . . . . . . . . . . . . . . 21
               |
95 | 94 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . 20
                       |
96 | 95 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . 19
     
     
             |
97 | 96 | rspcv 3132 |
. . . . . . . . . . . . . . . . . 18
      
     
             |
98 | 78, 93, 97 | sylc 61 |
. . . . . . . . . . . . . . . . 17
    
   
               |
99 | 98 | adantlr 729 |
. . . . . . . . . . . . . . . 16
   

     
               |
100 | 70, 77, 99 | ltnsymd 9801 |
. . . . . . . . . . . . . . 15
   

     
               |
101 | 66, 67, 68, 100 | syl21anc 1291 |
. . . . . . . . . . . . . 14
      

     
     
            
            |
102 | 63, 101 | jcn 37431 |
. . . . . . . . . . . . 13
      

     
     
            
                      |
103 | 102 | ex 441 |
. . . . . . . . . . . 12
     
  
   
        
           
      
              |
104 | 103 | reximdva 2858 |
. . . . . . . . . . 11
                 

            
 
      
              |
105 | 34, 104 | mpd 15 |
. . . . . . . . . 10
                  
      
             |
106 | | rexnal 2836 |
. . . . . . . . . 10
   
      
          

                      |
107 | 105, 106 | sylib 201 |
. . . . . . . . 9
               

                      |
108 | 107 | nrexdv 2842 |
. . . . . . . 8
   
         
                        |
109 | 108 | ex 441 |
. . . . . . 7
  

                                  |
110 | 109 | reximdva 2858 |
. . . . . 6
 
  
       


                       |
111 | 8, 110 | mpd 15 |
. . . . 5
 
                          |
112 | | rexnal 2836 |
. . . . 5
  

                      
                      |
113 | 111, 112 | sylib 201 |
. . . 4
 
                          |
114 | 113 | intnand 930 |
. . 3
 
 
  
                       |
115 | 71, 86 | fssd 5750 |
. . . . 5
       |
116 | 115, 11, 46 | ellimc3 22913 |
. . . 4
   lim     
                        |
117 | 116 | adantr 472 |
. . 3
 
 
 lim 
     
      
               |
118 | 114, 117 | mtbird 308 |
. 2
 

 lim    |
119 | 2, 118 | condan 811 |
1
   |