Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  minvecolem2OLD Structured version   Visualization version   Unicode version

Theorem minvecolem2OLD 26520
 Description: Lemma for minvecoOLD 26529. Any two points and in are close to each other if they are close to the infimum of distance to . (Contributed by Mario Carneiro, 9-May-2014.) Obsolete version of minvecolem2 26510 as of 4-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
minvecoOLD.x
minvecoOLD.m
minvecoOLD.n CV
minvecoOLD.y
minvecoOLD.u
minvecoOLD.w
minvecoOLD.a
minvecoOLD.d
minvecoOLD.j
minvecoOLD.r
minvecoOLD.s
minvecolem2OLD.1
minvecolem2OLD.2
minvecolem2OLD.3
minvecolem2OLD.4
minvecolem2OLD.5
minvecolem2OLD.6
Assertion
Ref Expression
minvecolem2OLD
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem minvecolem2OLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 4re 10683 . . . . . 6
2 minvecoOLD.s . . . . . . . 8
3 minvecoOLD.x . . . . . . . . . . 11
4 minvecoOLD.m . . . . . . . . . . 11
5 minvecoOLD.n . . . . . . . . . . 11 CV
6 minvecoOLD.y . . . . . . . . . . 11
7 minvecoOLD.u . . . . . . . . . . 11
8 minvecoOLD.w . . . . . . . . . . 11
9 minvecoOLD.a . . . . . . . . . . 11
10 minvecoOLD.d . . . . . . . . . . 11
11 minvecoOLD.j . . . . . . . . . . 11
12 minvecoOLD.r . . . . . . . . . . 11
133, 4, 5, 6, 7, 8, 9, 10, 11, 12minvecolem1 26509 . . . . . . . . . 10
1413simp1d 1019 . . . . . . . . 9
1513simp2d 1020 . . . . . . . . 9
16 0re 9640 . . . . . . . . . 10
1713simp3d 1021 . . . . . . . . . 10
18 breq1 4404 . . . . . . . . . . . 12
1918ralbidv 2826 . . . . . . . . . . 11
2019rspcev 3149 . . . . . . . . . 10
2116, 17, 20sylancr 668 . . . . . . . . 9
22 infmrclOLD 10590 . . . . . . . . 9
2314, 15, 21, 22syl3anc 1267 . . . . . . . 8
242, 23syl5eqel 2532 . . . . . . 7
2524resqcld 12439 . . . . . 6
26 remulcl 9621 . . . . . 6
271, 25, 26sylancr 668 . . . . 5
28 phnv 26448 . . . . . . . . 9
297, 28syl 17 . . . . . . . 8
303, 10imsmet 26316 . . . . . . . 8
3129, 30syl 17 . . . . . . 7
32 inss1 3651 . . . . . . . . . 10
3332, 8sseldi 3429 . . . . . . . . 9
34 eqid 2450 . . . . . . . . . 10
353, 6, 34sspba 26359 . . . . . . . . 9
3629, 33, 35syl2anc 666 . . . . . . . 8
37 minvecolem2OLD.3 . . . . . . . 8
3836, 37sseldd 3432 . . . . . . 7
39 minvecolem2OLD.4 . . . . . . . 8
4036, 39sseldd 3432 . . . . . . 7
41 metcl 21340 . . . . . . 7
4231, 38, 40, 41syl3anc 1267 . . . . . 6
4342resqcld 12439 . . . . 5
4427, 43readdcld 9667 . . . 4
45 ax-1cn 9594 . . . . . . . . . . . . 13
46 halfcl 10835 . . . . . . . . . . . . 13
4745, 46mp1i 13 . . . . . . . . . . . 12
48 eqid 2450 . . . . . . . . . . . . . . 15
49 eqid 2450 . . . . . . . . . . . . . . 15
506, 48, 49, 34sspgval 26361 . . . . . . . . . . . . . 14
5129, 33, 37, 39, 50syl22anc 1268 . . . . . . . . . . . . 13
5234sspnv 26358 . . . . . . . . . . . . . . 15
5329, 33, 52syl2anc 666 . . . . . . . . . . . . . 14
546, 49nvgcl 26232 . . . . . . . . . . . . . 14
5553, 37, 39, 54syl3anc 1267 . . . . . . . . . . . . 13
5651, 55eqeltrrd 2529 . . . . . . . . . . . 12
57 eqid 2450 . . . . . . . . . . . . 13
58 eqid 2450 . . . . . . . . . . . . 13
596, 57, 58, 34sspsval 26363 . . . . . . . . . . . 12
6029, 33, 47, 56, 59syl22anc 1268 . . . . . . . . . . 11
616, 58nvscl 26240 . . . . . . . . . . . 12
6253, 47, 56, 61syl3anc 1267 . . . . . . . . . . 11
6360, 62eqeltrrd 2529 . . . . . . . . . 10
6436, 63sseldd 3432 . . . . . . . . 9
653, 4nvmcl 26261 . . . . . . . . 9
6629, 9, 64, 65syl3anc 1267 . . . . . . . 8
673, 5nvcl 26281 . . . . . . . 8
6829, 66, 67syl2anc 666 . . . . . . 7
6968resqcld 12439 . . . . . 6
70 remulcl 9621 . . . . . 6
711, 69, 70sylancr 668 . . . . 5
7271, 43readdcld 9667 . . . 4
73 minvecolem2OLD.1 . . . . . 6
7425, 73readdcld 9667 . . . . 5
75 remulcl 9621 . . . . 5
761, 74, 75sylancr 668 . . . 4
7716a1i 11 . . . . . . . . . 10
78 infmrgelbOLD 10592 . . . . . . . . . 10
7914, 15, 21, 77, 78syl31anc 1270 . . . . . . . . 9
8017, 79mpbird 236 . . . . . . . 8
8180, 2syl6breqr 4442 . . . . . . 7
82 eqid 2450 . . . . . . . . . . . 12
83 oveq2 6296 . . . . . . . . . . . . . . 15
8483fveq2d 5867 . . . . . . . . . . . . . 14
8584eqeq2d 2460 . . . . . . . . . . . . 13
8685rspcev 3149 . . . . . . . . . . . 12
8763, 82, 86sylancl 667 . . . . . . . . . . 11
88 eqid 2450 . . . . . . . . . . . 12
89 fvex 5873 . . . . . . . . . . . 12
9088, 89elrnmpti 5084 . . . . . . . . . . 11
9187, 90sylibr 216 . . . . . . . . . 10
9291, 12syl6eleqr 2539 . . . . . . . . 9
93 infmrlbOLD 10594 . . . . . . . . 9
9414, 21, 92, 93syl3anc 1267 . . . . . . . 8
952, 94syl5eqbr 4435 . . . . . . 7
96 le2sq2 12347 . . . . . . 7
9724, 81, 68, 95, 96syl22anc 1268 . . . . . 6
98 4pos 10702 . . . . . . . . 9
991, 98pm3.2i 457 . . . . . . . 8
100 lemul2 10455 . . . . . . . 8
10199, 100mp3an3 1352 . . . . . . 7
10225, 69, 101syl2anc 666 . . . . . 6
10397, 102mpbid 214 . . . . 5
10427, 71, 43, 103leadd1dd 10224 . . . 4
105 metcl 21340 . . . . . . . . . 10
10631, 9, 38, 105syl3anc 1267 . . . . . . . . 9
107106resqcld 12439 . . . . . . . 8
108 metcl 21340 . . . . . . . . . 10
10931, 9, 40, 108syl3anc 1267 . . . . . . . . 9
110109resqcld 12439 . . . . . . . 8
111 minvecolem2OLD.5 . . . . . . . 8
112 minvecolem2OLD.6 . . . . . . . 8
113107, 110, 74, 74, 111, 112le2addd 10229 . . . . . . 7
11474recnd 9666 . . . . . . . 8
1151142timesd 10852 . . . . . . 7
116113, 115breqtrrd 4428 . . . . . 6
117107, 110readdcld 9667 . . . . . . 7
118 2re 10676 . . . . . . . 8
119 remulcl 9621 . . . . . . . 8
120118, 74, 119sylancr 668 . . . . . . 7
121 2pos 10698 . . . . . . . . 9
122118, 121pm3.2i 457 . . . . . . . 8
123 lemul2 10455 . . . . . . . 8
124122, 123mp3an3 1352 . . . . . . 7
125117, 120, 124syl2anc 666 . . . . . 6
126116, 125mpbid 214 . . . . 5
1273, 4nvmcl 26261 . . . . . . . 8
12829, 9, 38, 127syl3anc 1267 . . . . . . 7
1293, 4nvmcl 26261 . . . . . . . 8
13029, 9, 40, 129syl3anc 1267 . . . . . . 7
1313, 48, 4, 5phpar2 26457 . . . . . . 7
1327, 128, 130, 131syl3anc 1267 . . . . . 6
133 2cn 10677 . . . . . . . . . 10
13468recnd 9666 . . . . . . . . . 10
135 sqmul 12335 . . . . . . . . . 10
136133, 134, 135sylancr 668 . . . . . . . . 9
137 sq2 12368 . . . . . . . . . 10
138137oveq1i 6298 . . . . . . . . 9
139136, 138syl6eq 2500 . . . . . . . 8
140133a1i 11 . . . . . . . . . . . 12
1413, 57, 5nvs 26284 . . . . . . . . . . . 12
14229, 140, 66, 141syl3anc 1267 . . . . . . . . . . 11
143 0le2 10697 . . . . . . . . . . . . 13
144 absid 13352 . . . . . . . . . . . . 13
145118, 143, 144mp2an 677 . . . . . . . . . . . 12
146145oveq1i 6298 . . . . . . . . . . 11
147142, 146syl6eq 2500 . . . . . . . . . 10
1483, 4, 57nvmdi 26264 . . . . . . . . . . . . 13
14929, 140, 9, 64, 148syl13anc 1269 . . . . . . . . . . . 12
1503, 48, 57nv2 26246 . . . . . . . . . . . . . 14
15129, 9, 150syl2anc 666 . . . . . . . . . . . . 13
152 2ne0 10699 . . . . . . . . . . . . . . . . 17
153133, 152recidi 10335 . . . . . . . . . . . . . . . 16
154153oveq1i 6298 . . . . . . . . . . . . . . 15
1553, 48nvgcl 26232 . . . . . . . . . . . . . . . . 17
15629, 38, 40, 155syl3anc 1267 . . . . . . . . . . . . . . . 16
1573, 57nvsid 26241 . . . . . . . . . . . . . . . 16
15829, 156, 157syl2anc 666 . . . . . . . . . . . . . . 15
159154, 158syl5eq 2496 . . . . . . . . . . . . . 14
1603, 57nvsass 26242 . . . . . . . . . . . . . . 15
16129, 140, 47, 156, 160syl13anc 1269 . . . . . . . . . . . . . 14
162159, 161eqtr3d 2486 . . . . . . . . . . . . 13
163151, 162oveq12d 6306 . . . . . . . . . . . 12
1643, 48, 4nvaddsub4 26275 . . . . . . . . . . . . 13
16529, 9, 9, 38, 40, 164syl122anc 1276 . . . . . . . . . . . 12
166149, 163, 1653eqtr2d 2490 . . . . . . . . . . 11
167166fveq2d 5867 . . . . . . . . . 10
168147, 167eqtr3d 2486 . . . . . . . . 9
169168oveq1d 6303 . . . . . . . 8
170139, 169eqtr3d 2486 . . . . . . 7
1713, 4, 5, 10imsdval 26311 . . . . . . . . . 10
17229, 40, 38, 171syl3anc 1267 . . . . . . . . 9
173 metsym 21358 . . . . . . . . . 10
17431, 38, 40, 173syl3anc 1267 . . . . . . . . 9
1753, 4nvnnncan1 26262 . . . . . . . . . . 11
17629, 9, 38, 40, 175syl13anc 1269 . . . . . . . . . 10
177176fveq2d 5867 . . . . . . . . 9
178172, 174, 1773eqtr4d 2494 . . . . . . . 8
179178oveq1d 6303 . . . . . . 7
180170, 179oveq12d 6306 . . . . . 6
1813, 4, 5, 10imsdval 26311 . . . . . . . . . 10
18229, 9, 38, 181syl3anc 1267 . . . . . . . . 9
183182oveq1d 6303 . . . . . . . 8
1843, 4, 5, 10imsdval 26311 . . . . . . . . . 10
18529, 9, 40, 184syl3anc 1267 . . . . . . . . 9
186185oveq1d 6303 . . . . . . . 8
187183, 186oveq12d 6306 . . . . . . 7
188187oveq2d 6304 . . . . . 6
189132, 180, 1883eqtr4d 2494 . . . . 5
190 2t2e4 10756 . . . . . . 7
191190oveq1i 6298 . . . . . 6
192140, 140, 114mulassd 9663 . . . . . 6
193191, 192syl5eqr 2498 . . . . 5
194126, 189, 1933brtr4d 4432 . . . 4
19544, 72, 76, 104, 194letrd 9789 . . 3
196 4cn 10684 . . . . 5
197196a1i 11 . . . 4
19825recnd 9666 . . . 4
19973recnd 9666 . . . 4
200197, 198, 199adddid 9664 . . 3
201195, 200breqtrd 4426 . 2
202 remulcl 9621 . . . 4
2031, 73, 202sylancr 668 . . 3
20443, 203, 27leadd2d 10205 . 2
205201, 204mpbird 236 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 188   wa 371   wceq 1443   wcel 1886   wne 2621  wral 2736  wrex 2737   cin 3402   wss 3403  c0 3730   class class class wbr 4401   cmpt 4460  ccnv 4832   crn 4834  cfv 5581  (class class class)co 6288  csup 7951  cc 9534  cr 9535  cc0 9536  c1 9537   caddc 9539   cmul 9541   clt 9672   cle 9673   cdiv 10266  c2 10656  c4 10658  cexp 12269  cabs 13290  cme 18949  cmopn 18953  cnv 26196  cpv 26197  cba 26198  cns 26199  cnsb 26201  CVcnmcv 26202  cims 26203  css 26353  ccphlo 26446  ccbn 26497 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-rep 4514  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613  ax-pre-sup 9614  ax-addf 9615  ax-mulf 9616 This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-map 7471  df-en 7567  df-dom 7568  df-sdom 7569  df-sup 7953  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-2 10665  df-3 10666  df-4 10667  df-n0 10867  df-z 10935  df-uz 11157  df-rp 11300  df-xadd 11407  df-seq 12211  df-exp 12270  df-cj 13155  df-re 13156  df-im 13157  df-sqrt 13291  df-abs 13292  df-xmet 18956  df-met 18957  df-grpo 25912  df-gid 25913  df-ginv 25914  df-gdiv 25915  df-ablo 26003  df-vc 26158  df-nv 26204  df-va 26207  df-ba 26208  df-sm 26209  df-0v 26210  df-vs 26211  df-nmcv 26212  df-ims 26213  df-ssp 26354  df-ph 26447  df-cbn 26498 This theorem is referenced by:  minvecolem3OLD  26521  minvecolem7OLD  26528
 Copyright terms: Public domain W3C validator