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

Theorem minveclem4 19338
 Description: Lemma for minvec 19342. The convergent point of the Cauchy sequence attains the minimum distance, and so is closer to than any other point in . (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
Hypotheses
Ref Expression
minvec.x
minvec.m
minvec.n
minvec.u
minvec.y
minvec.w s CMetSp
minvec.a
minvec.j
minvec.r
minvec.s
minvec.d
minvec.f
minvec.p
minvec.t
Assertion
Ref Expression
minveclem4
Distinct variable groups:   ,,   ,,,   ,,,   ,,   ,,   ,,   ,,,   ,,   ,,   ,,,   ,,,   ,,,   ,,,   ,,
Allowed substitution hints:   ()   ()   ()   ()   ()   ()   ()

Proof of Theorem minveclem4
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 inss2 3564 . . 3
2 minvec.x . . . 4
3 minvec.m . . . 4
4 minvec.n . . . 4
5 minvec.u . . . 4
6 minvec.y . . . 4
7 minvec.w . . . 4 s CMetSp
8 minvec.a . . . 4
9 minvec.j . . . 4
10 minvec.r . . . 4
11 minvec.s . . . 4
12 minvec.d . . . 4
13 minvec.f . . . 4
14 minvec.p . . . 4
152, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14minveclem4a 19336 . . 3
161, 15sseldi 3348 . 2
1712oveqi 6097 . . . . . . 7
182, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14minveclem4b 19337 . . . . . . . 8
198, 18ovresd 6217 . . . . . . 7
2017, 19syl5eq 2482 . . . . . 6
21 cphngp 19141 . . . . . . . 8 NrmGrp
225, 21syl 16 . . . . . . 7 NrmGrp
23 eqid 2438 . . . . . . . 8
244, 2, 3, 23ngpds 18655 . . . . . . 7 NrmGrp
2522, 8, 18, 24syl3anc 1185 . . . . . 6
2620, 25eqtrd 2470 . . . . 5
2726adantr 453 . . . 4
28 ngpms 18652 . . . . . . . 8 NrmGrp
292, 12msmet 18492 . . . . . . . 8
3022, 28, 293syl 19 . . . . . . 7
31 metcl 18367 . . . . . . 7
3230, 8, 18, 31syl3anc 1185 . . . . . 6
3332adantr 453 . . . . 5
342, 3, 4, 5, 6, 7, 8, 9, 10, 11minveclem4c 19331 . . . . . 6
3534adantr 453 . . . . 5
3622adantr 453 . . . . . 6 NrmGrp
37 cphlmod 19142 . . . . . . . . 9
385, 37syl 16 . . . . . . . 8
3938adantr 453 . . . . . . 7
408adantr 453 . . . . . . 7
41 eqid 2438 . . . . . . . . . 10
422, 41lssss 16018 . . . . . . . . 9
436, 42syl 16 . . . . . . . 8
4443sselda 3350 . . . . . . 7
452, 3lmodvsubcl 15994 . . . . . . 7
4639, 40, 44, 45syl3anc 1185 . . . . . 6
472, 4nmcl 18667 . . . . . 6 NrmGrp
4836, 46, 47syl2anc 644 . . . . 5
4934, 32ltnled 9225 . . . . . . . 8
502, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13minveclem3b 19334 . . . . . . . . . . . . . . . . . 18
51 fbsspw 17869 . . . . . . . . . . . . . . . . . . . 20
5250, 51syl 16 . . . . . . . . . . . . . . . . . . 19
53 sspwb 4416 . . . . . . . . . . . . . . . . . . . 20
5443, 53sylib 190 . . . . . . . . . . . . . . . . . . 19
5552, 54sstrd 3360 . . . . . . . . . . . . . . . . . 18
56 fvex 5745 . . . . . . . . . . . . . . . . . . . 20
572, 56eqeltri 2508 . . . . . . . . . . . . . . . . . . 19
5857a1i 11 . . . . . . . . . . . . . . . . . 18
59 fbasweak 17902 . . . . . . . . . . . . . . . . . 18
6050, 55, 58, 59syl3anc 1185 . . . . . . . . . . . . . . . . 17
6160adantr 453 . . . . . . . . . . . . . . . 16
62 fgcl 17915 . . . . . . . . . . . . . . . 16
6361, 62syl 16 . . . . . . . . . . . . . . 15
64 ssfg 17909 . . . . . . . . . . . . . . . . 17
6561, 64syl 16 . . . . . . . . . . . . . . . 16
66 minvec.t . . . . . . . . . . . . . . . . . . 19
6732, 34readdcld 9120 . . . . . . . . . . . . . . . . . . . . . . . 24
6867rehalfcld 10219 . . . . . . . . . . . . . . . . . . . . . . 23
6968resqcld 11554 . . . . . . . . . . . . . . . . . . . . . 22
7034resqcld 11554 . . . . . . . . . . . . . . . . . . . . . 22
7169, 70resubcld 9470 . . . . . . . . . . . . . . . . . . . . 21
7271adantr 453 . . . . . . . . . . . . . . . . . . . 20
7334, 32, 34ltadd1d 9624 . . . . . . . . . . . . . . . . . . . . . . 23
7434recnd 9119 . . . . . . . . . . . . . . . . . . . . . . . . 25
75742timesd 10215 . . . . . . . . . . . . . . . . . . . . . . . 24
7675breq1d 4225 . . . . . . . . . . . . . . . . . . . . . . 23
77 2re 10074 . . . . . . . . . . . . . . . . . . . . . . . . . 26
78 2pos 10087 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7977, 78pm3.2i 443 . . . . . . . . . . . . . . . . . . . . . . . . 25
8079a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24
81 ltmuldiv2 9886 . . . . . . . . . . . . . . . . . . . . . . . 24
8234, 67, 80, 81syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . 23
8373, 76, 823bitr2d 274 . . . . . . . . . . . . . . . . . . . . . 22
842, 3, 4, 5, 6, 7, 8, 9, 10minveclem1 19330 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8584simp3d 972 . . . . . . . . . . . . . . . . . . . . . . . . 25
8684simp1d 970 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8784simp2d 971 . . . . . . . . . . . . . . . . . . . . . . . . . 26
88 0re 9096 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
89 breq1 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9089ralbidv 2727 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9190rspcev 3054 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9288, 85, 91sylancr 646 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9388a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
94 infmrgelb 9993 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9586, 87, 92, 93, 94syl31anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . 25
9685, 95mpbird 225 . . . . . . . . . . . . . . . . . . . . . . . 24
9796, 11syl6breqr 4255 . . . . . . . . . . . . . . . . . . . . . . 23
98 metge0 18380 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9930, 8, 18, 98syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . 25
10032, 34, 99, 97addge0d 9607 . . . . . . . . . . . . . . . . . . . . . . . 24
101 divge0 9884 . . . . . . . . . . . . . . . . . . . . . . . 24
10267, 100, 80, 101syl21anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23
10334, 68, 97, 102lt2sqd 11562 . . . . . . . . . . . . . . . . . . . . . 22
10470, 69posdifd 9618 . . . . . . . . . . . . . . . . . . . . . 22
10583, 103, 1043bitrd 272 . . . . . . . . . . . . . . . . . . . . 21
106105biimpa 472 . . . . . . . . . . . . . . . . . . . 20
10772, 106elrpd 10651 . . . . . . . . . . . . . . . . . . 19
10866, 107syl5eqel 2522 . . . . . . . . . . . . . . . . . 18
1096adantr 453 . . . . . . . . . . . . . . . . . . 19
110 rabexg 4356 . . . . . . . . . . . . . . . . . . 19
111109, 110syl 16 . . . . . . . . . . . . . . . . . 18
112 eqid 2438 . . . . . . . . . . . . . . . . . . 19
113 oveq2 6092 . . . . . . . . . . . . . . . . . . . . 21
114113breq2d 4227 . . . . . . . . . . . . . . . . . . . 20
115114rabbidv 2950 . . . . . . . . . . . . . . . . . . 19
116112, 115elrnmpt1s 5121 . . . . . . . . . . . . . . . . . 18
117108, 111, 116syl2anc 644 . . . . . . . . . . . . . . . . 17
118117, 13syl6eleqr 2529 . . . . . . . . . . . . . . . 16
11965, 118sseldd 3351 . . . . . . . . . . . . . . 15
120 ssrab2 3430 . . . . . . . . . . . . . . . 16
121120a1i 11 . . . . . . . . . . . . . . 15
12266oveq2i 6095 . . . . . . . . . . . . . . . . . . . 20
12370ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . 22
124123recnd 9119 . . . . . . . . . . . . . . . . . . . . 21
12568ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23
126125resqcld 11554 . . . . . . . . . . . . . . . . . . . . . 22
127126recnd 9119 . . . . . . . . . . . . . . . . . . . . 21
128124, 127pncan3d 9419 . . . . . . . . . . . . . . . . . . . 20
129122, 128syl5eq 2482 . . . . . . . . . . . . . . . . . . 19
130129breq2d 4227 . . . . . . . . . . . . . . . . . 18
13130ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20
1328ad2antrr 708 . . . . . . . . . . . . . . . . . . . 20
13344adantlr 697 . . . . . . . . . . . . . . . . . . . 20
134 metcl 18367 . . . . . . . . . . . . . . . . . . . 20
135131, 132, 133, 134syl3anc 1185 . . . . . . . . . . . . . . . . . . 19
136 metge0 18380 . . . . . . . . . . . . . . . . . . . 20
137131, 132, 133, 136syl3anc 1185 . . . . . . . . . . . . . . . . . . 19
138102ad2antrr 708 . . . . . . . . . . . . . . . . . . 19
139135, 125, 137, 138le2sqd 11563 . . . . . . . . . . . . . . . . . 18
140130, 139bitr4d 249 . . . . . . . . . . . . . . . . 17
141140rabbidva 2949 . . . . . . . . . . . . . . . 16
14243adantr 453 . . . . . . . . . . . . . . . . 17
143 rabss2 3428 . . . . . . . . . . . . . . . . 17
144142, 143syl 16 . . . . . . . . . . . . . . . 16
145141, 144eqsstrd 3384 . . . . . . . . . . . . . . 15
146 filss 17890 . . . . . . . . . . . . . . 15
14763, 119, 121, 145, 146syl13anc 1187 . . . . . . . . . . . . . 14
148 flimclsi 18015 . . . . . . . . . . . . . 14
149147, 148syl 16 . . . . . . . . . . . . 13
150 inss1 3563 . . . . . . . . . . . . . . 15
151150, 15sseldi 3348 . . . . . . . . . . . . . 14
152151adantr 453 . . . . . . . . . . . . 13
153149, 152sseldd 3351 . . . . . . . . . . . 12
154 ngpxms 18653 . . . . . . . . . . . . . . . . 17 NrmGrp
1552, 12xmsxmet 18491 . . . . . . . . . . . . . . . . 17
15622, 154, 1553syl 19 . . . . . . . . . . . . . . . 16
157156adantr 453 . . . . . . . . . . . . . . 15
1588adantr 453 . . . . . . . . . . . . . . 15
15968adantr 453 . . . . . . . . . . . . . . . 16
160159rexrd 9139 . . . . . . . . . . . . . . 15
161 eqid 2438 . . . . . . . . . . . . . . . 16
162 eqid 2438 . . . . . . . . . . . . . . . 16
163161, 162blcld 18540 . . . . . . . . . . . . . . 15
164157, 158, 160, 163syl3anc 1185 . . . . . . . . . . . . . 14
1659, 2, 12xmstopn 18486 . . . . . . . . . . . . . . . . 17
16622, 154, 1653syl 19 . . . . . . . . . . . . . . . 16
167166adantr 453 . . . . . . . . . . . . . . 15
168167fveq2d 5735 . . . . . . . . . . . . . 14
169164, 168eleqtrrd 2515 . . . . . . . . . . . . 13
170 cldcls 17111 . . . . . . . . . . . . 13
171169, 170syl 16 . . . . . . . . . . . 12
172153, 171eleqtrd 2514 . . . . . . . . . . 11
173 oveq2 6092 . . . . . . . . . . . . . 14
174173breq1d 4225 . . . . . . . . . . . . 13
175174elrab 3094 . . . . . . . . . . . 12
176175simprbi 452 . . . . . . . . . . 11
177172, 176syl 16 . . . . . . . . . 10
17832, 34, 32leadd2d 9626 . . . . . . . . . . . 12
17932recnd 9119 . . . . . . . . . . . . . 14
1801792timesd 10215 . . . . . . . . . . . . 13
181180breq1d 4225 . . . . . . . . . . . 12
182 lemuldiv2 9895 . . . . . . . . . . . . . 14
18379, 182mp3an3 1269 . . . . . . . . . . . . 13
18432, 67, 183syl2anc 644 . . . . . . . . . . . 12
185178, 181, 1843bitr2d 274 . . . . . . . . . . 11
186185biimpar 473 . . . . . . . . . 10
187177, 186syldan 458 . . . . . . . . 9
188187ex 425 . . . . . . . 8
18949, 188sylbird 228 . . . . . . 7
190189pm2.18d 106 . . . . . 6
191190adantr 453 . . . . 5
19286adantr 453 . . . . . . 7
19392adantr 453 . . . . . . 7
194 simpr 449 . . . . . . . . 9
195 fvex 5745 . . . . . . . . 9
196 eqid 2438 . . . . . . . . . 10
197196elrnmpt1 5122 . . . . . . . . 9
198194, 195, 197sylancl 645 . . . . . . . 8
199198, 10syl6eleqr 2529 . . . . . . 7
200 infmrlb 9994 . . . . . . 7
201192, 193, 199, 200syl3anc 1185 . . . . . 6
20211, 201syl5eqbr 4248 . . . . 5
20333, 35, 48, 191, 202letrd 9232 . . . 4
20427, 203eqbrtrrd 4237 . . 3
205204ralrimiva 2791 . 2
206 oveq2 6092 . . . . . 6
207206fveq2d 5735 . . . . 5
208207breq1d 4225 . . . 4
209208ralbidv 2727 . . 3
210209rspcev 3054 . 2
21116, 205, 210syl2anc 644 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 178   wa 360   wceq 1653   wcel 1726   wne 2601  wral 2707  wrex 2708  crab 2711  cvv 2958   cin 3321   wss 3322  c0 3630  cpw 3801  cuni 4017   class class class wbr 4215   cmpt 4269   cxp 4879  ccnv 4880   crn 4882   cres 4883  cfv 5457  (class class class)co 6084  csup 7448  cr 8994  cc0 8995   caddc 8998   cmul 9000  cxr 9124   clt 9125   cle 9126   cmin 9296   cdiv 9682  c2 10054  crp 10617  cexp 11387  cbs 13474   ↾s cress 13475  cds 13543  ctopn 13654  csg 14693  clmod 15955  clss 16013  cxmt 16691  cme 16692  cfbas 16694  cfg 16695  cmopn 16696  ccld 17085  ccl 17087  cfil 17882   cflim 17971  cxme 18352  cmt 18353  cnm 18629  NrmGrpcngp 18630  ccph 19134  CMetSpccms 19290 This theorem is referenced by:  minveclem5  19339 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4323  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-inf2 7599  ax-cnex 9051  ax-resscn 9052  ax-1cn 9053  ax-icn 9054  ax-addcl 9055  ax-addrcl 9056  ax-mulcl 9057  ax-mulrcl 9058  ax-mulcom 9059  ax-addass 9060  ax-mulass 9061  ax-distr 9062  ax-i2m1 9063  ax-1ne0 9064  ax-1rid 9065  ax-rnegex 9066  ax-rrecex 9067  ax-cnre 9068  ax-pre-lttri 9069  ax-pre-lttrn 9070  ax-pre-ltadd 9071  ax-pre-mulgt0 9072  ax-pre-sup 9073  ax-addf 9074  ax-mulf 9075 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-isom 5466  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-1st 6352  df-2nd 6353  df-tpos 6482  df-riota 6552  df-recs 6636  df-rdg 6671  df-1o 6727  df-oadd 6731  df-er 6908  df-map 7023  df-en 7113  df-dom 7114  df-sdom 7115  df-fin 7116  df-fi 7419  df-sup 7449  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131  df-sub 9298  df-neg 9299  df-div 9683  df-nn 10006  df-2 10063  df-3 10064  df-4 10065  df-5 10066  df-6 10067  df-7 10068  df-8 10069  df-9 10070  df-10 10071  df-n0 10227  df-z 10288  df-dec 10388  df-uz 10494  df-q 10580  df-rp 10618  df-xneg 10715  df-xadd 10716  df-xmul 10717  df-ico 10927  df-icc 10928  df-fz 11049  df-seq 11329  df-exp 11388  df-cj 11909  df-re 11910  df-im 11911  df-sqr 12045  df-abs 12046  df-struct 13476  df-ndx 13477  df-slot 13478  df-base 13479  df-sets 13480  df-ress 13481  df-plusg 13547  df-mulr 13548  df-starv 13549  df-sca 13550  df-vsca 13551  df-tset 13553  df-ple 13554  df-ds 13556  df-unif 13557  df-rest 13655  df-topgen 13672  df-0g 13732  df-mnd 14695  df-mhm 14743  df-grp 14817  df-minusg 14818  df-sbg 14819  df-mulg 14820  df-subg 14946  df-ghm 15009  df-cmn 15419  df-abl 15420  df-mgp 15654  df-rng 15668  df-cring 15669  df-ur 15670  df-oppr 15733  df-dvdsr 15751  df-unit 15752  df-invr 15782  df-dvr 15793  df-rnghom 15824  df-drng 15842  df-subrg 15871  df-staf 15938  df-srng 15939  df-lmod 15957  df-lss 16014  df-lmhm 16103  df-lvec 16180  df-sra 16249  df-rgmod 16250  df-psmet 16699  df-xmet 16700  df-met 16701  df-bl 16702  df-mopn 16703  df-fbas 16704  df-fg 16705  df-cnfld 16709  df-phl 16862  df-top 16968  df-bases 16970  df-topon 16971  df-topsp 16972  df-cld 17088  df-ntr 17089  df-cls 17090  df-nei 17167  df-haus 17384  df-fil 17883  df-flim 17976  df-xms 18355  df-ms 18356  df-nm 18635  df-ngp 18636  df-nlm 18639  df-clm 19093  df-cph 19136  df-cfil 19213  df-cmet 19215  df-cms 19293
 Copyright terms: Public domain W3C validator