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 e. _V
Assertion	hlimconvi	|- ( ( F ~~>v A /\ B e. RR+ ) -> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < B )

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	simprbi	|- ( F ~~>v A -> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x )
4		breq2	|- ( x = B -> ( ( normh ` ( ( F ` z ) -h A ) ) < x <-> ( normh ` ( ( F ` z ) -h A ) ) < B ) )
5	4	rexralbidv	|- ( x = B -> ( E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x <-> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < B ) )
6	5	rspccva	|- ( ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x /\ B e. RR+ ) -> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < B )
7	3 6	sylan	|- ( ( F ~~>v A /\ B e. RR+ ) -> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < B )