Step | Hyp | Ref
| Expression |
1 | | minveco.u |
. . . . . 6
    |
2 | | phnv 26455 |
. . . . . 6
 
  |
3 | | minveco.x |
. . . . . . 7
     |
4 | | minveco.d |
. . . . . . 7
     |
5 | 3, 4 | imsxmet 26324 |
. . . . . 6
        |
6 | 1, 2, 5 | 3syl 18 |
. . . . 5
        |
7 | | minveco.j |
. . . . . 6
     |
8 | 7 | methaus 21535 |
. . . . 5
        |
9 | | lmfun 20397 |
. . . . 5

       |
10 | 6, 8, 9 | 3syl 18 |
. . . 4
        |
11 | | minveco.m |
. . . . . 6
     |
12 | | minveco.n |
. . . . . 6
 CV   |
13 | | minveco.y |
. . . . . 6
     |
14 | | minveco.w |
. . . . . 6
         |
15 | | minveco.a |
. . . . . 6
   |
16 | | minveco.r |
. . . . . 6
           |
17 | | minveco.s |
. . . . . 6
inf    |
18 | | minveco.f |
. . . . . 6
       |
19 | | minveco.1 |
. . . . . 6
 

                      |
20 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4a 26519 |
. . . . 5
                                   |
21 | | eqid 2451 |
. . . . . . 7
 ↾t   ↾t   |
22 | | nnuz 11194 |
. . . . . . 7
     |
23 | | fvex 5875 |
. . . . . . . . 9
     |
24 | 13, 23 | eqeltri 2525 |
. . . . . . . 8
 |
25 | 24 | a1i 11 |
. . . . . . 7
   |
26 | 1, 2 | syl 17 |
. . . . . . . 8
   |
27 | 7 | mopntop 21455 |
. . . . . . . 8
        |
28 | 26, 5, 27 | 3syl 18 |
. . . . . . 7
   |
29 | | elin 3617 |
. . . . . . . . . . . . 13
           
   |
30 | 14, 29 | sylib 200 |
. . . . . . . . . . . 12
     
   |
31 | 30 | simpld 461 |
. . . . . . . . . . 11
       |
32 | | eqid 2451 |
. . . . . . . . . . . 12
         |
33 | 3, 13, 32 | sspba 26366 |
. . . . . . . . . . 11
      
  |
34 | 26, 31, 33 | syl2anc 667 |
. . . . . . . . . 10

  |
35 | | xmetres2 21376 |
. . . . . . . . . 10
       
           |
36 | 6, 34, 35 | syl2anc 667 |
. . . . . . . . 9
            |
37 | | eqid 2451 |
. . . . . . . . . 10
   
       
     |
38 | 37 | mopntopon 21454 |
. . . . . . . . 9
 
            
   TopOn    |
39 | 36, 38 | syl 17 |
. . . . . . . 8
         TopOn    |
40 | | lmcl 20313 |
. . . . . . . 8
          TopOn                                                      |
41 | 39, 20, 40 | syl2anc 667 |
. . . . . . 7
                    |
42 | | 1zzd 10968 |
. . . . . . 7
   |
43 | 21, 22, 25, 28, 41, 42, 18 | lmss 20314 |
. . . . . 6
                 
             
↾t             
          |
44 | | eqid 2451 |
. . . . . . . . . 10
    
    |
45 | 44, 7, 37 | metrest 21539 |
. . . . . . . . 9
       
 ↾t     
      |
46 | 6, 34, 45 | syl2anc 667 |
. . . . . . . 8
 
↾t      
     |
47 | 46 | fveq2d 5869 |
. . . . . . 7
      ↾t           
      |
48 | 47 | breqd 4413 |
. . . . . 6
       
↾t             
      
                                   |
49 | 43, 48 | bitrd 257 |
. . . . 5
                 
                                           |
50 | 20, 49 | mpbird 236 |
. . . 4
                
          |
51 | | funbrfv 5903 |
. . . 4
     
                                          
           |
52 | 10, 50, 51 | sylc 62 |
. . 3
                  
          |
53 | 52, 41 | eqeltrd 2529 |
. 2
            |
54 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4b 26520 |
. . . . . 6
            |
55 | 3, 11, 12, 4 | imsdval 26318 |
. . . . . 6
 
                                          |
56 | 26, 15, 54, 55 | syl3anc 1268 |
. . . . 5
                                 |
57 | 56 | adantr 467 |
. . . 4
 
                                 |
58 | 3, 4 | imsmet 26323 |
. . . . . . . 8
       |
59 | 1, 2, 58 | 3syl 18 |
. . . . . . 7
       |
