Metamath Proof Explorer


Theorem seq1hcau

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

Ref Expression
Assertion seq1hcau
|- ( F : NN --> ~H -> ( F e. Cauchy <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )

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 baib
 |-  ( F : NN --> ~H -> ( F e. Cauchy <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )