Step | Hyp | Ref
| Expression |
1 | | eqid 2453 |
. . . . 5
  ℂfld   ℂfld |
2 | 1 | cnfldtop 21816 |
. . . 4
  ℂfld  |
3 | 2 | a1i 11 |
. . 3
   ℂfld
  |
4 | | islpcn.s |
. . 3

  |
5 | | islpcn.p |
. . 3
   |
6 | | unicntop 37381 |
. . . 4
   ℂfld |
7 | 6 | islp2 20173 |
. . 3
    ℂfld
 
      ℂfld           ℂfld                |
8 | 3, 4, 5, 7 | syl3anc 1269 |
. 2
        ℂfld           ℂfld                |
9 | | cnxmet 21805 |
. . . . . . . . . . 11

      |
10 | 9 | a1i 11 |
. . . . . . . . . 10
 

        |
11 | 5 | adantr 467 |
. . . . . . . . . 10
 

  |
12 | | simpr 463 |
. . . . . . . . . 10
 

  |
13 | 1 | cnfldtopn 21814 |
. . . . . . . . . . 11
  ℂfld       |
14 | 13 | blnei 21529 |
. . . . . . . . . 10
  
    
                ℂfld        |
15 | 10, 11, 12, 14 | syl3anc 1269 |
. . . . . . . . 9
 

               ℂfld        |
16 | 15 | adantlr 722 |
. . . . . . . 8
   
      ℂfld                              ℂfld        |
17 | | simplr 763 |
. . . . . . . 8
   
      ℂfld                      ℂfld               |
18 | | ineq1 3629 |
. . . . . . . . . 10
         
                       |
19 | 18 | neeq1d 2685 |
. . . . . . . . 9
         
 
    
                  |
20 | 19 | rspcva 3150 |
. . . . . . . 8
                 ℂfld      
      ℂfld                               |
21 | 16, 17, 20 | syl2anc 667 |
. . . . . . 7
   
      ℂfld                                |
22 | | n0 3743 |
. . . . . . 7
                                  |
23 | 21, 22 | sylib 200 |
. . . . . 6
   
      ℂfld               
                 |
24 | | elinel2 3622 |
. . . . . . . . . . 11
                      |
25 | 24 | adantl 468 |
. . . . . . . . . 10
                   
      |
26 | 4 | adantr 467 |
. . . . . . . . . . . . . . 15
 
                  |
27 | 24 | eldifad 3418 |
. . . . . . . . . . . . . . . 16
                  |
28 | 27 | adantl 468 |
. . . . . . . . . . . . . . 15
 
               
  |
29 | 26, 28 | sseldd 3435 |
. . . . . . . . . . . . . 14
 
               
  |
30 | 5 | adantr 467 |
. . . . . . . . . . . . . 14
 
               
  |
31 | 29, 30 | abssubd 13527 |
. . . . . . . . . . . . 13
 
                              |
32 | | eqid 2453 |
. . . . . . . . . . . . . . 15

  |
33 | 32 | cnmetdval 21803 |
. . . . . . . . . . . . . 14
 
   
          |
34 | 30, 29, 33 | syl2anc 667 |
. . . . . . . . . . . . 13
 
                  
          |
35 | 31, 34 | eqtr4d 2490 |
. . . . . . . . . . . 12
 
                             |
36 | 35 | adantlr 722 |
. . . . . . . . . . 11
                                 |
37 | | elinel1 3621 |
. . . . . . . . . . . . . 14
                           |
38 | 37 | adantl 468 |
. . . . . . . . . . . . 13
                   
           |
39 | 9 | a1i 11 |
. . . . . . . . . . . . . 14
                    
       |
40 | 11 | adantr 467 |
. . . . . . . . . . . . . 14
                   
  |
41 | | rpxr 11316 |
. . . . . . . . . . . . . . 15

  |
42 | 41 | ad2antlr 734 |
. . . . . . . . . . . . . 14
                      |
43 | | elbl 21415 |
. . . . . . . . . . . . . 14
  
    
          
          |
44 | 39, 40, 42, 43 | syl3anc 1269 |
. . . . . . . . . . . . 13
                             
          |
45 | 38, 44 | mpbid 214 |
. . . . . . . . . . . 12
                       
 
   |
46 | 45 | simprd 465 |
. . . . . . . . . . 11
                      
 
  |
47 | 36, 46 | eqbrtrd 4426 |
. . . . . . . . . 10
                            |
48 | 25, 47 | jca 535 |
. . . . . . . . 9
                                  |
49 | 48 | ex 436 |
. . . . . . . 8
 

                    
          |
50 | 49 | adantlr 722 |
. . . . . . 7
   
      ℂfld                                   
          |
51 | 50 | eximdv 1766 |
. . . . . 6
   
      ℂfld                
                                |
52 | 23, 51 | mpd 15 |
. . . . 5
   
      ℂfld                               |
53 | | df-rex 2745 |
. . . . 5
            
                |
54 | 52, 53 | sylibr 216 |
. . . 4
   
      ℂfld                             |
55 | 54 | ralrimiva 2804 |
. . 3
 
       ℂfld                             |
56 | 9 | a1i 11 |
. . . . . . . 8
 
       |
57 | 13 | neibl 21528 |
. . . . . . . 8
  
    
        ℂfld     
          
    |
58 | 56, 5, 57 | syl2anc 667 |
. . . . . . 7
        ℂfld     
          
    |
