metdcn - Mathbox for Jeff Madsen

Mathbox for Jeff Madsen

< Previous Next >
Related theorems
Unicode version

Theorem metdcn 15853

Description: The function which gives the distance to a fixed point in a metric space is a continuous function into nonnegative reals.

**Hypotheses**
Ref	Expression
metdcn.1
metdcn.2	Open
metdcn.3	Open [,) [,)
metdcn.4	$/\$

**Assertion**
Ref	Expression
metdcn	Met $/\$ Cn

Distinct variable groups:

**Proof of Theorem metdcn**
Step	Hyp	Ref	Expression
1		eqid 1884	. . . . . 6
2	1	cnmet 9182	. . . . 5 Met
3		metres 9100	. . . . 5 Met [,) [,) Met
4	2, 3	ax-mp 7	. . . 4 [,) [,) Met
5		metdcn.1	. . . . 5
6		metdcn.2	. . . . 5 Open
7		elnnr 15803	. . . . . . . . 9 [,) $/\$
8	7	simplbi 349	. . . . . . . 8 [,)
9	8	ssriv 2621	. . . . . . 7 [,)
10		axresscn 6420	. . . . . . 7
11	9, 10	sstri 2626	. . . . . 6 [,)
12	1	cnmetba 9181	. . . . . . 7
13	12	metssba2 9087	. . . . . 6 Met $/\$ [,) [,) [,) [,)
14	2, 11, 13	mp2an 761	. . . . 5 [,) [,) [,)
15		metdcn.3	. . . . 5 Open [,) [,)
16	5, 6, 14, 15	metcn 9167	. . . 4 Met $/\$ [,) [,) Met Cn [,) $/\$ $/\$ [,) [,)
17	4, 16	mpan2 760	. . 3 Met Cn [,) $/\$ $/\$ [,) [,)
18	17	adantr 425	. 2 Met $/\$ Cn [,) $/\$ $/\$ [,) [,)
19		elnnr 15803	. . . . . 6 [,) $/\$
20	5	metcl 9088	. . . . . 6 Met $/\$ $/\$
21	5	metge0 9096	. . . . . 6 Met $/\$ $/\$
22	19, 20, 21	sylanbrc 527	. . . . 5 Met $/\$ $/\$ [,)
23	22	3expa 1067	. . . 4 Met $/\$ $/\$ [,)
24	23	r19.21aiva 2176	. . 3 Met $/\$ [,)
25		metdcn.4	. . . 4 $/\$
26	25	fopab2 4796	. . 3 [,) [,)
27	24, 26	sylib 215	. 2 Met $/\$ [,)
28		simplrr 455	. . . . 5 Met $/\$ $/\$ $/\$ $/\$
29		simpr 350	. . . . 5 Met $/\$ $/\$ $/\$ $/\$
30		opreq2 4890	. . . . . . . . . . . . . 14
31		oprex 4907	. . . . . . . . . . . . . 14
32	30, 25, 31	fvopab4 4743	. . . . . . . . . . . . 13
33	32	ad2antrl 442	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$
34	33	ad2antrr 440	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$
35		opreq2 4890	. . . . . . . . . . . . 13
36		oprex 4907	. . . . . . . . . . . . 13
37	35, 25, 36	fvopab4 4743	. . . . . . . . . . . 12
38	37	ad2antlr 441	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$
39	34, 38	opreq12d 4900	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$ $/\$ [,) [,) [,) [,)
40		elnnr 15803	. . . . . . . . . . . . . . . 16 [,) $/\$
41	5	metcl 9088	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$
42	5	metge0 9096	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$
43	40, 41, 42	sylanbrc 527	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ [,)
44	43	3expa 1067	. . . . . . . . . . . . . 14 Met $/\$ $/\$ [,)
45	44	adantr 425	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ [,)
46		elnnr 15803	. . . . . . . . . . . . . . . 16 [,) $/\$
47	5	metcl 9088	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$
48	5	metge0 9096	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$
49	46, 47, 48	sylanbrc 527	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ [,)
50	49	3expa 1067	. . . . . . . . . . . . . 14 Met $/\$ $/\$ [,)
51	50	adantlr 429	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ [,)
52		oprvres 4963	. . . . . . . . . . . . 13 [,) $/\$ [,) [,) [,)
53	45, 51, 52	syl11anc 524	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ [,) [,)
54	53	adantlrr 435	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ [,) [,)
55	54	adantr 425	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$ $/\$ [,) [,)
56	39, 55	eqtrd 1925	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$ [,) [,)
57	41	recnd 6468	. . . . . . . . . . . . . . 15 Met $/\$ $/\$
58	57	3expa 1067	. . . . . . . . . . . . . 14 Met $/\$ $/\$
59	58	adantr 425	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$
60	47	recnd 6468	. . . . . . . . . . . . . . 15 Met $/\$ $/\$
61	60	3expa 1067	. . . . . . . . . . . . . 14 Met $/\$ $/\$
62	61	adantlr 429	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$
63	1	cnmetdval 9180	. . . . . . . . . . . . 13 $/\$
64	59, 62, 63	syl11anc 524	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$
65	64	adantlrr 435	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$
66	65	adantr 425	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$ $/\$
67	41	3expa 1067	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$
68	67	adantr 425	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$
69	47	3expa 1067	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$
70	69	adantlr 429	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$
71		resubcl 6601	. . . . . . . . . . . . . . 15 $/\$
72	68, 70, 71	syl11anc 524	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$
73	72	adantlrr 435	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$
74		simplrr 455	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$
75		abslt 8132	. . . . . . . . . . . . 13 $/\$ $/\$
76	73, 74, 75	syl11anc 524	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$ $/\$
77	76	adantr 425	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
78	5	mettri 9094	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$ $/\$
79	78	3exp2 1086	. . . . . . . . . . . . . . . . . . 19 Met
80	79	imp41 395	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$ $/\$
81	80	an1rs 547	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$
82	5	metcl 9088	. . . . . . . . . . . . . . . . . . . 20 Met $/\$ $/\$
83	82	3expa 1067	. . . . . . . . . . . . . . . . . . 19 Met $/\$ $/\$
84	83	adantllr 433	. . . . . . . . . . . . . . . . . 18 Met $/\$ $/\$ $/\$
85		lesubadd2 6813	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
86	70, 68, 84, 85	syl111anc 1100	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$
87	81, 86	mpbird 213	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$
88	87	adantlrr 435	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$ $/\$
89		resubcl 6601	. . . . . . . . . . . . . . . . . 18 $/\$
90	70, 68, 89	syl11anc 524	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$
91	90	adantlrr 435	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$
92	84	adantlrr 435	. . . . . . . . . . . . . . . 16 Met $/\$ $/\$ $/\$ $/\$
93		lelttr 6693	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
94	91, 92, 74, 93	syl111anc 1100	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$ $/\$ $/\$
95	88, 94	mpand 765	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$
96	95	imp 377	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$ $/\$
97		ltneg 6844	. . . . . . . . . . . . . . 15 $/\$
98	91, 74, 97	syl11anc 524	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$ $/\$
99	98	adantr 425	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$ $/\$
100	96, 99	mpbid 212	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$ $/\$
101		negsubdi2 6623	. . . . . . . . . . . . . . 15 $/\$
102	62, 59, 101	syl11anc 524	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$
103	102	adantlrr 435	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$
104	103	adantr 425	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$ $/\$
105	100, 104	breqtrd 3361	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$
106	5	mettri3 9095	. . . . . . . . . . . . . . . . 17 Met $/\$ $/\$ $/\$
107	106	3exp2 1086	. . . . . . . . . . . . . . . 16 Met
108	107	imp41 395	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$
109		lesubadd2 6813	. . . . . . . . . . . . . . . 16 $/\$ $/\$
110	68, 70, 84, 109	syl111anc 1100	. . . . . . . . . . . . . . 15 Met $/\$ $/\$ $/\$
111	108, 110	mpbird 213	. . . . . . . . . . . . . 14 Met $/\$ $/\$ $/\$
112	111	adantlrr 435	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$
113		lelttr 6693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
114	73, 92, 74, 113	syl111anc 1100	. . . . . . . . . . . . 13 Met $/\$ $/\$ $/\$ $/\$ $/\$
115	112, 114	mpand 765	. . . . . . . . . . . 12 Met $/\$ $/\$ $/\$ $/\$
116	115	imp 377	. . . . . . . . . . 11 Met $/\$ $/\$ $/\$ $/\$ $/\$
117	77, 105, 116	mpbir2and 802	. . . . . . . . . 10 Met $/\$ $/\$ $/\$ $/\$ $/\$
118	66, 117	eqbrtrd 3357	. . . . . . . . 9 Met $/\$ $/\$ $/\$ $/\$ $/\$
119	56, 118	eqbrtrd 3357	. . . . . . . 8 Met $/\$ $/\$ $/\$ $/\$ $/\$ [,) [,)
120	119	ex 402	. . . . . . 7 Met $/\$ $/\$ $/\$ $/\$ [,) [,)
121	120	adantlr 429	. . . . . 6 Met $/\$ $/\$ $/\$ $/\$ $/\$ [,) [,)
122	121	r19.21aiva 2176	. . . . 5 Met $/\$ $/\$ $/\$ $/\$ [,) [,)
123		breq2 3342	. . . . . . 7
124		breq2 3342	. . . . . . . . 9
125	124	imbi1d 675	. . . . . . . 8 [,) [,) [,) [,)
126	125	ralbidv 2123	. . . . . . 7 [,) [,) [,) [,)
127	123, 126	anbi12d 690	. . . . . 6 $/\$ [,) [,) $/\$ [,) [,)
128	127	rcla4ev 2381	. . . . 5 $/\$ $/\$ [,) [,) $/\$ [,) [,)
129	28, 29, 122, 128	syl12anc 1098	. . . 4 Met $/\$ $/\$ $/\$ $/\$ $/\$ [,) [,)
130	129	exp31 407	. . 3 Met $/\$ $/\$ $/\$ [,) [,)
131	130	r19.21aivv 2183	. 2 Met $/\$ $/\$ [,) [,)
132	18, 27, 131	mpbir2and 802	1 Met $/\$ Cn

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wral 2105

