Proof of Theorem ubthlem2
Step | Hyp | Ref
| Expression |
1 | | ubthlem.10 |
. . . . . 6
   |
2 | 1 | nnrpd 11368 |
. . . . 5
   |
3 | 2, 2 | rpaddcld 11385 |
. . . 4
     |
4 | | ubthlem.12 |
. . . 4
   |
5 | 3, 4 | rpdivcld 11387 |
. . 3
       |
6 | 5 | rpred 11370 |
. 2
       |
7 | | ubthlem.13 |
. . . . . . . . . 10
             |
8 | | rabss 3518 |
. . . . . . . . . 10
     
                  |
9 | 7, 8 | sylib 201 |
. . . . . . . . 9
              |
10 | 9 | ad2antrr 737 |
. . . . . . . 8
     
            |
11 | | ubthlem.5 |
. . . . . . . . . . 11
 |
12 | | bnnv 26557 |
. . . . . . . . . . 11

  |
13 | 11, 12 | ax-mp 5 |
. . . . . . . . . 10
 |
14 | 13 | a1i 11 |
. . . . . . . . 9
       |
15 | | ubthlem.11 |
. . . . . . . . . 10
   |
16 | 15 | ad2antrr 737 |
. . . . . . . . 9
       |
17 | 4 | ad2antrr 737 |
. . . . . . . . . . 11
       |
18 | 17 | rpcnd 11372 |
. . . . . . . . . 10
       |
19 | | simpr 467 |
. . . . . . . . . 10
       |
20 | | ubth.1 |
. . . . . . . . . . 11
     |
21 | | eqid 2462 |
. . . . . . . . . . 11
           |
22 | 20, 21 | nvscl 26296 |
. . . . . . . . . 10
              |
23 | 14, 18, 19, 22 | syl3anc 1276 |
. . . . . . . . 9
                |
24 | | eqid 2462 |
. . . . . . . . . 10
         |
25 | 20, 24 | nvgcl 26288 |
. . . . . . . . 9
 
                             |
26 | 14, 16, 23, 25 | syl3anc 1276 |
. . . . . . . 8
                        |
27 | | oveq2 6323 |
. . . . . . . . . . 11
                                             |
28 | 27 | breq1d 4426 |
. . . . . . . . . 10
                                           
   |
29 | | eleq1 2528 |
. . . . . . . . . 10
                                               |
30 | 28, 29 | imbi12d 326 |
. . . . . . . . 9
                                                                            |
31 | 30 | rspccv 3159 |
. . . . . . . 8
 
    
                      
                                               |
32 | 10, 26, 31 | sylc 62 |
. . . . . . 7
                                                   |
33 | | ubthlem.3 |
. . . . . . . . . . . . . . . 16
     |
34 | 20, 33 | cbncms 26556 |
. . . . . . . . . . . . . . 15

      |
35 | 11, 34 | ax-mp 5 |
. . . . . . . . . . . . . 14
     |
36 | | cmetmet 22305 |
. . . . . . . . . . . . . 14
    
      |
37 | | metxmet 21398 |
. . . . . . . . . . . . . 14
    
       |
38 | 35, 36, 37 | mp2b 10 |
. . . . . . . . . . . . 13
      |
39 | 38 | a1i 11 |
. . . . . . . . . . . 12
            |
40 | | xmetsym 21411 |
. . . . . . . . . . . 12
                                                                     |
41 | 39, 16, 26, 40 | syl3anc 1276 |
. . . . . . . . . . 11
                                                 |
42 | | eqid 2462 |
. . . . . . . . . . . . 13
         |
43 | | eqid 2462 |
. . . . . . . . . . . . 13
 CV   CV   |
44 | 20, 42, 43, 33 | imsdval 26367 |
. . . . . . . . . . . 12
                  
                        CV                                |
45 | 14, 26, 16, 44 | syl3anc 1276 |
. . . . . . . . . . 11
                            CV                                |
46 | 20, 24, 42 | nvpncan2 26326 |
. . . . . . . . . . . . 13
 
                                              |
47 | 14, 16, 23, 46 | syl3anc 1276 |
. . . . . . . . . . . 12
                                         |
48 | 47 | fveq2d 5892 |
. . . . . . . . . . 11
       CV                                CV                |
