Step | Hyp | Ref
| Expression |
1 | | limcrecl.4 |
. . 3
  lim    |
2 | 1 | adantr 467 |
. 2
 
  lim    |
3 | | limccl 22830 |
. . . . . . . . . 10
 lim   |
4 | 3, 1 | sseldi 3430 |
. . . . . . . . 9
   |
5 | 4 | adantr 467 |
. . . . . . . 8
 
   |
6 | | simpr 463 |
. . . . . . . 8
 

  |
7 | 5, 6 | eldifd 3415 |
. . . . . . 7
 
     |
8 | 7 | dstregt0 37491 |
. . . . . 6
 
           |
9 | | cnxmet 21793 |
. . . . . . . . . . . . . 14

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

  |
12 | 11 | ad4antr 738 |
. . . . . . . . . . . . . 14
                  |
13 | 12 | ssdifssd 3571 |
. . . . . . . . . . . . 13
                      |
14 | | limcrecl.3 |
. . . . . . . . . . . . . . 15
       ℂfld      |
15 | | eqid 2451 |
. . . . . . . . . . . . . . . . . 18
  ℂfld   ℂfld |
16 | 15 | cnfldtop 21804 |
. . . . . . . . . . . . . . . . 17
  ℂfld  |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . . . 16
   ℂfld
  |
18 | | unicntop 37371 |
. . . . . . . . . . . . . . . . 17
   ℂfld |
19 | 11, 18 | syl6sseq 3478 |
. . . . . . . . . . . . . . . 16

   ℂfld  |
20 | | eqid 2451 |
. . . . . . . . . . . . . . . . 17
   ℂfld    ℂfld |
21 | 20 | lpdifsn 20159 |
. . . . . . . . . . . . . . . 16
    ℂfld
   ℂfld 
      ℂfld   
      ℂfld           |
22 | 17, 19, 21 | syl2anc 667 |
. . . . . . . . . . . . . . 15
        ℂfld   
      ℂfld           |
23 | 14, 22 | mpbid 214 |
. . . . . . . . . . . . . 14
       ℂfld          |
24 | 23 | ad4antr 738 |
. . . . . . . . . . . . 13
                      ℂfld          |
25 | | simpr 463 |
. . . . . . . . . . . . 13
                  |
26 | 15 | cnfldtopn 21802 |
. . . . . . . . . . . . . 14
  ℂfld       |
27 | 26 | lpbl 21518 |
. . . . . . . . . . . . 13
   
               ℂfld        
 
                |
28 | 10, 13, 24, 25, 27 | syl31anc 1271 |
. . . . . . . . . . . 12
                                 |
29 | | eldif 3414 |
. . . . . . . . . . . . . . 15
    

     |
30 | 29 | anbi1i 701 |
. . . . . . . . . . . . . 14
     
         
 
               |
31 | | anass 655 |
. . . . . . . . . . . . . 14
                                 |
32 | 30, 31 | bitri 253 |
. . . . . . . . . . . . 13
     
         


               |
33 | 32 | rexbii2 2887 |
. . . . . . . . . . . 12
               


              |
34 | 28, 33 | sylib 200 |
. . . . . . . . . . 11
                 
              |
35 | | simprl 764 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
            
    |
36 | | elsn 3982 |
. . . . . . . . . . . . . . . . . 18
     |
37 | 36 | necon3bbii 2671 |
. . . . . . . . . . . . . . . . 17
     |
38 | 35, 37 | sylib 200 |
. . . . . . . . . . . . . . . 16
     
  
   
    
               |
39 | | simp-5l 778 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
               |
40 | | simplr 762 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
               |
41 | | simprr 766 |
. . . . . . . . . . . . . . . . 17
     
  
   
    
                        |
42 | | simp3 1010 |
. . . . . . . . . . . . . . . . . . . . 21
 
                     |
43 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
 
          
       |
44 | 18 | lpss 20158 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    ℂfld
       ℂfld   
  |
45 | 17, 11, 44 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       ℂfld   
  |
46 | 45, 14 | sseldd 3433 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
47 | 46 | 3ad2ant1 1029 |
. . . . . . . . . . . . . . . . . . . . . 22
 
         
  |
48 | | rpxr 11309 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
49 | 48 | 3ad2ant2 1030 |
. . . . . . . . . . . . . . . . . . . . . 22
 
            |
50 | | elbl 21403 |
. . . . . . . . . . . . . . . . . . . . . 22
  
    
          
          |
51 | 43, 47, 49, 50 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . 21
 
                   
          |
52 | 42, 51 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . 20
 
             
 
   |
53 | 52 | simpld 461 |
. . . . . . . . . . . . . . . . . . 19
 
            |