59 | 58 | simplbda 630 |
. . . . . 6
 
      ℂfld       
           |
60 | 59 | adantlr 722 |
. . . . 5
   
            
      ℂfld       
           |
61 | | nfv 1763 |
. . . . . . . 8
   |
62 | | nfra1 2771 |
. . . . . . . 8
                |
63 | 61, 62 | nfan 2013 |
. . . . . . 7
   
              |
64 | | nfv 1763 |
. . . . . . 7
       ℂfld       |
65 | 63, 64 | nfan 2013 |
. . . . . 6
                 
      ℂfld        |
66 | | nfv 1763 |
. . . . . 6
         |
67 | | simp1l 1033 |
. . . . . . . . . 10
   
            
        
   |
68 | | simp2 1010 |
. . . . . . . . . 10
   
            
        
   |
69 | 67, 68 | jca 535 |
. . . . . . . . 9
   
            
        
     |
70 | | rspa 2757 |
. . . . . . . . . . 11
              
 
             |
71 | 70 | adantll 721 |
. . . . . . . . . 10
   
            

              |
72 | 71 | 3adant3 1029 |
. . . . . . . . 9
   
            
        
               |
73 | | simp3 1011 |
. . . . . . . . 9
   
            
        
            |
74 | 53 | biimpi 198 |
. . . . . . . . . . . 12
                             |
75 | 74 | ad2antlr 734 |
. . . . . . . . . . 11
   
                      
                 |
76 | | nfv 1763 |
. . . . . . . . . . . . . 14
  
  |
77 | | nfre1 2850 |
. . . . . . . . . . . . . 14
  
            |
78 | 76, 77 | nfan 2013 |
. . . . . . . . . . . . 13
   
               |
79 | | nfv 1763 |
. . . . . . . . . . . . 13
            |
80 | 78, 79 | nfan 2013 |
. . . . . . . . . . . 12
                  
        
  |
81 | | simplr 763 |
. . . . . . . . . . . . . . . 16
   
          
                        |
82 | 4 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
 

      |
83 | | eldifi 3557 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
  |
84 | 83 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
 

   
  |
85 | 82, 84 | sseldd 3435 |
. . . . . . . . . . . . . . . . . . . . 21
 

   
  |
86 | 85 | adantrr 724 |
. . . . . . . . . . . . . . . . . . . 20
 
            
  |
87 | 5 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

   
  |
88 | 87, 85, 33 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

      
          |
89 | 87, 85 | abssubd 13527 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

       
          |
90 | 88, 89 | eqtrd 2487 |
. . . . . . . . . . . . . . . . . . . . . 22
 

      
          |
91 | 90 | adantrr 724 |
. . . . . . . . . . . . . . . . . . . . 21
 
               
          |
92 | | simprr 767 |
. . . . . . . . . . . . . . . . . . . . 21
 
                     |
93 | 91, 92 | eqbrtrd 4426 |
. . . . . . . . . . . . . . . . . . . 20
 
               
 
  |
94 | 86, 93 | jca 535 |
. . . . . . . . . . . . . . . . . . 19
 
                
 
   |
95 | 94 | adantlr 722 |
. . . . . . . . . . . . . . . . . 18
        
                 |
96 | 9 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
        
                |
97 | 11 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
        
          |
98 | 41 | ad2antlr 734 |
. . . . . . . . . . . . . . . . . . 19
        
          |
99 | 96, 97, 98, 43 | syl3anc 1269 |
. . . . . . . . . . . . . . . . . 18
        
                 
          |
100 | 95, 99 | mpbird 236 |
. . . . . . . . . . . . . . . . 17
        
                   |
101 | 100 | adantlr 722 |
. . . . . . . . . . . . . . . 16
   
          
            
           |
102 | 81, 101 | sseldd 3435 |
. . . . . . . . . . . . . . 15
   
          
            
  |
103 | | simprl 765 |
. . . . . . . . . . . . . . 15
   
          
            
      |
104 | 102, 103 | elind 3620 |
. . . . . . . . . . . . . 14
   
          
            
        |
105 | 104 | ex 436 |
. . . . . . . . . . . . 13
             
     
      

        |
106 | 105 | adantlr 722 |
. . . . . . . . . . . 12
   
                      
                       |
107 | 80, 106 | eximd 1962 |
. . . . . . . . . . 11
   
                      
        
      

         |
108 | 75, 107 | mpd 15 |
. . . . . . . . . 10
   
                      
          |
109 | | n0 3743 |
. . . . . . . . . 10
      

        |
110 | 108, 109 | sylibr 216 |
. . . . . . . . 9
   
                      
         |
111 | 69, 72, 73, 110 | syl21anc 1268 |
. . . . . . . 8
   
            
        
         |
112 | 111 | 3exp 1208 |
. . . . . . 7
 
             

                    |
113 | 112 | adantr 467 |
. . . . . 6
   
            
      ℂfld                 
          |
114 | 65, 66, 113 | rexlimd 2873 |
. . . . 5
   
            
      ℂfld                  
        |
115 | 60, 114 | mpd 15 |
. . . 4
   
            
      ℂfld               |
116 | 115 | ralrimiva 2804 |
. . 3
 
             
       ℂfld               |
117 | 55, 116 | impbida 844 |
. 2
         ℂfld                             |
118 | 8, 117 | bitrd 257 |
1
        ℂfld                    |