Step | Hyp | Ref
| Expression |
1 | | ellimc3.f |
. . 3
       |
2 | | ellimc3.a |
. . 3

  |
3 | | ellimc3.b |
. . 3
   |
4 | | eqid 2471 |
. . 3
  ℂfld   ℂfld |
5 | 1, 2, 3, 4 | ellimc2 22911 |
. 2
   lim      ℂfld 
   ℂfld                  |
6 | | cnxmet 21871 |
. . . . . . . . . 10

      |
7 | 6 | a1i 11 |
. . . . . . . . 9
             |
8 | | simplr 770 |
. . . . . . . . 9
       |
9 | | simpr 468 |
. . . . . . . . 9
       |
10 | | blcntr 21506 |
. . . . . . . . 9
  
    
            |
11 | 7, 8, 9, 10 | syl3anc 1292 |
. . . . . . . 8
                |
12 | | rpxr 11332 |
. . . . . . . . . . 11

  |
13 | 12 | adantl 473 |
. . . . . . . . . 10
       |
14 | 4 | cnfldtopn 21880 |
. . . . . . . . . . 11
  ℂfld       |
15 | 14 | blopn 21593 |
. . . . . . . . . 10
  
    
            ℂfld  |
16 | 7, 8, 13, 15 | syl3anc 1292 |
. . . . . . . . 9
                ℂfld  |
17 | | eleq2 2538 |
. . . . . . . . . . 11
         

            |
18 | | sseq2 3440 |
. . . . . . . . . . . . 13
         
          
                      |
19 | 18 | anbi2d 718 |
. . . . . . . . . . . 12
         
 
         
           
             |
20 | 19 | rexbidv 2892 |
. . . . . . . . . . 11
         
 
  ℂfld            
   ℂfld                         |
21 | 17, 20 | imbi12d 327 |
. . . . . . . . . 10
         
 
   ℂfld             
             ℂfld                          |
22 | 21 | rspcv 3132 |
. . . . . . . . 9
            ℂfld
 
  ℂfld     ℂfld                           ℂfld                          |
23 | 16, 22 | syl 17 |
. . . . . . . 8
      
  ℂfld 
   ℂfld                           ℂfld                          |
24 | 11, 23 | mpid 41 |
. . . . . . 7
      
  ℂfld 
   ℂfld                 ℂfld                         |
25 | 14 | mopni2 21586 |
. . . . . . . . . . 11
  
    
  ℂfld

         
  |
26 | 6, 25 | mp3an1 1377 |
. . . . . . . . . 10
    ℂfld

         
  |
27 | | ssrin 3648 |
. . . . . . . . . . . . 13
                         
       |
28 | | imass2 5210 |
. . . . . . . . . . . . 13
                                        
            |
29 | | sstr2 3425 |
. . . . . . . . . . . . 13
                             
                   
                               |
30 | 27, 28, 29 | 3syl 18 |
. . . . . . . . . . . 12
                                                             |
31 | 30 | com12 31 |
. . . . . . . . . . 11
          
        
                            
            |
32 | 31 | reximdv 2857 |
. . . . . . . . . 10
          
        
 
                                         |
33 | 26, 32 | syl5com 30 |
. . . . . . . . 9
    ℂfld

                   
                                |
34 | 33 | impr 631 |
. . . . . . . 8
    ℂfld                                                      |
35 | 34 | rexlimiva 2868 |
. . . . . . 7
    ℂfld                      
                              |
36 | 24, 35 | syl6 33 |
. . . . . 6
      
  ℂfld 
   ℂfld                                              |
37 | 36 | ralrimdva 2812 |
. . . . 5
 

 
  ℂfld     ℂfld                                               |
38 | 14 | mopni2 21586 |
. . . . . . . . . 10
  
    
  ℂfld

         
  |
39 | 6, 38 | mp3an1 1377 |
. . . . . . . . 9
    ℂfld

         
  |
40 | | r19.29r 2913 |
. . . . . . . . . . 11
                                           
          
                               |
41 | 6 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   


 
       |
42 | 3 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . 17
   


   |
43 | | simpr 468 |
. . . . . . . . . . . . . . . . . 18
   


   |
44 | 43 | rpxrd 11365 |
. . . . . . . . . . . . . . . . 17
   


   |
45 | 14 | blopn 21593 |
. . . . . . . . . . . . . . . . 17
  
    
            ℂfld  |