54 | 53, 47 | abssubd 13515 |
. . . . . . . . . . . . . . . . . 18
 
                        |
55 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . . 21

  |
56 | 55 | cnmetdval 21791 |
. . . . . . . . . . . . . . . . . . . 20
 
   
          |
57 | 47, 53, 56 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
 
            
          |
58 | 52 | simprd 465 |
. . . . . . . . . . . . . . . . . . 19
 
            
 
  |
59 | 57, 58 | eqbrtrrd 4425 |
. . . . . . . . . . . . . . . . . 18
 
             
 
  |
60 | 54, 59 | eqbrtrd 4423 |
. . . . . . . . . . . . . . . . 17
 
                  |
61 | 39, 40, 41, 60 | syl3anc 1268 |
. . . . . . . . . . . . . . . 16
     
  
   
    
                     |
62 | 38, 61 | jca 535 |
. . . . . . . . . . . . . . 15
     
  
   
    
             
         |
63 | 62 | adantlr 721 |
. . . . . . . . . . . . . 14
      

     
     
             
         |
64 | 39 | adantlr 721 |
. . . . . . . . . . . . . . . 16
      

     
     
               |
65 | | simplr 762 |
. . . . . . . . . . . . . . . 16
      

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

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

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

     
     
                 
    |
69 | | rpre 11308 |
. . . . . . . . . . . . . . . . 17

  |
70 | 69 | ad2antlr 733 |
. . . . . . . . . . . . . . . 16
   

     
     |
71 | | limcrecl.1 |
. . . . . . . . . . . . . . . . . . . . 21
       |
72 | 71 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
73 | 72 | recnd 9669 |
. . . . . . . . . . . . . . . . . . 19
 
       |
74 | 73 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . 18
   

     
         |
75 | 4 | ad3antrrr 736 |
. . . . . . . . . . . . . . . . . 18
   

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

     
           |
77 | 76 | abscld 13498 |
. . . . . . . . . . . . . . . 16
   

     
               |
78 | 72 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
    
   
         |
79 | | nfv 1761 |
. . . . . . . . . . . . . . . . . . . . 21
   |
80 | | nfra1 2769 |
. . . . . . . . . . . . . . . . . . . . 21
  
   
   |
81 | 79, 80 | nfan 2011 |
. . . . . . . . . . . . . . . . . . . 20
  
         |
82 | | rspa 2755 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 

   
    |
83 | 82 | adantll 720 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   
       
    |
84 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

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

  |
87 | 86 | sselda 3432 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

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

              |
89 | 88 | adantlr 721 |
. . . . . . . . . . . . . . . . . . . . . 22
   
   
                  |
90 | 83, 89 | breqtrd 4427 |
. . . . . . . . . . . . . . . . . . . . 21
   
   
            |
91 | 90 | ex 436 |
. . . . . . . . . . . . . . . . . . . 20
 
        
         |
92 | 81, 91 | ralrimi 2788 |
. . . . . . . . . . . . . . . . . . 19
 
                 |
93 | 92 | adantlr 721 |
. . . . . . . . . . . . . . . . . 18
    
   
            |
94 | | oveq1 6297 |
. . . . . . . . . . . . . . . . . . . . 21
               |
95 | 94 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . . . 20
                       |
96 | 95 | breq2d 4414 |
. . . . . . . . . . . . . . . . . . 19
     
     
             |
97 | 96 | rspcv 3146 |
. . . . . . . . . . . . . . . . . 18
      
     
             |
98 | 78, 93, 97 | sylc 62 |
. . . . . . . . . . . . . . . . 17
    
   
               |
99 | 98 | adantlr 721 |
. . . . . . . . . . . . . . . 16
   

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

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

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

     
     
            
                      |
103 | 102 | ex 436 |
. . . . . . . . . . . 12
     
  
   
        
           
      
              |
104 | 103 | reximdva 2862 |
. . . . . . . . . . 11
                 

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

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

                      |
108 | 107 | nrexdv 2843 |
. . . . . . . 8
   
         
                        |
109 | 108 | ex 436 |
. . . . . . 7
  

                                  |
110 | 109 | reximdva 2862 |
. . . . . 6
 
  
       


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

                      
                      |
113 | 111, 112 | sylib 200 |
. . . 4
 
                          |
114 | 113 | intnand 927 |
. . 3
 
 
  
                       |
115 | 71, 86 | fssd 5738 |
. . . . 5
       |
116 | 115, 11, 46 | ellimc3 22834 |
. . . 4
   lim     
                        |
117 | 116 | adantr 467 |
. . 3
 
 
 lim 
     
      
               |
118 | 114, 117 | mtbird 303 |
. 2
 

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