Metamath Proof Explorer


Theorem seq1hcau

Description: A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion seq1hcau ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ∈ Cauchy ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )

Proof

Step Hyp Ref Expression
1 hcau ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
2 1 baib ( 𝐹 : ℕ ⟶ ℋ → ( 𝐹 ∈ Cauchy ↔ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )