# Metamath Proof Explorer

## Theorem recusp

Description: The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017)

Ref Expression
Assertion recusp ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$

### Proof

Step Hyp Ref Expression
1 0re ${⊢}0\in ℝ$
2 1 ne0ii ${⊢}ℝ\ne \varnothing$
3 recms ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}$
4 reust ${⊢}\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)↾}_{{ℝ}^{2}}\right)$
5 rebase ${⊢}ℝ={\mathrm{Base}}_{{ℝ}_{\mathrm{fld}}}$
6 eqid ${⊢}{\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)↾}_{{ℝ}^{2}}={\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)↾}_{{ℝ}^{2}}$
7 eqid ${⊢}\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)$
8 5 6 7 cmetcusp1 ${⊢}\left(ℝ\ne \varnothing \wedge {ℝ}_{\mathrm{fld}}\in \mathrm{CMetSp}\wedge \mathrm{UnifSt}\left({ℝ}_{\mathrm{fld}}\right)=\mathrm{metUnif}\left({\mathrm{dist}\left({ℝ}_{\mathrm{fld}}\right)↾}_{{ℝ}^{2}}\right)\right)\to {ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$
9 2 3 4 8 mp3an ${⊢}{ℝ}_{\mathrm{fld}}\in \mathrm{CUnifSp}$