Step | Hyp | Ref
| Expression |
1 | | limccl 22842 |
. . . . . . . . . . . . 13
 
    lim   |
2 | | limclner.r |
. . . . . . . . . . . . 13
  
    lim    |
3 | 1, 2 | sseldi 3398 |
. . . . . . . . . . . 12
   |
4 | 3 | ad2antrr 737 |
. . . . . . . . . . 11
    
                      
  |
5 | | limccl 22842 |
. . . . . . . . . . . . 13
 
    lim   |
6 | | limclner.l |
. . . . . . . . . . . . 13
  
    lim    |
7 | 5, 6 | sseldi 3398 |
. . . . . . . . . . . 12
   |
8 | 7 | ad2antrr 737 |
. . . . . . . . . . 11
    
                      
  |
9 | 4, 8 | subcld 9973 |
. . . . . . . . . 10
    
                           |
10 | | limclner.lner |
. . . . . . . . . . . . 13
   |
11 | 10 | necomd 2679 |
. . . . . . . . . . . 12
   |
12 | 11 | ad2antrr 737 |
. . . . . . . . . . 11
    
                         |
13 | 4, 8, 12 | subne0d 9982 |
. . . . . . . . . 10
    
                           |
14 | 9, 13 | absrpcld 13521 |
. . . . . . . . 9
    
                          
    |
15 | | 4re 10675 |
. . . . . . . . . . 11
 |
16 | | 4pos 10694 |
. . . . . . . . . . 11
 |
17 | 15, 16 | elrpii 11295 |
. . . . . . . . . 10
 |
18 | 17 | a1i 11 |
. . . . . . . . 9
    
                         |
19 | 14, 18 | rpdivcld 11348 |
. . . . . . . 8
    
                           
     |
20 | | nfv 1765 |
. . . . . . . . . . 11
     |
21 | | nfra1 2766 |
. . . . . . . . . . 11
    
                     |
22 | 20, 21 | nfan 2016 |
. . . . . . . . . 10
   
   
                      |
23 | | nfv 1765 |
. . . . . . . . . 10
            
           
      |
24 | 22, 23 | nfim 2008 |
. . . . . . . . 9
                             
     
  


                   |
25 | | ovex 6304 |
. . . . . . . . 9
         |
26 | | eleq1 2518 |
. . . . . . . . . . 11
        
            |
27 | | oveq2 6284 |
. . . . . . . . . . . . 13
        
       
      |
28 | 27 | breq2d 4386 |
. . . . . . . . . . . 12
        
            
 
             |
29 | 28 | 2rexbidv 2878 |
. . . . . . . . . . 11
        
 

         
           
       |
30 | 26, 29 | imbi12d 326 |
. . . . . . . . . 10
        
   
        
     
  


                    |
31 | 30 | imbi2d 322 |
. . . . . . . . 9
        
   
   
                    



         
  
 
                                 
           
         |
32 | | simpll 765 |
. . . . . . . . . . 11
   
   
                     
    |
33 | | simpr 467 |
. . . . . . . . . . 11
   
   
                     
  |
34 | | rspa 2755 |
. . . . . . . . . . . 12
    
                                             |
35 | 34 | adantll 725 |
. . . . . . . . . . 11
   
   
                     
                        |
36 | | limclner.f |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
37 | | fresin 5735 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
               |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
                 |
39 | | inss2 3621 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         |
40 | | ioosscn 37632 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    |
41 | 39, 40 | sstri 3409 |
. . . . . . . . . . . . . . . . . . . . . . 23
      |
42 | 41 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
        |
43 | | limclner.j |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
44 | | retop 21793 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     |
45 | 43, 44 | eqeltri 2526 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
46 | | ioossre 11686 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
    |
47 | 39, 46 | sstri 3409 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      |
48 | | uniretop 21794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      |
49 | 43 | unieqi 4177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       |
50 | 48, 49 | eqtr4i 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  |
51 | 50 | lpss 20169 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  
            
       |
52 | 45, 47, 51 | mp2an 683 |
. . . . . . . . . . . . . . . . . . . . . . . 24
       
    
 |
53 | | limclner.blp1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
        
       |