49 | 41, 45, 48 | 3eqtrd 2500 |
. . . . . . . . . 10
                            CV                |
50 | 17 | rprege0d 11377 |
. . . . . . . . . . 11
     
   |
51 | 20, 21, 43 | nvsge0 26341 |
. . . . . . . . . . 11
  
    CV                 CV        |
52 | 14, 50, 19, 51 | syl3anc 1276 |
. . . . . . . . . 10
       CV                 CV        |
53 | 49, 52 | eqtrd 2496 |
. . . . . . . . 9
                             CV        |
54 | 18 | mulid1d 9686 |
. . . . . . . . . 10
     
   |
55 | 54 | eqcomd 2468 |
. . . . . . . . 9
         |
56 | 53, 55 | breq12d 4429 |
. . . . . . . 8
                              CV           |
57 | 20, 43 | nvcl 26337 |
. . . . . . . . . . 11
     CV       |
58 | 13, 57 | mpan 681 |
. . . . . . . . . 10
   CV       |
59 | 58 | adantl 472 |
. . . . . . . . 9
       CV       |
60 | | 1red 9684 |
. . . . . . . . 9
       |
61 | 59, 60, 17 | lemul2d 11411 |
. . . . . . . 8
        CV        CV     
     |
62 | 56, 61 | bitr4d 264 |
. . . . . . 7
                             CV        |
63 | | breq2 4420 |
. . . . . . . . . . . . . 14
         
           |
64 | 63 | ralbidv 2839 |
. . . . . . . . . . . . 13
  
       

           |
65 | 64 | rabbidv 3048 |
. . . . . . . . . . . 12
  
          
           |
66 | | ubthlem.9 |
. . . . . . . . . . . 12
              |
67 | | fvex 5898 |
. . . . . . . . . . . . . 14
     |
68 | 20, 67 | eqeltri 2536 |
. . . . . . . . . . . . 13
 |
69 | 68 | rabex 4568 |
. . . . . . . . . . . 12
 
        
 |
70 | 65, 66, 69 | fvmpt 5971 |
. . . . . . . . . . 11
                  |
71 | 1, 70 | syl 17 |
. . . . . . . . . 10
      
           |
72 | 71 | eleq2d 2525 |
. . . . . . . . 9
                                                      |
73 | | fveq2 5888 |
. . . . . . . . . . . . 13
                                             |
74 | 73 | fveq2d 5892 |
. . . . . . . . . . . 12
                                                     |
75 | 74 | breq1d 4426 |
. . . . . . . . . . 11
                                                   
   |
76 | 75 | ralbidv 2839 |
. . . . . . . . . 10
                                                     
   |
77 | 76 | elrab 3208 |
. . . . . . . . 9
                   
        
                  
                            |
78 | 72, 77 | syl6bb 269 |
. . . . . . . 8
                                         
                             |
79 | 78 | ad2antrr 737 |
. . . . . . 7
                          
                                           
    |
80 | 32, 62, 79 | 3imtr3d 275 |
. . . . . 6
        CV    
                                           
    |
81 | | rsp 2766 |
. . . . . . . . . 10
 
                         
                            |
82 | 81 | com12 32 |
. . . . . . . . 9
  
                        
                        
   |
83 | 82 | ad2antlr 738 |
. . . . . . . 8
      
                        
                        
   |
84 | | xmet0 21406 |
. . . . . . . . . . . . . . . . . . . 20
       
      |
85 | 38, 15, 84 | sylancr 674 |
. . . . . . . . . . . . . . . . . . 19
       |
86 | 4 | rpge0d 11374 |
. . . . . . . . . . . . . . . . . . 19

  |
87 | 85, 86 | eqbrtrd 4437 |
. . . . . . . . . . . . . . . . . 18
    
  |
88 | | oveq2 6323 |
. . . . . . . . . . . . . . . . . . . 20
           |
89 | 88 | breq1d 4426 |
. . . . . . . . . . . . . . . . . . 19
     
       |
90 | 89 | elrab 3208 |
. . . . . . . . . . . . . . . . . 18
      
        |
91 | 15, 87, 90 | sylanbrc 675 |
. . . . . . . . . . . . . . . . 17
         |
92 | 7, 91 | sseldd 3445 |
. . . . . . . . . . . . . . . 16
       |