46 | 41, 42, 44, 45 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
   


            ℂfld  |
47 | | blcntr 21506 |
. . . . . . . . . . . . . . . . 17
  
    
            |
48 | 41, 42, 43, 47 | syl3anc 1292 |
. . . . . . . . . . . . . . . 16
   


            |
49 | | eleq2 2538 |
. . . . . . . . . . . . . . . . . . 19
         

            |
50 | | ineq1 3618 |
. . . . . . . . . . . . . . . . . . . . 21
         
                       |
51 | 50 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . . . . 20
         
                               |
52 | 51 | sseq1d 3445 |
. . . . . . . . . . . . . . . . . . 19
         
                                                   |
53 | 49, 52 | anbi12d 725 |
. . . . . . . . . . . . . . . . . 18
         
 
         
         
                                          |
54 | 53 | rspcev 3136 |
. . . . . . . . . . . . . . . . 17
             ℂfld

                                          ℂfld                        |
55 | 54 | expr 626 |
. . . . . . . . . . . . . . . 16
             ℂfld
         
                                ℂfld                         |
56 | 46, 48, 55 | syl2anc 673 |
. . . . . . . . . . . . . . 15
   


                                 ℂfld                         |
57 | 56 | rexlimdva 2871 |
. . . . . . . . . . . . . 14
      
                               ℂfld                         |
58 | | sstr2 3425 |
. . . . . . . . . . . . . . . . 17
          
        
             
         |
59 | 58 | com12 31 |
. . . . . . . . . . . . . . . 16
                                           |
60 | 59 | anim2d 575 |
. . . . . . . . . . . . . . 15
                                
         
    |
61 | 60 | reximdv 2857 |
. . . . . . . . . . . . . 14
              ℂfld                         ℂfld                |
62 | 57, 61 | syl9 72 |
. . . . . . . . . . . . 13
                
                               ℂfld                 |
63 | 62 | impd 438 |
. . . . . . . . . . . 12
               
                              
  ℂfld                |
64 | 63 | rexlimdva 2871 |
. . . . . . . . . . 11
 

            
                             
  ℂfld                |
65 | 40, 64 | syl5 32 |
. . . . . . . . . 10
 

                                           
  ℂfld                |
66 | 65 | expd 443 |
. . . . . . . . 9
 

                                             ℂfld                 |
67 | 39, 66 | syl5 32 |
. . . . . . . 8
 

    ℂfld

 
                                ℂfld                 |
68 | 67 | expdimp 444 |
. . . . . . 7
      ℂfld 
                                  ℂfld                 |
69 | 68 | com23 80 |
. . . . . 6
      ℂfld  
                             
   ℂfld                 |
70 | 69 | ralrimdva 2812 |
. . . . 5
 

 
                                ℂfld 
   ℂfld                 |
71 | 37, 70 | impbid 195 |
. . . 4
 

 
  ℂfld     ℂfld              
                                |
72 | 1 | ad2antrr 740 |
. . . . . . . . . 10
             |
73 | | ffun 5742 |
. . . . . . . . . 10
       |
74 | 72, 73 | syl 17 |
. . . . . . . . 9
         |
75 | | inss2 3644 |
. . . . . . . . . 10
                    |
76 | | difss 3549 |
. . . . . . . . . . 11
   
 |
77 | | fdm 5745 |
. . . . . . . . . . . 12
       |
78 | 72, 77 | syl 17 |
. . . . . . . . . . 11
         |
79 | 76, 78 | syl5sseqr 3467 |
. . . . . . . . . 10
             |
80 | 75, 79 | syl5ss 3429 |
. . . . . . . . 9
                        |
81 | | funimass4 5930 |
. . . . . . . . 9
                
                             
                                 |
82 | 74, 80, 81 | syl2anc 673 |
. . . . . . . 8
                                   
                                 |
83 | 6 | a1i 11 |
. . . . . . . . . . . . 13
   
   

    
       |
84 | | simplrr 779 |
. . . . . . . . . . . . . 14
   
   

      |
85 | 84 | rpxrd 11365 |
. . . . . . . . . . . . 13
   
   

      |
86 | 3 | ad3antrrr 744 |
. . . . . . . . . . . . 13
   
   

   
  |
87 | 76, 2 | syl5ss 3429 |
. . . . . . . . . . . . . . 15
       |
88 | 87 | ad2antrr 740 |
. . . . . . . . . . . . . 14
             |