54 | 52, 53 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
55 | 54 | recnd 9656 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
56 | 38, 42, 55 | ellimc3 22846 |
. . . . . . . . . . . . . . . . . . . . 21
        lim 
                                       |
57 | 6, 56 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . 20
            
      
     
             |
58 | 57 | simprd 469 |
. . . . . . . . . . . . . . . . . . 19
           
      
     
            |
59 | 58 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . 18
 

         
      
     
            |
60 | 59 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . 17
    
                    
         
      
     
            |
61 | | simp11l 1120 |
. . . . . . . . . . . . . . . . . . . . 21
   


                             
      
     
          
  |
62 | | simp12 1040 |
. . . . . . . . . . . . . . . . . . . . 21
   


                             
      
     
          
  |
63 | | simp2 1010 |
. . . . . . . . . . . . . . . . . . . . 21
   


                             
      
     
          
  |
64 | | ifcl 3891 |
. . . . . . . . . . . . . . . . . . . . . . . 24
          |
65 | 64 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
        |
66 | | inss1 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                             |
67 | 66 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                       
       |
68 | | limclner.k |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  ℂfld |
69 | 68 | cnfldtop 21815 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   |
71 | | ax-resscn 9583 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28

  |
73 | 47 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
        |
74 | | unicntop 37367 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   ℂfld |
75 | 68 | unieqi 4177 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
    ℂfld |
76 | 74, 75 | eqtr4i 2477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
  |
77 | 68 | tgioo2 21832 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     ↾t   |
78 | 43, 77 | eqtri 2474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

↾t   |
79 | 76, 78 | restlp 20210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
       
                      |
80 | 70, 72, 73, 79 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
        
                      |
81 | 68 | eqcomi 2461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
  ℂfld  |
82 | 81 | fveq2i 5851 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     ℂfld      |
83 | 82 | fveq1i 5849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
      ℂfld                       |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       ℂfld                        |
85 | 67, 80, 84 | 3sstr4d 3443 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        
           ℂfld           |
86 | 85, 53 | sseldd 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       ℂfld           |
87 | 42, 55 | islpcn 37761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        ℂfld         
                    |
88 | 86, 87 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                     |
89 | 88 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . . . . . . . 23
 
                     |
90 | | breq2 4378 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
            
              |
91 | 90 | rexbidv 2873 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                 |
92 | 91 | rspcva 3116 |
. . . . . . . . . . . . . . . . . . . . . . 23
                          
                 
     |
93 | 65, 89, 92 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                   
     |
94 | | eldifi 3523 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                 |
95 | 47, 94 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
96 | 72 | sselda 3400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  |
97 | 55 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 

  |
98 | 96, 97 | subcld 9973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 

    |
99 | 98 | abscld 13509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

        |
100 | 99 | 3ad2antl1 1171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
         |
101 | 100 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                      |
102 | 65 | rpred 11331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
        |
103 | 102 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                     |
104 | | rpre 11298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

  |
105 | 104 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
106 | 105 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                |
107 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                     
     |
108 | | rpre 11298 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30

  |
109 | | min1 11473 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
        |
110 | 104, 108,
109 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
  |
111 | 110 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
        |
112 | 111 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                  
  |
113 | 101, 103,
106, 107, 112 | ltletrd 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                      |
114 | 108 | adantl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     |
115 | 114 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
116 | 115 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                |
117 | | min2 11474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
 
        |
118 | 104, 108,
117 | syl2an 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       
  |
119 | 118 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
        |
120 | 119 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
                  
  |
121 | 101, 103,
116, 107, 120 | ltletrd 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
                      |
122 | 113, 121 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   
                              |
123 | 122 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
         
                    |
124 | 95, 123 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
   
                  
                    |
125 | 124 | reximdva 2839 |
. . . . . . . . . . . . . . . . . . . . . 22
 
                       
                            |
126 | 93, 125 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . 21
 
                            |
127 | 61, 62, 63, 126 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . 20
   


                             
      
     
          
                           |
128 | | nfv 1765 |
. . . . . . . . . . . . . . . . . . . . 21
     

                             
      
     
            |
129 | | nfre1 2827 |
. . . . . . . . . . . . . . . . . . . . 21
                          |
130 | | inss1 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
      |
