Step | Hyp | Ref
| Expression |
1 | | df-ioo 11414 |
. . . . . . . . . 10




    |
2 | 1 | ixxf 11420 |
. . . . . . . . 9
  
     |
3 | | ffn 5666 |
. . . . . . . . 9
       
    |
4 | 2, 3 | mp1i 12 |
. . . . . . . 8
     

    |
5 | | elssuni 4228 |
. . . . . . . . . . . . . 14
        |
6 | | tpr2rico.0 |
. . . . . . . . . . . . . . . 16
     |
7 | | retop 20471 |
. . . . . . . . . . . . . . . 16
     |
8 | 6, 7 | eqeltri 2538 |
. . . . . . . . . . . . . . 15
 |
9 | | uniretop 20472 |
. . . . . . . . . . . . . . . 16
      |
10 | 6 | unieqi 4207 |
. . . . . . . . . . . . . . . 16
       |
11 | 9, 10 | eqtr4i 2486 |
. . . . . . . . . . . . . . 15
  |
12 | 8, 8, 11, 11 | txunii 19297 |
. . . . . . . . . . . . . 14
      |
13 | 5, 12 | syl6sseqr 3510 |
. . . . . . . . . . . . 13
       |
14 | 13 | ad2antrr 725 |
. . . . . . . . . . . 12
     

    |
15 | | simplr 754 |
. . . . . . . . . . . 12
     

  |
16 | 14, 15 | sseldd 3464 |
. . . . . . . . . . 11
     


   |
17 | | xp1st 6715 |
. . . . . . . . . . 11
  
      |
18 | 16, 17 | syl 16 |
. . . . . . . . . 10
     

      |
19 | | simpr 461 |
. . . . . . . . . . . 12
     

  |
20 | 19 | rpred 11137 |
. . . . . . . . . . 11
     

  |
21 | 20 | rehalfcld 10681 |
. . . . . . . . . 10
     

    |
22 | 18, 21 | resubcld 9886 |
. . . . . . . . 9
     

          |
23 | 22 | rexrd 9543 |
. . . . . . . 8
     

          |
24 | 18, 21 | readdcld 9523 |
. . . . . . . . 9
     

          |
25 | 24 | rexrd 9543 |
. . . . . . . 8
     

          |
26 | | fnovrn 6347 |
. . . . . . . 8
           
                               |
27 | 4, 23, 25, 26 | syl3anc 1219 |
. . . . . . 7
     

                      |
28 | | xp2nd 6716 |
. . . . . . . . . . 11
  
      |
29 | 16, 28 | syl 16 |
. . . . . . . . . 10
     

      |
30 | 29, 21 | resubcld 9886 |
. . . . . . . . 9
     

          |
31 | 30 | rexrd 9543 |
. . . . . . . 8
     

          |
32 | 29, 21 | readdcld 9523 |
. . . . . . . . 9
     

          |
33 | 32 | rexrd 9543 |
. . . . . . . 8
     

          |
34 | | fnovrn 6347 |
. . . . . . . 8
           
                               |
35 | 4, 31, 33, 34 | syl3anc 1219 |
. . . . . . 7
     

                      |
36 | | eqidd 2455 |
. . . . . . 7
     

                                                                                      |
37 | | xpeq1 4961 |
. . . . . . . . 9
                    
                          |
38 | 37 | eqeq2d 2468 |
. . . . . . . 8
                    
                                                                                                                |
39 | | xpeq2 4962 |
. . . . . . . . 9
                    
                                                                  |
40 | 39 | eqeq2d 2468 |
. . . . . . . 8
                    
                                                                
                                                                                       |
41 | 38, 40 | rspc2ev 3186 |
. . . . . . 7
                                                                                                                                                                                 |
42 | 27, 35, 36, 41 | syl3anc 1219 |
. . . . . 6
     

                                                  |
43 | | eqid 2454 |
. . . . . . 7
  
    
   |
