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 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 )