Theorem recms

Description: The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017)

	Ref	Expression
Assertion	recms	⊢ ℝfld ∈ CMetSp

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
2	1	recld2	⊢ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) )
3		cncms	⊢ ℂfld ∈ CMetSp
4		ax-resscn	⊢ ℝ ⊆ ℂ
5		df-refld	⊢ ℝfld = ( ℂfld ↾s ℝ )
6		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
7	5 6 1	cmsss	⊢ ( ( ℂfld ∈ CMetSp ∧ ℝ ⊆ ℂ ) → ( ℝfld ∈ CMetSp ↔ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ) )
8	3 4 7	mp2an	⊢ ( ℝfld ∈ CMetSp ↔ ℝ ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
9	2 8	mpbir	⊢ ℝfld ∈ CMetSp