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⁡If:ℕ⟶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⁡If:ℕ⟶X→f∈dom⁡⇝t⁡MetOpen⁡ℝn⁡I
15 10 14 mpbird ⊢I∈Fin→ℝn⁡I∈CMet⁡X