Metamath Proof Explorer

Theorem rrncms

Description: Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

Ref Expression
Hypothesis rrncms.1 ⊢ X = ℝ I
Assertion rrncms ⊢ I ∈ Fin → ℝ n ⁡ I ∈ CMet ⁡ X

Proof

Step Hyp Ref Expression
1 rrncms.1 ⊢ X = ℝ I
2 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
3 eqid ⊢ MetOpen ⁡ ℝ n ⁡ I = MetOpen ⁡ ℝ n ⁡ I
4 simpll ⊢ I ∈ Fin ∧ f ∈ Cau ⁡ ℝ n ⁡ I ∧ f : ℕ ⟶ X → I ∈ Fin
5 simplr ⊢ I ∈ Fin ∧ f ∈ Cau ⁡ ℝ n ⁡ I ∧ f : ℕ ⟶ X → f ∈ Cau ⁡ ℝ n ⁡ I
6 simpr ⊢ I ∈ Fin ∧ f ∈ Cau ⁡ ℝ n ⁡ I ∧ f : ℕ ⟶ X → f : ℕ ⟶ X
7 eqid ⊢ m ∈ I ⟼ ⇝ ⁡ t ∈ ℕ ⟼ f ⁡ t ⁡ m = m ∈ I ⟼ ⇝ ⁡ t ∈ ℕ ⟼ f ⁡ t ⁡ m
8 1 2 3 4 5 6 7 rrncmslem ⊢ I ∈ Fin ∧ f ∈ Cau ⁡ ℝ n ⁡ I ∧ f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ ℝ n ⁡ I
9 8 ex ⊢ I ∈ Fin ∧ f ∈ Cau ⁡ ℝ n ⁡ I → f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ ℝ n ⁡ I
10 9 ralrimiva ⊢ I ∈ Fin → ∀ f ∈ Cau ⁡ ℝ n ⁡ I f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ ℝ n ⁡ I
11 nnuz ⊢ ℕ = ℤ ≥ 1
12 1zzd ⊢ I ∈ Fin → 1 ∈ ℤ
13 1 rrnmet ⊢ I ∈ Fin → ℝ n ⁡ I ∈ Met ⁡ X
14 11 3 12 13 iscmet3 ⊢ I ∈ Fin → ℝ n ⁡ I ∈ CMet ⁡ X ↔ ∀ f ∈ Cau ⁡ ℝ n ⁡ I f : ℕ ⟶ X → f ∈ dom ⁡ ⇝t ⁡ MetOpen ⁡ ℝ n ⁡ I
15 10 14 mpbird ⊢ I ∈ Fin → ℝ n ⁡ I ∈ CMet ⁡ X