60 | | metcl 21347 |
. . . . . . 7
     
                         |
61 | 59, 15, 54, 60 | syl3anc 1268 |
. . . . . 6
                |
62 | 61 | adantr 467 |
. . . . 5
 
                |
63 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19 | minvecolem4c 26521 |
. . . . . 6
   |
64 | 63 | adantr 467 |
. . . . 5
 
   |
65 | 26 | adantr 467 |
. . . . . 6
 
   |
66 | 15 | adantr 467 |
. . . . . . 7
 
   |
67 | 34 | sselda 3432 |
. . . . . . 7
 
   |
68 | 3, 11 | nvmcl 26268 |
. . . . . . 7
 
       |
69 | 65, 66, 67, 68 | syl3anc 1268 |
. . . . . 6
 
       |
70 | 3, 12 | nvcl 26288 |
. . . . . 6
                 |
71 | 65, 69, 70 | syl2anc 667 |
. . . . 5
 
           |
72 | 63, 61 | ltnled 9782 |
. . . . . . . 8
              
                |
73 | | eqid 2451 |
. . . . . . . . . . 11
                     |
74 | 6 | adantr 467 |
. . . . . . . . . . 11
 
             
       |
75 | | minveco.t |
. . . . . . . . . . . . . . 15
                              |
76 | 61, 63 | readdcld 9670 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
77 | 76 | rehalfcld 10859 |
. . . . . . . . . . . . . . . . . . . 20
                    |
78 | 77 | resqcld 12442 |
. . . . . . . . . . . . . . . . . . 19
                        |
79 | 63 | resqcld 12442 |
. . . . . . . . . . . . . . . . . . 19
       |
80 | 78, 79 | resubcld 10047 |
. . . . . . . . . . . . . . . . . 18
                              |
81 | 80 | adantr 467 |
. . . . . . . . . . . . . . . . 17
 
             
                             |
82 | 63, 61, 63 | ltadd1d 10206 |
. . . . . . . . . . . . . . . . . . . 20
              
                    |
83 | 63 | recnd 9669 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
84 | 83 | 2timesd 10855 |
. . . . . . . . . . . . . . . . . . . . 21
       |
85 | 84 | breq1d 4412 |
. . . . . . . . . . . . . . . . . . . 20
                    
                  |
86 | | 2re 10679 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
87 | | 2pos 10701 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
88 | 86, 87 | pm3.2i 457 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
     |
90 | | ltmuldiv2 10479 |
. . . . . . . . . . . . . . . . . . . . 21
                   
                 
                    |
91 | 63, 76, 89, 90 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . 20
                  
                    |
92 | 82, 85, 91 | 3bitr2d 285 |
. . . . . . . . . . . . . . . . . . 19
              
                    |
93 | 3, 11, 12, 13, 1, 14, 15, 4, 7, 16 | minvecolem1 26516 |
. . . . . . . . . . . . . . . . . . . . . . 23
  
   |
94 | 93 | simp3d 1022 |
. . . . . . . . . . . . . . . . . . . . . 22
 
  |
95 | 93 | simp1d 1020 |
. . . . . . . . . . . . . . . . . . . . . . 23

  |
96 | 93 | simp2d 1021 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
97 | | 0re 9643 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 |
98 | | breq1 4405 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
   |
99 | 98 | ralbidv 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
  

   |
100 | 99 | rspcev 3150 |
. . . . . . . . . . . . . . . . . . . . . . . 24
    
   |
101 | 97, 94, 100 | sylancr 669 |
. . . . . . . . . . . . . . . . . . . . . . 23
     |
102 | 97 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
103 | | infregelb 10594 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

  
inf       |
104 | 95, 96, 101, 102, 103 | syl31anc 1271 |
. . . . . . . . . . . . . . . . . . . . . 22
  inf   
   |
105 | 94, 104 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21

inf     |
106 | 105, 17 | syl6breqr 4443 |
. . . . . . . . . . . . . . . . . . . 20

  |
107 | | metge0 21360 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
                         |
108 | 59, 15, 54, 107 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . 22

               |
109 | 61, 63, 108, 106 | addge0d 10189 |
. . . . . . . . . . . . . . . . . . . . 21

                 |
110 | | divge0 10474 |
. . . . . . . . . . . . . . . . . . . . 21
                                                        |
111 | 76, 109, 89, 110 | syl21anc 1267 |
. . . . . . . . . . . . . . . . . . . 20

                   |
112 | 63, 77, 106, 111 | lt2sqd 12450 |
. . . . . . . . . . . . . . . . . . 19
                                               |