44 | | vex 3079 |
. . . . . . . 8
 |
45 | | vex 3079 |
. . . . . . . 8
 |
46 | 44, 45 | xpex 6617 |
. . . . . . 7
   |
47 | 43, 46 | elrnmpt2 6312 |
. . . . . 6
                                           
   
                                                  |
48 | 42, 47 | sylibr 212 |
. . . . 5
     

                                                 |
49 | | tpr2rico.2 |
. . . . 5
      |
50 | 48, 49 | syl6eleqr 2553 |
. . . 4
     

                                            |
51 | 50 | ralrimiva 2829 |
. . 3
   
                                              |
52 | | xpss 5053 |
. . . . . . 7
  
  |
53 | 52, 16 | sseldi 3461 |
. . . . . 6
     


   |
54 | 18 | rexrd 9543 |
. . . . . . . 8
     

      |
55 | 19 | rphalfcld 11149 |
. . . . . . . . 9
     

    |
56 | 18, 55 | ltsubrpd 11165 |
. . . . . . . 8
     

              |
57 | 18, 55 | ltaddrpd 11166 |
. . . . . . . 8
     

              |
58 | | elioo1 11450 |
. . . . . . . . 9
         
                                 
    
                            |
59 | 23, 25, 58 | syl2anc 661 |
. . . . . . . 8
     

                                         
                |
60 | 54, 56, 57, 59 | mpbir3and 1171 |
. . . . . . 7
     

                          |
61 | 29 | rexrd 9543 |
. . . . . . . 8
     

      |
62 | 29, 55 | ltsubrpd 11165 |
. . . . . . . 8
     

              |
63 | 29, 55 | ltaddrpd 11166 |
. . . . . . . 8
     

              |
64 | | elioo1 11450 |
. . . . . . . . 9
         
                                 
    
                            |
65 | 31, 33, 64 | syl2anc 661 |
. . . . . . . 8
     

                                         
                |
66 | 61, 62, 63, 65 | mpbir3and 1171 |
. . . . . . 7
     

                          |
67 | 60, 66 | jca 532 |
. . . . . 6
     

                                                    |
68 | | elxp7 6718 |
. . . . . 6
                                          
                                                        |
69 | 53, 67, 68 | sylanbrc 664 |
. . . . 5
     

                                            |
70 | 69 | ralrimiva 2829 |
. . . 4
   
                                              |
71 | | mnfle 11223 |
. . . . . . . . . . . . . . . . . 18
        
          |
72 | 23, 71 | syl 16 |
. . . . . . . . . . . . . . . . 17
     

          |
73 | | pnfge 11220 |
. . . . . . . . . . . . . . . . . 18
        
          |
74 | 25, 73 | syl 16 |
. . . . . . . . . . . . . . . . 17
     

          |
75 | | mnfxr 11204 |
. . . . . . . . . . . . . . . . . 18
 |
76 | | pnfxr 11202 |
. . . . . . . . . . . . . . . . . 18
 |
77 | | ioossioo 11497 |
. . . . . . . . . . . . . . . . . 18
                                             |
78 | 75, 76, 77 | mpanl12 682 |
. . . . . . . . . . . . . . . . 17

                                         |
79 | 72, 74, 78 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
     

                        |
80 | | ioomax 11480 |
. . . . . . . . . . . . . . . 16
   |
81 | 79, 80 | syl6sseq 3509 |
. . . . . . . . . . . . . . 15
     

                      |
82 | | mnfle 11223 |
. . . . . . . . . . . . . . . . . 18
        
          |
83 | 31, 82 | syl 16 |
. . . . . . . . . . . . . . . . 17
     

          |
84 | | pnfge 11220 |
. . . . . . . . . . . . . . . . . 18
        
          |
85 | 33, 84 | syl 16 |
. . . . . . . . . . . . . . . . 17
     

          |