131 | 130, 94 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            |
132 | 131 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

                             
      
     
                                     |
133 | | simp113 1140 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

                             
      
     
                                     
      
             |
134 | | eldifsni 4067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
            |
135 | 134 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                            |
136 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                                  |
137 | 135, 136 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                          
         |
138 | 137 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

                             
      
     
                                   
         |
139 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 
   |
140 | | oveq1 6283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
       |
141 | 140 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
142 | 141 | breq1d 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
         |
143 | 139, 142 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     |
144 | | fveq2 5848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
           |
145 | 144 | oveq1d 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
146 | 145 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                       |
147 | 146 | breq1d 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             |
148 | 143, 147 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      
                                  |
149 | 148 | rspcva 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                       
                      |
150 | 149 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
      
                                 |
151 | 132, 133,
138, 150 | syl21anc 1270 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

                             
      
     
                                               |
152 | 94 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

                             
      
     
                                          |
153 | 61 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

                             
      
     
                                     |
154 | | simp13 1041 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

                             
      
     
                                                                     |
155 | | nfv 1765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   |
156 | | nfra1 2766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
  
                                |
157 | 155, 156 | nfan 2016 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
        
      
     
            |
158 | | elinel2 3588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
     
     |
159 | | fvres 5862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
                   |
160 | 158, 159 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
     
               |
161 | 160 | eqcomd 2458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
     
               |
162 | 161 | oveq1d 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
     
                   |
163 | 162 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
     
                           |
164 | 163 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   

                                    
       
                           |
165 | | rspa 2755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                                 

      
      
     
            |
166 | 165 | 3impia 1207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                                 

                              |
167 | 166 | 3adant1l 1263 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   

                                    
       
     
           |
168 | 164, 167 | eqbrtrd 4395 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   

                                    
       
            |
169 | 168 | 3exp 1209 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
        
      
     
          
                             |
170 | 157, 169 | ralrimi 2781 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
        
      
     
          
        
      
             |
171 | 153, 154,
170 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

                             
      
     
                                                                |
172 | 134 | anim1i 576 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                            |
173 | 172 | adantrl 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                          
         |
174 | 173 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     

                             
      
     
                                   
         |
175 | 141 | breq1d 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
       
         |
176 | 139, 175 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                     |
177 | 144 | oveq1d 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
               |
178 | 177 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                       |
179 | 178 | breq1d 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
           
             |
180 | 176, 179 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   
      
                                  |
181 | 180 | rspcva 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                  
                      |
182 | 181 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                                                         |
183 | 152, 171,
174, 182 | syl21anc 1270 |
. . . . . . . . . . . . . . . . . . . . . . 23
     

                             
      
     
                                               |
184 | | rspe 2825 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                  |
185 | 132, 151,
183, 184 | syl12anc 1269 |
. . . . . . . . . . . . . . . . . . . . . 22
     

                             
      
     
                                                            |
186 | 185 | 3exp 1209 |
. . . . . . . . . . . . . . . . . . . . 21
   


                             
      
     
          
                         
                          |
187 | 128, 129,
186 | rexlimd 2847 |
. . . . . . . . . . . . . . . . . . . 20
   


                             
      
     
          
 
                        
                         |
188 | 127, 187 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
   


                             
      
     
          

          
             |
189 | 188 | 3exp 1209 |
. . . . . . . . . . . . . . . . . 18
    
                    

 

                              
                          |
190 | 189 | rexlimdv 2851 |
. . . . . . . . . . . . . . . . 17
    
                    
 
        
      
     
                                    |
191 | 60, 190 | mpd 15 |
. . . . . . . . . . . . . . . 16
    
                    

          
             |
192 | 191 | 3exp 1209 |
. . . . . . . . . . . . . . 15
 


 
                                               |
193 | 192 | rexlimdv 2851 |
. . . . . . . . . . . . . 14
 

 

                                              |
194 | 193 | imp 435 |
. . . . . . . . . . . . 13
    

                    

          
             |
195 | 194 | adantllr 730 |
. . . . . . . . . . . 12
   

                       

          
             |
196 | | fresin 5735 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     
               |
197 | 36, 196 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                 |
198 | | inss2 3621 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
         |
199 | | ioosscn 37632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
    |