113 | 79, 78 | posdifd 10200 |
. . . . . . . . . . . . . . . . . . 19
                          
                              |
114 | 92, 112, 113 | 3bitrd 283 |
. . . . . . . . . . . . . . . . . 18
              
                              |
115 | 114 | biimpa 487 |
. . . . . . . . . . . . . . . . 17
 
             
                             |
116 | 81, 115 | elrpd 11338 |
. . . . . . . . . . . . . . . 16
 
             
                             |
117 | 116 | rpreccld 11351 |
. . . . . . . . . . . . . . 15
 
             
                               |
118 | 75, 117 | syl5eqel 2533 |
. . . . . . . . . . . . . 14
 
             
  |
119 | 118 | rprege0d 11348 |
. . . . . . . . . . . . 13
 
             
    |
120 | | flge0nn0 12054 |
. . . . . . . . . . . . 13
         |
121 | | nn0p1nn 10909 |
. . . . . . . . . . . . 13
    
        |
122 | 119, 120,
121 | 3syl 18 |
. . . . . . . . . . . 12
 
             
        |
123 | 122 | nnzd 11039 |
. . . . . . . . . . 11
 
             
        |
124 | 50, 52 | breqtrrd 4429 |
. . . . . . . . . . . 12
                   |
125 | 124 | adantr 467 |
. . . . . . . . . . 11
 
             
                  |
126 | 15 | adantr 467 |
. . . . . . . . . . 11
 
             
  |
127 | 77 | adantr 467 |
. . . . . . . . . . . 12
 
             
                   |
128 | 127 | rexrd 9690 |
. . . . . . . . . . 11
 
             
                   |
129 | | simpll 760 |
. . . . . . . . . . . . . . 15
                              |
130 | | eluznn 11229 |
. . . . . . . . . . . . . . . 16
       
          
  |
131 | 122, 130 | sylan 474 |
. . . . . . . . . . . . . . 15
                              |
132 | 59 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

      |
133 | 15 | adantr 467 |
. . . . . . . . . . . . . . . 16
 

  |
134 | 18, 34 | fssd 5738 |
. . . . . . . . . . . . . . . . 17
       |
135 | 134 | ffvelrnda 6022 |
. . . . . . . . . . . . . . . 16
 

      |
136 | | metcl 21347 |
. . . . . . . . . . . . . . . 16
     
               |
137 | 132, 133,
135, 136 | syl3anc 1268 |
. . . . . . . . . . . . . . 15
 

          |
138 | 129, 131,
137 | syl2anc 667 |
. . . . . . . . . . . . . 14
                                      |
139 | 138 | resqcld 12442 |
. . . . . . . . . . . . 13
                                          |
140 | 63 | ad2antrr 732 |
. . . . . . . . . . . . . . 15
                              |
141 | 140 | resqcld 12442 |
. . . . . . . . . . . . . 14
                                  |
142 | 131 | nnrecred 10655 |
. . . . . . . . . . . . . 14
                                |
143 | 141, 142 | readdcld 9670 |
. . . . . . . . . . . . 13
                                      |
144 | 78 | ad2antrr 732 |
. . . . . . . . . . . . 13
                                                   |
145 | 129, 131,
19 | syl2anc 667 |
. . . . . . . . . . . . 13
                                                  |
146 | 118 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
                              |
147 | 146 | rpred 11341 |
. . . . . . . . . . . . . . . . 17
                              |
148 | | reflcl 12032 |
. . . . . . . . . . . . . . . . . 18
       |
149 | | peano2re 9806 |
. . . . . . . . . . . . . . . . . 18
             |
150 | 147, 148,
149 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
                                    |
151 | 131 | nnred 10624 |
. . . . . . . . . . . . . . . . 17
                              |
152 | | fllep1 12037 |
. . . . . . . . . . . . . . . . . 18
         |
153 | 147, 152 | syl 17 |
. . . . . . . . . . . . . . . . 17
                                    |
154 | | eluzle 11171 |
. . . . . . . . . . . . . . . . . 18
          
        |
155 | 154 | adantl 468 |
. . . . . . . . . . . . . . . . 17
                                    |
156 | 147, 150,
151, 153, 155 | letrd 9792 |
. . . . . . . . . . . . . . . 16
                              |
157 | 75, 156 | syl5eqbrr 4437 |
. . . . . . . . . . . . . . 15
                                                        
  |
158 | | 1red 9658 |
. . . . . . . . . . . . . . . 16
                              |
159 | 80 | ad2antrr 732 |
. . . . . . . . . . . . . . . 16
                                                         |
160 | 115 | adantr 467 |
. . . . . . . . . . . . . . . 16
                                                         |
