# Metamath Proof Explorer

## Theorem 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}=\mathrm{abs}\circ -$
Assertion cncmet ${⊢}{D}\in \mathrm{CMet}\left(ℂ\right)$

### Proof

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