89 | 88 | sselda 3418 |
. . . . . . . . . . . . 13
   
   

      |
90 | | elbl3 21485 |
. . . . . . . . . . . . 13
   
                  
  
     |
91 | 83, 85, 86, 89, 90 | syl22anc 1293 |
. . . . . . . . . . . 12
   
   

             
  
     |
92 | | eqid 2471 |
. . . . . . . . . . . . . . 15

  |
93 | 92 | cnmetdval 21869 |
. . . . . . . . . . . . . 14
 
   
          |
94 | 89, 86, 93 | syl2anc 673 |
. . . . . . . . . . . . 13
   
   

      
          |
95 | 94 | breq1d 4405 |
. . . . . . . . . . . 12
   
   

                   |
96 | 91, 95 | bitrd 261 |
. . . . . . . . . . 11
   
   

             
         |
97 | | simplrl 778 |
. . . . . . . . . . . . . 14
   
   

   
  |
98 | 97 | rpxrd 11365 |
. . . . . . . . . . . . 13
   
   

   
  |
99 | | simpllr 777 |
. . . . . . . . . . . . 13
   
   

   
  |
100 | | eldifi 3544 |
. . . . . . . . . . . . . 14
       |
101 | | ffvelrn 6035 |
. . . . . . . . . . . . . 14
     
       |
102 | 72, 100, 101 | syl2an 485 |
. . . . . . . . . . . . 13
   
   

          |
103 | | elbl3 21485 |
. . . . . . . . . . . . 13
   
                          
      
     |
104 | 83, 98, 99, 102, 103 | syl22anc 1293 |
. . . . . . . . . . . 12
   
   

                 
      
     |
105 | 92 | cnmetdval 21869 |
. . . . . . . . . . . . . 14
     
       
              |
106 | 102, 99, 105 | syl2anc 673 |
. . . . . . . . . . . . 13
   
   

          
              |
107 | 106 | breq1d 4405 |
. . . . . . . . . . . 12
   
   

                           |
108 | 104, 107 | bitrd 261 |
. . . . . . . . . . 11
   
   

                 
             |
109 | 96, 108 | imbi12d 327 |
. . . . . . . . . 10
   
   

                            
      
              |
110 | 109 | ralbidva 2828 |
. . . . . . . . 9
                       
             
                           |
111 | | elin 3608 |
. . . . . . . . . . . . 13
               
                 |
112 | | ancom 457 |
. . . . . . . . . . . . 13
               
                 |
113 | 111, 112 | bitri 257 |
. . . . . . . . . . . 12
               
                 |
114 | 113 | imbi1i 332 |
. . . . . . . . . . 11
                                    
                          |
115 | | impexp 453 |
. . . . . . . . . . 11
                
             
                                |
116 | 114, 115 | bitr2i 258 |
. . . . . . . . . 10
     
                                                         |
117 | 116 | ralbii2 2821 |
. . . . . . . . 9
 
                                                             |
118 | | impexp 453 |
. . . . . . . . . . 11
  

      
           

                       |
119 | | eldifsn 4088 |
. . . . . . . . . . . 12
    

   |
120 | 119 | imbi1i 332 |
. . . . . . . . . . 11
     
      
           
                        |
121 | | impexp 453 |
. . . . . . . . . . . 12
                                           |
122 | 121 | imbi2i 319 |
. . . . . . . . . . 11
   
      
           

                       |
123 | 118, 120,
122 | 3bitr4i 285 |
. . . . . . . . . 10
     
      
           

                       |
124 | 123 | ralbii2 2821 |
. . . . . . . . 9
 
                       
 
      
             |
125 | 110, 117,
124 | 3bitr3g 295 |
. . . . . . . 8
                                      
 
      
              |
126 | 82, 125 | bitrd 261 |
. . . . . . 7
                                   

                       |
127 | 126 | anassrs 660 |
. . . . . 6
   


                             

                       |
128 | 127 | rexbidva 2889 |
. . . . 5
      
                           
                         |
129 | 128 | ralbidva 2828 |
. . . 4
 

 
                            
    
      
              |
130 | 71, 129 | bitrd 261 |
. . 3
 

 
  ℂfld     ℂfld              
                         |
131 | 130 | pm5.32da 653 |
. 2
      ℂfld 
   ℂfld                    
      
               |
132 | 5, 131 | bitrd 261 |
1
   lim     
                        |