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

Theorem minveclem4 18798
 Description: Lemma for minvec 18802. 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 3392 . . 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 18796 . . 3
161, 15sseldi 3180 . 2
1712oveqi 5873 . . . . . . 7
182, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14minveclem4b 18797 . . . . . . . 8
198, 18ovresd 5990 . . . . . . 7
2017, 19syl5eq 2329 . . . . . 6
21 cphngp 18611 . . . . . . . 8 NrmGrp
225, 21syl 15 . . . . . . 7 NrmGrp
23 eqid 2285 . . . . . . . 8
244, 2, 3, 23ngpds 18127 . . . . . . 7 NrmGrp
2522, 8, 18, 24syl3anc 1182 . . . . . 6
2620, 25eqtrd 2317 . . . . 5
2726adantr 451 . . . 4
28 ngpms 18124 . . . . . . . 8 NrmGrp
292, 12msmet 18005 . . . . . . . 8
3022, 28, 293syl 18 . . . . . . 7
31 metcl 17899 . . . . . . 7
3230, 8, 18, 31syl3anc 1182 . . . . . 6
3332adantr 451 . . . . 5
342, 3, 4, 5, 6, 7, 8, 9, 10, 11minveclem4c 18791 . . . . . 6
3534adantr 451 . . . . 5
3622adantr 451 . . . . . 6 NrmGrp
37 cphlmod 18612 . . . . . . . . 9
385, 37syl 15 . . . . . . . 8
3938adantr 451 . . . . . . 7
408adantr 451 . . . . . . 7
41 eqid 2285 . . . . . . . . . 10
422, 41lssss 15696 . . . . . . . . 9
436, 42syl 15 . . . . . . . 8
4443sselda 3182 . . . . . . 7
452, 3lmodvsubcl 15672 . . . . . . 7
4639, 40, 44, 45syl3anc 1182 . . . . . 6
472, 4nmcl 18139 . . . . . 6 NrmGrp
4836, 46, 47syl2anc 642 . . . . 5
4934, 32ltnled 8968 . . . . . . . 8
502, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13minveclem3b 18794 . . . . . . . . . . . . . . . . . 18
51 fbsspw 17529 . . . . . . . . . . . . . . . . . . . 20
5250, 51syl 15 . . . . . . . . . . . . . . . . . . 19
53 sspwb 4225 . . . . . . . . . . . . . . . . . . . 20
5443, 53sylib 188 . . . . . . . . . . . . . . . . . . 19
5552, 54sstrd 3191 . . . . . . . . . . . . . . . . . 18
56 fvex 5541 . . . . . . . . . . . . . . . . . . . 20
572, 56eqeltri 2355 . . . . . . . . . . . . . . . . . . 19
5857a1i 10 . . . . . . . . . . . . . . . . . 18
59 fbasweak 17562 . . . . . . . . . . . . . . . . . 18
6050, 55, 58, 59syl3anc 1182 . . . . . . . . . . . . . . . . 17
6160adantr 451 . . . . . . . . . . . . . . . 16
62 fgcl 17575 . . . . . . . . . . . . . . . 16
6361, 62syl 15 . . . . . . . . . . . . . . 15
64 ssfg 17569 . . . . . . . . . . . . . . . . 17
6561, 64syl 15 . . . . . . . . . . . . . . . 16
66 minvec.t . . . . . . . . . . . . . . . . . . 19
6732, 34readdcld 8864 . . . . . . . . . . . . . . . . . . . . . . . 24
6867rehalfcld 9960 . . . . . . . . . . . . . . . . . . . . . . 23
6968resqcld 11273 . . . . . . . . . . . . . . . . . . . . . 22
7034resqcld 11273 . . . . . . . . . . . . . . . . . . . . . 22
7169, 70resubcld 9213 . . . . . . . . . . . . . . . . . . . . 21
7271adantr 451 . . . . . . . . . . . . . . . . . . . 20
7334, 32, 34ltadd1d 9367 . . . . . . . . . . . . . . . . . . . . . . 23
7434recnd 8863 . . . . . . . . . . . . . . . . . . . . . . . . 25
75742timesd 9956 . . . . . . . . . . . . . . . . . . . . . . . 24
7675breq1d 4035 . . . . . . . . . . . . . . . . . . . . . . 23
77 2re 9817 . . . . . . . . . . . . . . . . . . . . . . . . . 26
78 2pos 9830 . . . . . . . . . . . . . . . . . . . . . . . . . 26
7977, 78pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . 25
8079a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24
81 ltmuldiv2 9629 . . . . . . . . . . . . . . . . . . . . . . . 24
8234, 67, 80, 81syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . 23
8373, 76, 823bitr2d 272 . . . . . . . . . . . . . . . . . . . . . 22
842, 3, 4, 5, 6, 7, 8, 9, 10minveclem1 18790 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8584simp3d 969 . . . . . . . . . . . . . . . . . . . . . . . . 25
8684simp1d 967 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8784simp2d 968 . . . . . . . . . . . . . . . . . . . . . . . . . 26
88 0re 8840 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
89 breq1 4028 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9089ralbidv 2565 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9190rspcev 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9288, 85, 91sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9388a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26
94 infmrgelb 9736 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9586, 87, 92, 93, 94syl31anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . 25
9685, 95mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . 24
9796, 11syl6breqr 4065 . . . . . . . . . . . . . . . . . . . . . . 23
98 metge0 17912 . . . . . . . . . . . . . . . . . . . . . . . . . 26
9930, 8, 18, 98syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . . . 25
10032, 34, 99, 97addge0d 9350 . . . . . . . . . . . . . . . . . . . . . . . 24
101 divge0 9627 . . . . . . . . . . . . . . . . . . . . . . . 24
10267, 100, 80, 101syl21anc 1181 . . . . . . . . . . . . . . . . . . . . . . 23
10334, 68, 97, 102lt2sqd 11281 . . . . . . . . . . . . . . . . . . . . . 22
10470, 69posdifd 9361 . . . . . . . . . . . . . . . . . . . . . 22
10583, 103, 1043bitrd 270 . . . . . . . . . . . . . . . . . . . . 21
106105biimpa 470 . . . . . . . . . . . . . . . . . . . 20
10772, 106elrpd 10390 . . . . . . . . . . . . . . . . . . 19
10866, 107syl5eqel 2369 . . . . . . . . . . . . . . . . . 18
1096adantr 451 . . . . . . . . . . . . . . . . . . 19
110 rabexg 4166 . . . . . . . . . . . . . . . . . . 19
111109, 110syl 15 . . . . . . . . . . . . . . . . . 18
112 eqid 2285 . . . . . . . . . . . . . . . . . . 19
113 oveq2 5868 . . . . . . . . . . . . . . . . . . . . 21
114113breq2d 4037 . . . . . . . . . . . . . . . . . . . 20
115114rabbidv 2782 . . . . . . . . . . . . . . . . . . 19
116112, 115elrnmpt1s 4929 . . . . . . . . . . . . . . . . . 18
117108, 111, 116syl2anc 642 . . . . . . . . . . . . . . . . 17
118117, 13syl6eleqr 2376 . . . . . . . . . . . . . . . 16
11965, 118sseldd 3183 . . . . . . . . . . . . . . 15
120 ssrab2 3260 . . . . . . . . . . . . . . . 16
121120a1i 10 . . . . . . . . . . . . . . 15
12266oveq2i 5871 . . . . . . . . . . . . . . . . . . . 20
12370ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . 22
124123recnd 8863 . . . . . . . . . . . . . . . . . . . . 21
12568ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23
126125resqcld 11273 . . . . . . . . . . . . . . . . . . . . . 22
127126recnd 8863 . . . . . . . . . . . . . . . . . . . . 21
128124, 127pncan3d 9162 . . . . . . . . . . . . . . . . . . . 20
129122, 128syl5eq 2329 . . . . . . . . . . . . . . . . . . 19
130129breq2d 4037 . . . . . . . . . . . . . . . . . 18
13130ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20
1328ad2antrr 706 . . . . . . . . . . . . . . . . . . . 20
13344adantlr 695 . . . . . . . . . . . . . . . . . . . 20
134 metcl 17899 . . . . . . . . . . . . . . . . . . . 20
135131, 132, 133, 134syl3anc 1182 . . . . . . . . . . . . . . . . . . 19
136 metge0 17912 . . . . . . . . . . . . . . . . . . . 20
137131, 132, 133, 136syl3anc 1182 . . . . . . . . . . . . . . . . . . 19
138102ad2antrr 706 . . . . . . . . . . . . . . . . . . 19
139135, 125, 137, 138le2sqd 11282 . . . . . . . . . . . . . . . . . 18
140130, 139bitr4d 247 . . . . . . . . . . . . . . . . 17
141140rabbidva 2781 . . . . . . . . . . . . . . . 16
14243adantr 451 . . . . . . . . . . . . . . . . 17
143 rabss2 3258 . . . . . . . . . . . . . . . . 17
144142, 143syl 15 . . . . . . . . . . . . . . . 16
145141, 144eqsstrd 3214 . . . . . . . . . . . . . . 15
146 filss 17550 . . . . . . . . . . . . . . 15
14763, 119, 121, 145, 146syl13anc 1184 . . . . . . . . . . . . . 14
148 flimclsi 17675 . . . . . . . . . . . . . 14
149147, 148syl 15 . . . . . . . . . . . . 13
150 inss1 3391 . . . . . . . . . . . . . . 15
151150, 15sseldi 3180 . . . . . . . . . . . . . 14
152151adantr 451 . . . . . . . . . . . . 13
153149, 152sseldd 3183 . . . . . . . . . . . 12
154 ngpxms 18125 . . . . . . . . . . . . . . . . 17 NrmGrp
1552, 12xmsxmet 18004 . . . . . . . . . . . . . . . . 17
15622, 154, 1553syl 18 . . . . . . . . . . . . . . . 16
157156adantr 451 . . . . . . . . . . . . . . 15
1588adantr 451 . . . . . . . . . . . . . . 15
15968adantr 451 . . . . . . . . . . . . . . . 16
160159rexrd 8883 . . . . . . . . . . . . . . 15
161 eqid 2285 . . . . . . . . . . . . . . . 16
162 eqid 2285 . . . . . . . . . . . . . . . 16
163161, 162blcld 18053 . . . . . . . . . . . . . . 15
164157, 158, 160, 163syl3anc 1182 . . . . . . . . . . . . . 14
1659, 2, 12xmstopn 17999 . . . . . . . . . . . . . . . . 17
16622, 154, 1653syl 18 . . . . . . . . . . . . . . . 16
167166adantr 451 . . . . . . . . . . . . . . 15
168167fveq2d 5531 . . . . . . . . . . . . . 14
169164, 168eleqtrrd 2362 . . . . . . . . . . . . 13
170 cldcls 16781 . . . . . . . . . . . . 13
171169, 170syl 15 . . . . . . . . . . . 12
172153, 171eleqtrd 2361 . . . . . . . . . . 11
173 oveq2 5868 . . . . . . . . . . . . . 14
174173breq1d 4035 . . . . . . . . . . . . 13
175174elrab 2925 . . . . . . . . . . . 12
176175simprbi 450 . . . . . . . . . . 11
177172, 176syl 15 . . . . . . . . . 10
17832, 34, 32leadd2d 9369 . . . . . . . . . . . 12
17932recnd 8863 . . . . . . . . . . . . . 14
1801792timesd 9956 . . . . . . . . . . . . 13
181180breq1d 4035 . . . . . . . . . . . 12
182 lemuldiv2 9638 . . . . . . . . . . . . . 14
18379, 182mp3an3 1266 . . . . . . . . . . . . 13
18432, 67, 183syl2anc 642 . . . . . . . . . . . 12
185178, 181, 1843bitr2d 272 . . . . . . . . . . 11
186185biimpar 471 . . . . . . . . . 10
187177, 186syldan 456 . . . . . . . . 9
188187ex 423 . . . . . . . 8
18949, 188sylbird 226 . . . . . . 7
190189pm2.18d 103 . . . . . 6
191190adantr 451 . . . . 5
19286adantr 451 . . . . . . 7
19392adantr 451 . . . . . . 7
194 simpr 447 . . . . . . . . 9
195 fvex 5541 . . . . . . . . 9
196 eqid 2285 . . . . . . . . . 10
197196elrnmpt1 4930 . . . . . . . . 9
198194, 195, 197sylancl 643 . . . . . . . 8
199198, 10syl6eleqr 2376 . . . . . . 7
200 infmrlb 9737 . . . . . . 7
201192, 193, 199, 200syl3anc 1182 . . . . . 6
20211, 201syl5eqbr 4058 . . . . 5
20333, 35, 48, 191, 202letrd 8975 . . . 4
20427, 203eqbrtrrd 4047 . . 3
205204ralrimiva 2628 . 2
206 oveq2 5868 . . . . . 6
207206fveq2d 5531 . . . . 5
208207breq1d 4035 . . . 4
209208ralbidv 2565 . . 3
210209rspcev 2886 . 2
21116, 205, 210syl2anc 642 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   wceq 1625   wcel 1686   wne 2448  wral 2545  wrex 2546  crab 2549  cvv 2790   cin 3153   wss 3154  c0 3457  cpw 3627  cuni 3829   class class class wbr 4025   cmpt 4079   cxp 4689  ccnv 4690   crn 4692   cres 4693  cfv 5257  (class class class)co 5860  csup 7195  cr 8738  cc0 8739   caddc 8742   cmul 8744  cxr 8868   clt 8869   cle 8870   cmin 9039   cdiv 9425  c2 9797  crp 10356  cexp 11106  cbs 13150   ↾s cress 13151  cds 13219  ctopn 13328  csg 14367  clmod 15629  clss 15691  cxmt 16371  cme 16372  cmopn 16374  ccld 16755  ccl 16757  cfbas 17520  cfg 17521  cfil 17542   cflim 17631  cxme 17884  cmt 17885  cnm 18101  NrmGrpcngp 18102  ccph 18604  CMetSpccms 18756 This theorem is referenced by:  minveclem5  18799 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-inf2 7344  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816  ax-pre-sup 8817  ax-addf 8818  ax-mulf 8819 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-isom 5266  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-tpos 6236  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-oadd 6485  df-er 6662  df-map 6776  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-fi 7167  df-sup 7196  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-div 9426  df-nn 9749  df-2 9806  df-3 9807  df-4 9808  df-5 9809  df-6 9810  df-7 9811  df-8 9812  df-9 9813  df-10 9814  df-n0 9968  df-z 10027  df-dec 10127  df-uz 10233  df-q 10319  df-rp 10357  df-xneg 10454  df-xadd 10455  df-xmul 10456  df-ico 10664  df-icc 10665  df-fz 10785  df-seq 11049  df-exp 11107  df-cj 11586  df-re 11587  df-im 11588  df-sqr 11722  df-abs 11723  df-struct 13152  df-ndx 13153  df-slot 13154  df-base 13155  df-sets 13156  df-ress 13157  df-plusg 13223  df-mulr 13224  df-starv 13225  df-sca 13226  df-vsca 13227  df-tset 13229  df-ple 13230  df-ds 13232  df-rest 13329  df-topgen 13346  df-0g 13406  df-mnd 14369  df-mhm 14417  df-grp 14491  df-minusg 14492  df-sbg 14493  df-mulg 14494  df-subg 14620  df-ghm 14683  df-cmn 15093  df-abl 15094  df-mgp 15328  df-rng 15342  df-cring 15343  df-ur 15344  df-oppr 15407  df-dvdsr 15425  df-unit 15426  df-invr 15456  df-dvr 15467  df-rnghom 15498  df-drng 15516  df-subrg 15545  df-staf 15612  df-srng 15613  df-lmod 15631  df-lss 15692  df-lmhm 15781  df-lvec 15858  df-sra 15927  df-rgmod 15928  df-xmet 16375  df-met 16376  df-bl 16377  df-mopn 16378  df-cnfld 16380  df-phl 16532  df-top 16638  df-bases 16640  df-topon 16641  df-topsp 16642  df-cld 16758  df-ntr 16759  df-cls 16760  df-nei 16837  df-haus 17045  df-fbas 17522  df-fg 17523  df-fil 17543  df-flim 17636  df-xms 17887  df-ms 17888  df-nm 18107  df-ngp 18108  df-nlm 18111  df-clm 18563  df-cph 18606  df-cfil 18683  df-cmet 18685  df-cms 18759
 Copyright terms: Public domain W3C validator