Theorem hlimveci

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

	Ref	Expression
Hypothesis	hlim.1	|- A e. _V
Assertion	hlimveci	|- ( F ~~>v A -> A e. ~H )

Proof

Step	Hyp	Ref	Expression
1		hlim.1	|- A e. _V
2	1	hlimi	|- ( F ~~>v A <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) )
3	2	simplbi	|- ( F ~~>v A -> ( F : NN --> ~H /\ A e. ~H ) )
4	3	simprd	|- ( F ~~>v A -> A e. ~H )