161 | 131 | nngt0d 10653 |
. . . . . . . . . . . . . . . 16
                              |
162 | | lediv23 10498 |
. . . . . . . . . . . . . . . 16
                                                                                                                           |
163 | 158, 159,
160, 151, 161, 162 | syl122anc 1277 |
. . . . . . . . . . . . . . 15
                                                                                          |
164 | 157, 163 | mpbid 214 |
. . . . . . . . . . . . . 14
                                                           |
165 | 141, 142,
144 | leaddsub2d 10215 |
. . . . . . . . . . . . . 14
                                                                                          |
166 | 164, 165 | mpbird 236 |
. . . . . . . . . . . . 13
                                                           |
167 | 139, 143,
144, 145, 166 | letrd 9792 |
. . . . . . . . . . . 12
                                                               |
168 | 77 | ad2antrr 732 |
. . . . . . . . . . . . 13
                                               |
169 | | metge0 21360 |
. . . . . . . . . . . . . . 15
     
               |
170 | 132, 133,
135, 169 | syl3anc 1268 |
. . . . . . . . . . . . . 14
 

          |
171 | 129, 131,
170 | syl2anc 667 |
. . . . . . . . . . . . 13
                                      |
172 | 111 | ad2antrr 732 |
. . . . . . . . . . . . 13
                                               |
173 | 138, 168,
171, 172 | le2sqd 12451 |
. . . . . . . . . . . 12
                                                                 
                        |
174 | 167, 173 | mpbird 236 |
. . . . . . . . . . 11
                                                       |
175 | 73, 7, 74, 123, 125, 126, 128, 174 | lmle 22271 |
. . . . . . . . . 10
 
             
                                |
176 | 61, 63, 61 | leadd2d 10208 |
. . . . . . . . . . . 12
                                                             |
177 | 61 | recnd 9669 |
. . . . . . . . . . . . . 14
                |
178 | 177 | 2timesd 10855 |
. . . . . . . . . . . . 13
                                              |
179 | 178 | breq1d 4412 |
. . . . . . . . . . . 12
                                                           
                  |
180 | | lemuldiv2 10487 |
. . . . . . . . . . . . . 14
                                
                                                                |
181 | 88, 180 | mp3an3 1353 |
. . . . . . . . . . . . 13
                                                                                               |
182 | 61, 76, 181 | syl2anc 667 |
. . . . . . . . . . . 12
                                            
                    |
183 | 176, 179,
182 | 3bitr2d 285 |
. . . . . . . . . . 11
                                                |
184 | 183 | biimpar 488 |
. . . . . . . . . 10
 
                              
               |
185 | 175, 184 | syldan 473 |
. . . . . . . . 9
 
             
               |
186 | 185 | ex 436 |
. . . . . . . 8
                               |
187 | 72, 186 | sylbird 239 |
. . . . . . 7
                           
   |
188 | 187 | pm2.18d 115 |
. . . . . 6
             
  |
189 | 188 | adantr 467 |
. . . . 5
 
                |
190 | 95 | adantr 467 |
. . . . . . 7
 
   |
191 | 101 | adantr 467 |
. . . . . . 7
 
     |
192 | | simpr 463 |
. . . . . . . . 9
 
   |
193 | | fvex 5875 |
. . . . . . . . 9
         |
194 | | eqid 2451 |
. . . . . . . . . 10
                     |
195 | 194 | elrnmpt1 5083 |
. . . . . . . . 9
                               |
196 | 192, 193,
195 | sylancl 668 |
. . . . . . . 8
 
                     |
197 | 196, 16 | syl6eleqr 2540 |
. . . . . . 7
 
           |
198 | | infrelb 10596 |
. . . . . . 7
 


         inf  
          |
199 | 190, 191,
197, 198 | syl3anc 1268 |
. . . . . 6
 
 inf             |
200 | 17, 199 | syl5eqbr 4436 |
. . . . 5
 
           |
201 | 62, 64, 71, 189, 200 | letrd 9792 |
. . . 4
 
                        |
202 | 57, 201 | eqbrtrrd 4425 |
. . 3
 
                            |
203 | 202 | ralrimiva 2802 |
. 2
                             |
204 | | oveq2 6298 |
. . . . . 6
         
                   |
205 | 204 | fveq2d 5869 |
. . . . 5
         
                           |
206 | 205 | breq1d 4412 |
. . . 4
         
                                 
           |
207 | 206 | ralbidv 2827 |
. . 3
         
 
                                             |
208 | 207 | rspcev 3150 |
. 2
                                     


                  |
209 | 53, 203, 208 | syl2anc 667 |
1
  
                  |