# Metamath Proof Explorer

## Theorem recms

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

Ref Expression
Assertion recms ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 1 recld2 ${⊢}ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
3 cncms ${⊢}{ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}$
4 ax-resscn ${⊢}ℝ\subseteq ℂ$
5 df-refld ${⊢}{ℝ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{↾}_{𝑠}ℝ$
6 cnfldbas ${⊢}ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$
7 5 6 1 cmsss ${⊢}\left({ℂ}_{\mathrm{fld}}\in \mathrm{CMetSp}\wedge ℝ\subseteq ℂ\right)\to \left({ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}↔ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\right)$
8 3 4 7 mp2an ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}↔ℝ\in \mathrm{Clsd}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
9 2 8 mpbir ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$