86 | | ioossioo 11497 |
. . . . . . . . . . . . . . . . . 18
                                             |
87 | 75, 76, 86 | mpanl12 682 |
. . . . . . . . . . . . . . . . 17

                                         |
88 | 83, 85, 87 | syl2anc 661 |
. . . . . . . . . . . . . . . 16
     

                        |
89 | 88, 80 | syl6sseq 3509 |
. . . . . . . . . . . . . . 15
     

                      |
90 | | xpss12 5052 |
. . . . . . . . . . . . . . 15
                     
                                                               
   |
91 | 81, 89, 90 | syl2anc 661 |
. . . . . . . . . . . . . 14
     

                                          
   |
92 | 91 | sselda 3463 |
. . . . . . . . . . . . 13
     
                                                 |
93 | 92 | expcom 435 |
. . . . . . . . . . . 12
                                                       |
94 | 93 | ancld 553 |
. . . . . . . . . . 11
                                                      
        |
95 | 94 | imdistanri 691 |
. . . . . . . . . 10
     
                                                   
                                                 |
96 | 13 | adantr 465 |
. . . . . . . . . . . . . . . 16
    
        |
97 | | simpr1 994 |
. . . . . . . . . . . . . . . 16
    
   
  |
98 | 96, 97 | sseldd 3464 |
. . . . . . . . . . . . . . 15
    
   
    |
99 | 98 | 3anassrs 1210 |
. . . . . . . . . . . . . 14
     
         |
100 | | simpr 461 |
. . . . . . . . . . . . . 14
     
         |
101 | | simplr 754 |
. . . . . . . . . . . . . . 15
     
       |
102 | 101 | rphalfcld 11149 |
. . . . . . . . . . . . . 14
     
         |
103 | | tpr2rico.1 |
. . . . . . . . . . . . . . 15
 


    |
104 | 103 | cnre2csqima 26485 |
. . . . . . . . . . . . . 14
   
                                                                                             |
105 | 99, 100, 102, 104 | syl3anc 1219 |
. . . . . . . . . . . . 13
     
                                                                                             |
106 | | eqid 2454 |
. . . . . . . . . . . . . . . . . . . . 21
  ℂfld   ℂfld |
107 | 103, 6, 106 | cnrehmeo 20656 |
. . . . . . . . . . . . . . . . . . . 20
       ℂfld  |
108 | 106 | cnfldtopon 20493 |
. . . . . . . . . . . . . . . . . . . . . 22
  ℂfld TopOn   |
109 | 108 | toponunii 18668 |
. . . . . . . . . . . . . . . . . . . . 21
   ℂfld |
110 | 12, 109 | hmeof1o 19468 |
. . . . . . . . . . . . . . . . . . . 20
        ℂfld         |
111 | | f1of 5748 |
. . . . . . . . . . . . . . . . . . . 20
      
        |
112 | 107, 110,
111 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
       |
113 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
     
             |
114 | 113, 99 | ffvelrnd 5952 |
. . . . . . . . . . . . . . . . 17
     
           |
115 | 112 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
     

        |
116 | 115 | ffvelrnda 5951 |
. . . . . . . . . . . . . . . . 17
     
           |
117 | | sqsscirc2 26483 |
. . . . . . . . . . . . . . . . 17
                                  
                    
                 |
118 | 114, 116,
101, 117 | syl21anc 1218 |
. . . . . . . . . . . . . . . 16
     
                                                                 |
119 | 118 | imp 429 |
. . . . . . . . . . . . . . 15
                                                                       |
120 | 101 | rpxrd 11138 |
. . . . . . . . . . . . . . . . . 18
     
       |
121 | 120 | adantr 465 |
. . . . . . . . . . . . . . . . 17
                          
  |
122 | | cnxmet 20483 |
. . . . . . . . . . . . . . . . 17

      |
