# Metamath Proof Explorer

## Theorem cncms

Description: The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Assertion cncms fld ∈ CMetSp

### Proof

Step Hyp Ref Expression
1 cnfldms fld ∈ MetSp
2 eqid ( abs ∘ − ) = ( abs ∘ − )
3 2 cncmet ( abs ∘ − ) ∈ ( CMet ‘ ℂ )
4 cnfldbas ℂ = ( Base ‘ ℂfld )
5 cnmet ( abs ∘ − ) ∈ ( Met ‘ ℂ )
6 metf ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) → ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ )
7 5 6 ax-mp ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ
8 ffn ( ( abs ∘ − ) : ( ℂ × ℂ ) ⟶ ℝ → ( abs ∘ − ) Fn ( ℂ × ℂ ) )
9 fnresdm ( ( abs ∘ − ) Fn ( ℂ × ℂ ) → ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − ) )
10 7 8 9 mp2b ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( abs ∘ − )
11 cnfldds ( abs ∘ − ) = ( dist ‘ ℂfld )
12 11 reseq1i ( ( abs ∘ − ) ↾ ( ℂ × ℂ ) ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
13 10 12 eqtr3i ( abs ∘ − ) = ( ( dist ‘ ℂfld ) ↾ ( ℂ × ℂ ) )
14 4 13 iscms ( ℂfld ∈ CMetSp ↔ ( ℂfld ∈ MetSp ∧ ( abs ∘ − ) ∈ ( CMet ‘ ℂ ) ) )
15 1 3 14 mpbir2an fld ∈ CMetSp