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 ⊢ 𝐷 = ( abs ∘ − )
Assertion cncmet 𝐷 ∈ ( CMet ‘ ℂ )

Proof

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