cncmet

Description: The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2015)

		Ref	Expression
	Hypothesis	cncmet.1	$⊢ D = abs \circ -$
	Assertion	cncmet	$⊢ D \in CMet (ℂ)$

Proof

Step	Hyp	Ref	Expression
1		cncmet.1	$⊢ D = abs \circ -$
2		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
3	2	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
4	1	fveq2i	$⊢ MetOpen (D) = MetOpen (abs \circ -)$
5	3 4	eqtr4i	$⊢ TopOpen (ℂ_{fld}) = MetOpen (D)$
6		cnmet	$⊢ abs \circ - \in Met (ℂ)$
7	1 6	eqeltri	$⊢ D \in Met (ℂ)$
8	7	a1i	$⊢ ⊤ \to D \in Met (ℂ)$
9		1rp	$⊢ 1 \in ℝ^{+}$
10	9	a1i	$⊢ ⊤ \to 1 \in ℝ^{+}$
11	2	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
12		metxmet	$⊢ D \in Met (ℂ) \to D \in ∞Met (ℂ)$
13	7 12	ax-mp	$⊢ D \in ∞Met (ℂ)$
14		1xr	$⊢ 1 \in ℝ^{*}$
15		blssm	$⊢ (D \in ∞Met (ℂ) \land x \in ℂ \land 1 \in ℝ^{*}) \to x ball (D) 1 \subseteq ℂ$
16	13 14 15	mp3an13	$⊢ x \in ℂ \to x ball (D) 1 \subseteq ℂ$
17		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
18	17	clscld	$⊢ (TopOpen (ℂ_{fld}) \in Top \land x ball (D) 1 \subseteq ℂ) \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Clsd (TopOpen (ℂ_{fld}))$
19	11 16 18	sylancr	$⊢ x \in ℂ \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Clsd (TopOpen (ℂ_{fld}))$
20		abscl	$⊢ x \in ℂ \to \|x\| \in ℝ$
21		peano2re	$⊢ \|x\| \in ℝ \to \|x\| + 1 \in ℝ$
22	20 21	syl	$⊢ x \in ℂ \to \|x\| + 1 \in ℝ$
23		df-rab	$⊢ \{y \in ℂ \| x D y \leq 1\} = \{y \| (y \in ℂ \land x D y \leq 1)\}$
24	23	eqcomi	$⊢ \{y \| (y \in ℂ \land x D y \leq 1)\} = \{y \in ℂ \| x D y \leq 1\}$
25	5 24	blcls	$⊢ (D \in ∞Met (ℂ) \land x \in ℂ \land 1 \in ℝ^{*}) \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq \{y \| (y \in ℂ \land x D y \leq 1)\}$
26	13 14 25	mp3an13	$⊢ x \in ℂ \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq \{y \| (y \in ℂ \land x D y \leq 1)\}$
27		abscl	$⊢ y \in ℂ \to \|y\| \in ℝ$
28	27	ad2antrl	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y\| \in ℝ$
29	20	adantr	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|x\| \in ℝ$
30	28 29	resubcld	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y\| - \|x\| \in ℝ$
31		simpl	$⊢ (y \in ℂ \land x D y \leq 1) \to y \in ℂ$
32		id	$⊢ x \in ℂ \to x \in ℂ$
33		subcl	$⊢ (y \in ℂ \land x \in ℂ) \to y - x \in ℂ$
34	31 32 33	syl2anr	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to y - x \in ℂ$
35	34	abscld	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y - x\| \in ℝ$
36		1red	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to 1 \in ℝ$
37		simprl	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to y \in ℂ$
38		simpl	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to x \in ℂ$
39	37 38	abs2difd	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y\| - \|x\| \leq \|y - x\|$
40	1	cnmetdval	$⊢ (x \in ℂ \land y \in ℂ) \to x D y = \|x - y\|$
41		abssub	$⊢ (x \in ℂ \land y \in ℂ) \to \|x - y\| = \|y - x\|$
42	40 41	eqtrd	$⊢ (x \in ℂ \land y \in ℂ) \to x D y = \|y - x\|$
43	42	adantrr	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to x D y = \|y - x\|$
44		simprr	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to x D y \leq 1$
45	43 44	eqbrtrrd	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y - x\| \leq 1$
46	30 35 36 39 45	letrd	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y\| - \|x\| \leq 1$
47	28 29 36	lesubadd2d	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to (\|y\| - \|x\| \leq 1 \leftrightarrow \|y\| \leq \|x\| + 1)$
48	46 47	mpbid	$⊢ (x \in ℂ \land (y \in ℂ \land x D y \leq 1)) \to \|y\| \leq \|x\| + 1$
49	48	ex	$⊢ x \in ℂ \to ((y \in ℂ \land x D y \leq 1) \to \|y\| \leq \|x\| + 1)$
50	49	ss2abdv	$⊢ x \in ℂ \to \{y \| (y \in ℂ \land x D y \leq 1)\} \subseteq \{y \| \|y\| \leq \|x\| + 1\}$
51	26 50	sstrd	$⊢ x \in ℂ \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq \{y \| \|y\| \leq \|x\| + 1\}$
52		ssabral	$⊢ cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq \{y \| \|y\| \leq \|x\| + 1\} \leftrightarrow \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq \|x\| + 1$
53	51 52	sylib	$⊢ x \in ℂ \to \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq \|x\| + 1$
54		brralrspcev	$⊢ (\|x\| + 1 \in ℝ \land \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq \|x\| + 1) \to \exists r \in ℝ \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq r$
55	22 53 54	syl2anc	$⊢ x \in ℂ \to \exists r \in ℝ \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq r$
56	17	clsss3	$⊢ (TopOpen (ℂ_{fld}) \in Top \land x ball (D) 1 \subseteq ℂ) \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq ℂ$
57	11 16 56	sylancr	$⊢ x \in ℂ \to cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq ℂ$
58		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} cls (TopOpen (ℂ_{fld})) (x ball (D) 1) = TopOpen (ℂ_{fld}) ↾_{𝑡} cls (TopOpen (ℂ_{fld})) (x ball (D) 1)$
59	2 58	cnheibor	$⊢ cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \subseteq ℂ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Comp \leftrightarrow (cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Clsd (TopOpen (ℂ_{fld})) \land \exists r \in ℝ \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq r))$
60	57 59	syl	$⊢ x \in ℂ \to (TopOpen (ℂ_{fld}) ↾_{𝑡} cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Comp \leftrightarrow (cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Clsd (TopOpen (ℂ_{fld})) \land \exists r \in ℝ \forall y \in cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \|y\| \leq r))$
61	19 55 60	mpbir2and	$⊢ x \in ℂ \to TopOpen (ℂ_{fld}) ↾_{𝑡} cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Comp$
62	61	adantl	$⊢ (⊤ \land x \in ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} cls (TopOpen (ℂ_{fld})) (x ball (D) 1) \in Comp$
63	5 8 10 62	relcmpcmet	$⊢ ⊤ \to D \in CMet (ℂ)$
64	63	mptru	$⊢ D \in CMet (ℂ)$

Metamath Proof Explorer

Theorem cncmet

Proof