123 | 121, 122 | jctil 537 |
. . . . . . . . . . . . . . . 16
                          
      
   |
124 | 114 | adantr 465 |
. . . . . . . . . . . . . . . . 17
                          
      |
125 | 116 | adantr 465 |
. . . . . . . . . . . . . . . . 17
                          
      |
126 | 124, 125 | jca 532 |
. . . . . . . . . . . . . . . 16
                          
            |
127 | | eqid 2454 |
. . . . . . . . . . . . . . . . . . 19

  |
128 | 127 | cnmetdval 20481 |
. . . . . . . . . . . . . . . . . 18
                 
                      |
129 | 125, 124,
128 | syl2anc 661 |
. . . . . . . . . . . . . . . . 17
                          
      
                      |
130 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
                          
                |
131 | 129, 130 | eqbrtrd 4419 |
. . . . . . . . . . . . . . . 16
                          
      
        |
132 | | elbl3 20098 |
. . . . . . . . . . . . . . . . 17
   
                                  
      
         |
133 | 132 | biimpar 485 |
. . . . . . . . . . . . . . . 16
    
                       
     
                    |
134 | 123, 126,
131, 133 | syl21anc 1218 |
. . . . . . . . . . . . . . 15
                          
                   |
135 | 119, 134 | syldan 470 |
. . . . . . . . . . . . . 14
                                                                          |
136 | 135 | ex 434 |
. . . . . . . . . . . . 13
     
                                                                    |
137 | 105, 136 | syld 44 |
. . . . . . . . . . . 12
     
                                                                    |
138 | | f1ocnv 5760 |
. . . . . . . . . . . . . . 15
      
         |
139 | 107, 110,
138 | mp2b 10 |
. . . . . . . . . . . . . 14
        |
140 | | f1ofun 5750 |
. . . . . . . . . . . . . 14
       
   |
141 | 139, 140 | ax-mp 5 |
. . . . . . . . . . . . 13
  |
142 | | f1odm 5752 |
. . . . . . . . . . . . . . 15
       
   |
143 | 139, 142 | ax-mp 5 |
. . . . . . . . . . . . . 14

 |
144 | 116, 143 | syl6eleqr 2553 |
. . . . . . . . . . . . 13
     
            |
145 | | funfvima 6060 |
. . . . . . . . . . . . 13
        
                                                |
146 | 141, 144,
145 | sylancr 663 |
. . . . . . . . . . . 12
     
                                                     |
147 | 107, 110 | mp1i 12 |
. . . . . . . . . . . . . . 15
     
             |
148 | | f1ocnvfv1 6091 |
. . . . . . . . . . . . . . 15
       
              |
149 | 147, 100,
148 | syl2anc 661 |
. . . . . . . . . . . . . 14
     
                |
150 | 149 | eleq1d 2523 |
. . . . . . . . . . . . 13
     
                                
                     |
151 | 150 | biimpd 207 |
. . . . . . . . . . . 12
     
                                
                     |
152 | 137, 146,
151 | 3syld 55 |
. . . . . . . . . . 11
     
                                               
                     |
153 | 152 | imp 429 |
. . . . . . . . . 10
                                                                           |
154 | 95, 153 | syl 16 |
. . . . . . . . 9
     
                                                                 |
155 | 154 | ex 434 |
. . . . . . . 8
     

                                          
                     |
156 | 155 | ssrdv 3469 |
. . . . . . 7
     

                                                              |
157 | 156 | ralrimiva 2829 |
. . . . . 6
   
                                                                |
158 | 103 | mpt2fun 6301 |
. . . . . . . . . 10
 |
159 | 158 | a1i 11 |
. . . . . . . . 9
   
   |
160 | 13 | sselda 3463 |
. . . . . . . . . 10
   
     |
161 | | f1odm 5752 |
. . . . . . . . . . 11
      
    |
162 | 107, 110,
161 | mp2b 10 |
. . . . . . . . . 10
   |