93 | 92, 71 | eleqtrd 2542 |
. . . . . . . . . . . . . . 15
  
           |
94 | | fveq2 5888 |
. . . . . . . . . . . . . . . . . . 19
           |
95 | 94 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
                   |
96 | 95 | breq1d 4426 |
. . . . . . . . . . . . . . . . 17
         
           |
97 | 96 | ralbidv 2839 |
. . . . . . . . . . . . . . . 16
  
       

           |
98 | 97 | elrab 3208 |
. . . . . . . . . . . . . . 15
  
                      |
99 | 93, 98 | sylib 201 |
. . . . . . . . . . . . . 14
              |
100 | 99 | simprd 469 |
. . . . . . . . . . . . 13
            |
101 | 100 | r19.21bi 2769 |
. . . . . . . . . . . 12
 
           |
102 | 101 | adantr 471 |
. . . . . . . . . . 11
               |
103 | | ubthlem.6 |
. . . . . . . . . . . . 13
 |
104 | | ubthlem.7 |
. . . . . . . . . . . . . . . . . 18

    |
105 | 104 | sselda 3444 |
. . . . . . . . . . . . . . . . 17
 
     |
106 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19
         |
107 | | ubthlem.4 |
. . . . . . . . . . . . . . . . . . 19
     |
108 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19
                 |
109 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . 19
  
  |
110 | 33, 106, 107, 108, 109, 13, 103 | blocn2 26498 |
. . . . . . . . . . . . . . . . . 18
  

           |
111 | 107 | mopntopon 21503 |
. . . . . . . . . . . . . . . . . . . 20
      TopOn    |
112 | 38, 111 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
TopOn   |
113 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . . 21
         |
114 | 113, 106 | imsxmet 26373 |
. . . . . . . . . . . . . . . . . . . 20
                |
115 | 108 | mopntopon 21503 |
. . . . . . . . . . . . . . . . . . . 20
             
        TopOn        |
116 | 103, 114,
115 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
        TopOn       |
117 | | iscncl 20334 |
. . . . . . . . . . . . . . . . . . 19
  TopOn          TopOn                          
                           |
118 | 112, 116,
117 | mp2an 683 |
. . . . . . . . . . . . . . . . . 18
                                              |
119 | 110, 118 | sylib 201 |
. . . . . . . . . . . . . . . . 17
  
        
                          |
120 | 105, 119 | syl 17 |
. . . . . . . . . . . . . . . 16
 
          
                         |
121 | 120 | simpld 465 |
. . . . . . . . . . . . . . 15
 
           |
122 | 121 | adantr 471 |
. . . . . . . . . . . . . 14
               |
123 | 122, 26 | ffvelrnd 6046 |
. . . . . . . . . . . . 13
                                |
124 | | ubth.2 |
. . . . . . . . . . . . . 14
 CV   |
125 | 113, 124 | nvcl 26337 |
. . . . . . . . . . . . 13
                                                       |
126 | 103, 123,
125 | sylancr 674 |
. . . . . . . . . . . 12
                                |
127 | 122, 16 | ffvelrnd 6046 |
. . . . . . . . . . . . 13
               |
128 | 113, 124 | nvcl 26337 |
. . . . . . . . . . . . 13
          
          |
129 | 103, 127,
128 | sylancr 674 |
. . . . . . . . . . . 12
               |
130 | 1 | nnred 10652 |
. . . . . . . . . . . . 13
   |
131 | 130 | ad2antrr 737 |
. . . . . . . . . . . 12
       |
132 | | le2add 10124 |
. . . . . . . . . . . 12
                                     
                                     
                                   
    |
133 | 126, 129,
131, 131, 132 | syl22anc 1277 |
. . . . . . . . . . 11
                                        
                                   
    |
134 | 102, 133 | mpan2d 685 |
. . . . . . . . . 10
                                                                  
    |
135 | 47 | fveq2d 5892 |
. . . . . . . . . . . . . . 15
                                                 |
136 | 103 | a1i 11 |
. . . . . . . . . . . . . . . 16
       |
137 | | eqid 2462 |
. . . . . . . . . . . . . . . . . . . 20
  
  |
138 | 137, 109 | bloln 26474 |
. . . . . . . . . . . . . . . . . . 19
 

 

   |
139 | 13, 103, 138 | mp3an12 1363 |
. . . . . . . . . . . . . . . . . 18
  

   |
