# 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
`|- CCfld e. CMetSp`

### Proof

Step Hyp Ref Expression
1 cnfldms
` |-  CCfld e. MetSp`
2 eqid
` |-  ( abs o. - ) = ( abs o. - )`
3 2 cncmet
` |-  ( abs o. - ) e. ( CMet ` CC )`
4 cnfldbas
` |-  CC = ( Base ` CCfld )`
5 cnmet
` |-  ( abs o. - ) e. ( Met ` CC )`
6 metf
` |-  ( ( abs o. - ) e. ( Met ` CC ) -> ( abs o. - ) : ( CC X. CC ) --> RR )`
7 5 6 ax-mp
` |-  ( abs o. - ) : ( CC X. CC ) --> RR`
8 ffn
` |-  ( ( abs o. - ) : ( CC X. CC ) --> RR -> ( abs o. - ) Fn ( CC X. CC ) )`
9 fnresdm
` |-  ( ( abs o. - ) Fn ( CC X. CC ) -> ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - ) )`
10 7 8 9 mp2b
` |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( abs o. - )`
11 cnfldds
` |-  ( abs o. - ) = ( dist ` CCfld )`
12 11 reseq1i
` |-  ( ( abs o. - ) |` ( CC X. CC ) ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )`
13 10 12 eqtr3i
` |-  ( abs o. - ) = ( ( dist ` CCfld ) |` ( CC X. CC ) )`
14 4 13 iscms
` |-  ( CCfld e. CMetSp <-> ( CCfld e. MetSp /\ ( abs o. - ) e. ( CMet ` CC ) ) )`
15 1 3 14 mpbir2an
` |-  CCfld e. CMetSp`