163 | 160, 162 | syl6eleqr 2553 |
. . . . . . . . 9
   
   |
164 | | simpr 461 |
. . . . . . . . 9
   
   |
165 | | funfvima 6060 |
. . . . . . . . . 10
               |
166 | 165 | imp 429 |
. . . . . . . . 9
  
 
          |
167 | 159, 163,
164, 166 | syl21anc 1218 |
. . . . . . . 8
   
           |
168 | | hmeoima 19469 |
. . . . . . . . . . 11
         ℂfld          ℂfld  |
169 | 107, 168 | mpan 670 |
. . . . . . . . . 10
         ℂfld  |
170 | 106 | cnfldtopn 20492 |
. . . . . . . . . . . . 13
  ℂfld       |
171 | 170 | elmopn2 20151 |
. . . . . . . . . . . 12
      
       ℂfld
                             |
172 | 122, 171 | ax-mp 5 |
. . . . . . . . . . 11
       ℂfld
                            |
173 | 172 | simprbi 464 |
. . . . . . . . . 10
       ℂfld
                      |
174 | 169, 173 | syl 16 |
. . . . . . . . 9
                         |
175 | 174 | adantr 465 |
. . . . . . . 8
   
                       |
176 | | oveq1 6206 |
. . . . . . . . . . 11
                             |
177 | 176 | sseq1d 3490 |
. . . . . . . . . 10
                  
            
       |
178 | 177 | rexbidv 2864 |
. . . . . . . . 9
      
            
             
       |
179 | 178 | rspcva 3175 |
. . . . . . . 8
                                                   |
180 | 167, 175,
179 | syl2anc 661 |
. . . . . . 7
   
                     |
181 | | imass2 5311 |
. . . . . . . . . 10
                                   
           |
182 | | f1of1 5747 |
. . . . . . . . . . . . 13
      
        |
183 | 107, 110,
182 | mp2b 10 |
. . . . . . . . . . . 12
       |
184 | | f1imacnv 5764 |
. . . . . . . . . . . 12
       
              |
185 | 183, 13, 184 | sylancr 663 |
. . . . . . . . . . 11
              |
186 | 185 | sseq2d 3491 |
. . . . . . . . . 10
                     
        
                     |
187 | 181, 186 | syl5ib 219 |
. . . . . . . . 9
                                          |
188 | 187 | reximdv 2931 |
. . . . . . . 8
    
                 
                     |
189 | 188 | adantr 465 |
. . . . . . 7
   
                                      
   |
190 | 180, 189 | mpd 15 |
. . . . . 6
   
                      |
191 | | r19.29 2961 |
. . . . . 6
                                                                                                                                                                      |
192 | 157, 190,
191 | syl2anc 661 |
. . . . 5
   
                                                                                    |
193 | | sstr 3471 |
. . . . . 6
                                                                                                                             |
194 | 193 | reximi 2927 |
. . . . 5
                                                                                                                               |
195 | 192, 194 | syl 16 |
. . . 4
   
                                              |
196 | | r19.29 2961 |
. . . 4
                                                                                        
                                                                                         |
197 | 70, 195, 196 | syl2anc 661 |
. . 3
   
  
                                                                                       |
198 | | r19.29 2961 |
. . 3
                                                                                                                                     
                                                                                                                                    |
199 | 51, 197, 198 | syl2anc 661 |
. 2
   
                                                                                                                                      |
200 | | eleq2 2527 |
. . . . 5
                                                                                         |
201 | | sseq1 3484 |
. . . . 5
                                                                                         |
202 | 200, 201 | anbi12d 710 |
. . . 4
                                             
                                                                                         |
203 | 202 | rspcev 3177 |
. . 3
                                                                                                                                   

   |
204 | 203 | rexlimivw 2941 |
. 2
                                                                                                                                    

   |
205 | 199, 204 | syl 16 |
1
   
  
   |