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

Metamath Proof Explorer

Theorem hlimseqi

Description: A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

Ref Expression
Hypothesis hlim.1 ⊢ 𝐴 ∈ V
Assertion hlimseqi ( 𝐹 ⇝𝑣 𝐴 → 𝐹 : ℕ ⟶ ℋ )

Proof

Step Hyp Ref Expression
1 hlim.1 ⊢ 𝐴 ∈ V
2 1 hlimi ⊢ ( 𝐹 ⇝𝑣 𝐴 ↔ ( ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝐹 ‘ 𝑧 ) −ℎ 𝐴 ) ) < 𝑥 ) )
3 2 simplbi ⊢ ( 𝐹 ⇝𝑣 𝐴 → ( 𝐹 : ℕ ⟶ ℋ ∧ 𝐴 ∈ ℋ ) )
4 3 simpld ⊢ ( 𝐹 ⇝𝑣 𝐴 → 𝐹 : ℕ ⟶ ℋ )