200 | 198, 199 | sstri 3409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
      |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
        |
202 | 197, 201,
55 | ellimc3 22846 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        lim 
           
      
                    |
203 | 2, 202 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
            
      
                   |
204 | 203 | simprd 469 |
. . . . . . . . . . . . . . . . . . . . . . 23
           
      
                  |
205 | 204 | r19.21bi 2757 |
. . . . . . . . . . . . . . . . . . . . . 22
 

         
      
                  |
206 | 205 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . . . . . 21
    
                    
         
      
                  |
207 | | simp11l 1120 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                             
      
                
  |
208 | | simp12 1040 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                             
      
                
  |
209 | | simp2 1010 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
   


                             
      
                
  |
210 | | inss1 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                             |
211 | 210 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                               |
212 | | ioossre 11686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
    |
213 | 198, 212 | sstri 3409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
      |
214 | 213 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
        |
215 | 76, 78 | restlp 20210 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                                      |
216 | 70, 72, 214, 215 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                               |
217 | 82 | fveq1i 5849 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
      ℂfld                       |
218 | 217 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
       ℂfld                        |
219 | 211, 216,
218 | 3sstr4d 3443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
                    ℂfld           |
220 | | limclner.blp2 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
        
       |
221 | 219, 220 | sseldd 3401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
       ℂfld           |
222 | 201, 55 | islpcn 37761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
        ℂfld        
       
             |
223 | 221, 222 | mpbid 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
                     |
224 | 223 | 3ad2ant1 1030 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 
                     |
225 | | breq2 4378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
            
              |
226 | 225 | rexbidv 2873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
             
                            
      |
227 | 226 | rspcva 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                                            
     |
228 | 65, 224, 227 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                   
     |
229 | | eldifi 3523 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                 |
230 | 213, 229 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            |
231 | 72 | sselda 3400 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

  |
232 | 55 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
 

  |
233 | 231, 232 | subcld 9973 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 

    |
234 | 233 | abscld 13509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
 

        |
235 | 234 | 3ad2antl1 1171 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
   
         |
236 | 235 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                      |
237 | 102 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                     |
238 | 105 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                |
239 | | simpr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                     
     |
240 | 111 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                  
  |
241 | 236, 237,
238, 239, 240 | ltletrd 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
                      |
242 | 115 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                |
243 | 238, 242,
117 | syl2anc 671 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
   
                  
  |
244 | 236, 237,
242, 239, 243 | ltletrd 9782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
                      |
245 | 241, 244 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
   
                              |
246 | 245 | ex 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
   
         
                    |
247 | 230, 246 | sylan2 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
   
     
            
                    |
248 | 247 | reximdva 2839 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
        
              
      
                     |
249 | 228, 248 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
                            |
250 | 207, 208,
209, 249 | syl3anc 1271 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   


                             
      
                
      
                    |
251 | | nfv 1765 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     

                             
      
                  |
252 | | nfre1 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                          |
253 | | inss1 3620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
      |
254 | 253, 229 | sseldi 3398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
            |
255 | 254 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     

                             
      
                      
                    |
256 | | simp113 1140 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

                             
      
                      
                    
      
             |
257 | | eldifsni 4067 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
            |
258 | 257 | adantr 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
          |
259 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
          
      
                |
260 | 258, 259 | jca 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
          
      
                  |
261 | 260 | 3adant1 1027 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

                             
      
                      
                  
         |
262 | | neeq1 2686 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 
   |
263 | | oveq1 6283 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
       |
264 | 263 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
               |
265 | 264 | breq1d 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
       
         |
266 | 262, 265 | anbi12d 722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
                     |
267 | | fveq2 5848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
           |
268 | 267 | oveq1d 6291 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
               |
269 | 268 | fveq2d 5852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
                       |
270 | 269 | breq1d 4384 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
           
             |
271 | 266, 270 | imbi12d 326 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
   
      
                                  |
272 | 271 | rspcva 3116 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
                       
                      |
273 | 272 | imp 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     
      
                                 |
274 | 255, 256,
261, 273 | syl21anc 1270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
     

                             
      
                      
                              |
275 | 229 | 3ad2ant2 1031 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
     

                             
      
                |