Metamath Proof Explorer


Theorem hcaucvg

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

Ref Expression
Assertion hcaucvg ( ( 𝐹 ∈ Cauchy ∧ 𝐴 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 hcau ( 𝐹 ∈ Cauchy ↔ ( 𝐹 : ℕ ⟶ ℋ ∧ ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ) )
2 1 simprbi ( 𝐹 ∈ Cauchy → ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 )
3 breq2 ( 𝑥 = 𝐴 → ( ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ↔ ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝐴 ) )
4 3 rexralbidv ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥 ↔ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝐴 ) )
5 4 rspccva ( ( ∀ 𝑥 ∈ ℝ+𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝑥𝐴 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝐴 )
6 2 5 sylan ( ( 𝐹 ∈ Cauchy ∧ 𝐴 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ𝑦 ) ( norm ‘ ( ( 𝐹𝑦 ) − ( 𝐹𝑧 ) ) ) < 𝐴 )