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