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

Metamath Proof Explorer

Theorem hcaucvg

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

Ref Expression
Assertion hcaucvg 
|- ( ( F e. Cauchy /\ A e. RR+ ) -> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < A )

Proof

Step Hyp Ref Expression
1 hcau 
 |-  ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
2 1 simprbi 
 |-  ( F e. Cauchy -> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x )
3 breq2 
 |-  ( x = A -> ( ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x <-> ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < A ) )
4 3 rexralbidv 
 |-  ( x = A -> ( E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x <-> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < A ) )
5 4 rspccva 
 |-  ( ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x /\ A e. RR+ ) -> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < A )
6 2 5 sylan 
 |-  ( ( F e. Cauchy /\ A e. RR+ ) -> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < A )