wrex 2106

wss 2593 class class class wbr 3338

copab 3395

cxp 3984

cdm 3986

cres 3988

ccom 3990

wf 3994

cfv 3998 (class class class)co 4884

cc 6384

cr 6385

cc0 6386

caddc 6389

cmin 6445

cneg 6446

cle 6448

cpnf 6650

clt 6653 [,)cico 7526

cabs 8000 Cn ccn 9028 Metcme 9066 Opencopn 9069

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-nel 2020 df-ral 2109 df-rex 2110 df-reu 2111 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-int 3215 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-opr 4886 df-oprab 4887 df-mpt 5006 df-1st 5020 df-2nd 5021 df-iota 5089 df-rdg 5140 df-1o 5177 df-oadd 5179 df-omul 5180 df-er 5318 df-ec 5320 df-qs 5323 df-map 5383 df-en 5427 df-dom 5428 df-sdom 5429 df-undef 5556 df-riota 5560 df-sup 5664 df-ni 6152 df-pli 6153 df-mi 6154 df-lti 6155 df-plpq 6187 df-mpq 6188 df-enq 6189 df-nq 6190 df-plq 6191 df-mq 6192 df-rq 6193 df-ltq 6194 df-1q 6195 df-np 6238 df-1p 6239 df-plp 6240 df-mp 6241 df-ltp 6242 df-plpr 6316 df-mpr 6317 df-enr 6318 df-nr 6319 df-plr 6320 df-mr 6321 df-ltr 6322 df-0r 6323 df-1r 6324 df-m1r 6325 df-c 6392 df-0 6393 df-1 6394 df-i 6395 df-r 6396 df-plus 6397 df-mul 6398 df-lt 6399 df-sub 6511 df-neg 6513 df-pnf 6654 df-mnf 6655 df-xr 6656 df-ltxr 6657 df-le 6658 df-div 6892 df-n 7108 df-2 7154 df-n0 7309 df-z 7345 df-ico 7530 df-seq1 7721 df-exp 7812 df-sqr 7920 df-re 8001 df-im 8002 df-cj 8003 df-abs 8004 df-top 8861 df-cn 9030 df-cnp 9031 df-met 9070 df-bl 9072 df-opn 9073