Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem dscmet 7856

Description: The discrete metric on any set . Definition 1.1-8 of [Kreyszig] p. 8. (Contributed by FL, 12-Oct-2006.)

Hypotheses

Ref	Expression
dscmet.1
dscmet.2

Assertion

Ref	Expression
dscmet	Met

Distinct variable group:   ,,,

---

Proof of Theorem dscmet

Step	Hyp	Ref	Expression
1		dscmet.1	. 2
2		dscmet.2	. . 3
3		0re 5412	. . . . 5
4		1re 5407	. . . . 5
5	3, 4	keepel 2389	. . . 4
6	5	a1i 8	. . 3
7	2, 6	foprab 4104	. 2
8	3, 4	keepel 2389	. . . . . 6
9	8	elisseti 1809	. . . . 5
10		eqeq1 1473	. . . . . 6
11	10	ifbid 2362	. . . . 5
12		eqeq2 1476	. . . . . 6
13	12	ifbid 2362	. . . . 5
14	9, 11, 13, 2	oprabval2 4013	. . . 4
15	14	eqeq1d 1475	. . 3
16		eqif 2367	. . . . . 6
17		pm3.26 319	. . . . . . 7
18		ax1ne0 5252	. . . . . . . . . . . 12
19		necom 1628	. . . . . . . . . . . 12
20	18, 19	mpbi 189	. . . . . . . . . . 11
21		df-ne 1579	. . . . . . . . . . 11
22	20, 21	mpbi 189	. . . . . . . . . 10
23	22	pm2.21i 77	. . . . . . . . 9
24	23	orcanai 688	. . . . . . . 8
25	24	ancoms 436	. . . . . . 7
26	17, 25	jaoi 341	. . . . . 6
27	16, 26	sylbi 199	. . . . 5
28	27	eqcoms 1470	. . . 4
29		iftrue 2356	. . . 4
30	28, 29	impbi 157	. . 3
31	15, 30	syl6bb 534	. 2
32		equtr 1127	. . . . . . . . 9
33	32	imdistani 443	. . . . . . . 8
34		iftrue 2356	. . . . . . . . . 10
35		iftrue 2356	. . . . . . . . . 10
36	34, 35	opreqan12d 3964	. . . . . . . . 9
37		0nn0 6060	. . . . . . . . . 10
38	3, 37	nn0addge1 6079	. . . . . . . . 9
39	36, 38	syl5breqr 2641	. . . . . . . 8
40	33, 39	syl 10	. . . . . . 7
41		equequ2 1131	. . . . . . . . . . 11
42	41	negbid 609	. . . . . . . . . 10
43	42	biimpcd 155	. . . . . . . . 9
44	43	imdistani 443	. . . . . . . 8
45		iffalse 2357	. . . . . . . . . 10
46		iffalse 2357	. . . . . . . . . 10
47	45, 46	opreqan12d 3964	. . . . . . . . 9
48		lt01 5653	. . . . . . . . . . 11
49	3, 4, 48	ltlei 5554	. . . . . . . . . 10
50	4, 4	addge0 5573	. . . . . . . . . 10
51	49, 49, 50	mp2an 695	. . . . . . . . 9
52	47, 51	syl5breqr 2641	. . . . . . . 8
53	44, 52	syl 10	. . . . . . 7
54	40, 53	pm2.61ian 475	. . . . . 6
55	29, 54	eqbrtrd 2625	. . . . 5
56		iffalse 2357	. . . . . 6
57		neeq1 1582	. . . . . . . . . . . 12
58	57	biimprd 154	. . . . . . . . . . 11
59		df-ne 1579	. . . . . . . . . . 11
60		df-ne 1579	. . . . . . . . . . 11
61	58, 59, 60	3imtr3g 550	. . . . . . . . . 10
62	61	imdistani 443	. . . . . . . . 9
63	34, 46	opreqan12d 3964	. . . . . . . . . . 11
64		ax1cn 5241	. . . . . . . . . . . 12
65	64	addid2 5303	. . . . . . . . . . 11
66	63, 65	syl6eq 1515	. . . . . . . . . 10
67	4	leid 5584	. . . . . . . . . 10
68	66, 67	syl5breqr 2641	. . . . . . . . 9
69	62, 68	syl 10	. . . . . . . 8
70	69	ex 373	. . . . . . 7
71	45, 35	opreqan12d 3964	. . . . . . . . . . 11
72	64	addid1 5302	. . . . . . . . . . 11
73	71, 72	syl6eq 1515	. . . . . . . . . 10
74	73, 67	syl5breqr 2641	. . . . . . . . 9
75		df-2 5917	. . . . . . . . . . 11
76	47, 75	syl6eqr 1517	. . . . . . . . . 10
77		2re 5926	. . . . . . . . . . 11
78		1lt2 5975	. . . . . . . . . . 11
79	4, 77, 78	ltlei 5554	. . . . . . . . . 10
80	76, 79	syl5breqr 2641	. . . . . . . . 9
81	74, 80	pm2.61dan 476	. . . . . . . 8
82	81	a1d 12	. . . . . . 7
83	70, 82	pm2.61i 126	. . . . . 6
84	56, 83	eqbrtrd 2625	. . . . 5
85	55, 84	pm2.61i 126	. . . 4
86	85	a1i 8	. . 3