Theorem recusp

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

	Ref	Expression
Assertion	recusp	⊢ ℝfld ∈ CUnifSp

Proof

Step	Hyp	Ref	Expression
1		0re	⊢ 0 ∈ ℝ
2	1	ne0ii	⊢ ℝ ≠ ∅
3		recms	⊢ ℝfld ∈ CMetSp
4		reust	⊢ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) )
5		rebase	⊢ ℝ = ( Base ‘ ℝfld )
6		eqid	⊢ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) )
7		eqid	⊢ ( UnifSt ‘ ℝfld ) = ( UnifSt ‘ ℝfld )
8	5 6 7	cmetcusp1	⊢ ( ( ℝ ≠ ∅ ∧ ℝfld ∈ CMetSp ∧ ( UnifSt ‘ ℝfld ) = ( metUnif ‘ ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) ) ) ) → ℝfld ∈ CUnifSp )
9	2 3 4 8	mp3an	⊢ ℝfld ∈ CUnifSp