140 | 105, 139 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
     |
141 | 140 | adantr 471 |
. . . . . . . . . . . . . . . 16
         |
142 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
         |
143 | 20, 42, 142, 137 | lnosub 26449 |
. . . . . . . . . . . . . . . 16
  
                    
 
                                                                |
144 | 14, 136, 141, 26, 16, 143 | syl32anc 1284 |
. . . . . . . . . . . . . . 15
                                                                     |
145 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
           |
146 | 20, 21, 145, 137 | lnomul 26450 |
. . . . . . . . . . . . . . . 16
  
   
                              |
147 | 14, 136, 141, 18, 19, 146 | syl32anc 1284 |
. . . . . . . . . . . . . . 15
                                 |
148 | 135, 144,
147 | 3eqtr3d 2504 |
. . . . . . . . . . . . . 14
                                                     |
149 | 148 | fveq2d 5892 |
. . . . . . . . . . . . 13
                                                             |
150 | 121 | ffvelrnda 6045 |
. . . . . . . . . . . . . 14
               |
151 | 113, 145,
124 | nvsge0 26341 |
. . . . . . . . . . . . . 14
  
         
                             |
152 | 136, 50, 150, 151 | syl3anc 1276 |
. . . . . . . . . . . . 13
                                  |
153 | 149, 152 | eqtrd 2496 |
. . . . . . . . . . . 12
                                                      |
154 | 113, 142,
124 | nvmtri 26349 |
. . . . . . . . . . . . 13
                                   
                                                                          |
155 | 136, 123,
127, 154 | syl3anc 1276 |
. . . . . . . . . . . 12
                                         
                                     |
156 | 153, 155 | eqbrtrrd 4439 |
. . . . . . . . . . 11
     
                                              |
157 | 17 | rpred 11370 |
. . . . . . . . . . . . 13
       |
158 | 113, 124 | nvcl 26337 |
. . . . . . . . . . . . . 14
          
          |
159 | 103, 150,
158 | sylancr 674 |
. . . . . . . . . . . . 13
               |
160 | 157, 159 | remulcld 9697 |
. . . . . . . . . . . 12
     
           |
161 | 126, 129 | readdcld 9696 |
. . . . . . . . . . . 12
                                          |
162 | 3 | rpred 11370 |
. . . . . . . . . . . . 13
     |
163 | 162 | ad2antrr 737 |
. . . . . . . . . . . 12
     
   |
164 | | letr 9753 |
. . . . . . . . . . . 12
                                               
                                                                                   
                  |
165 | 160, 161,
163, 164 | syl3anc 1276 |
. . . . . . . . . . 11
                
                                                                     
                  |
166 | 156, 165 | mpand 686 |
. . . . . . . . . 10
                                         
                |
167 | 134, 166 | syld 45 |
. . . . . . . . 9
                                              |
168 | 159, 163,
17 | lemuldiv2d 11417 |
. . . . . . . . 9
                 
               |
169 | 167, 168 | sylibd 222 |
. . . . . . . 8
                                      
 
     |
170 | 83, 169 | syld 45 |
. . . . . . 7
      
                        
               |
171 | 170 | adantld 473 |
. . . . . 6
                        
                                         |
172 | 80, 171 | syld 45 |
. . . . 5
        CV    
               |
173 | 172 | ralrimiva 2814 |
. . . 4
 
 
   CV            
 
     |
174 | 5 | rpxrd 11371 |
. . . . . 6
       |
175 | 174 | adantr 471 |
. . . . 5
 
       |
176 | | eqid 2462 |
. . . . . 6
           |
177 | 20, 113, 43, 124, 176, 13, 103 | nmoubi 26462 |
. . . . 5
                        
 
 

   CV            
 
      |
178 | 121, 175,
177 | syl2anc 671 |
. . . 4
 
          
 
 

   CV            
 
      |
179 | 173, 178 | mpbird 240 |
. . 3
 
                |
180 | 179 | ralrimiva 2814 |
. 2
          
 
    |
181 | | breq2 4420 |
. . . 4
              
                |
182 | 181 | ralbidv 2839 |
. . 3
      
        

                |
183 | 182 | rspcev 3162 |
. 2
                                  |
184 | 6, 180, 183 | syl2anc 671 |
1
              |