This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hlimconvi

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

Ref Expression
Hypothesis hlim.1 ⊢ A ∈ V
Assertion hlimconvi ⊢ F ⇝v A ∧ B ∈ ℝ + → ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < B

Proof

Step Hyp Ref Expression
1 hlim.1 ⊢ A ∈ V
2 1 hlimi ⊢ F ⇝v A ↔ F : ℕ ⟶ ℋ ∧ A ∈ ℋ ∧ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
3 2 simprbi ⊢ F ⇝v A → ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x
4 breq2 ⊢ x = B → norm ℎ ⁡ F ⁡ z - ℎ A < x ↔ norm ℎ ⁡ F ⁡ z - ℎ A < B
5 4 rexralbidv ⊢ x = B → ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x ↔ ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < B
6 5 rspccva ⊢ ∀ x ∈ ℝ + ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < x ∧ B ∈ ℝ + → ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < B
7 3 6 sylan ⊢ F ⇝v A ∧ B ∈ ℝ + → ∃ y ∈ ℕ ∀ z ∈ ℤ ≥ y norm ℎ ⁡ F ⁡ z - ℎ A < B