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 Cauchy A + y z y norm F y - F z < A

Proof

Step Hyp Ref Expression
1 hcau F Cauchy F : x + y z y norm F y - F z < x
2 1 simprbi F Cauchy x + y z y norm F y - F z < x
3 breq2 x = A norm F y - F z < x norm F y - F z < A
4 3 rexralbidv x = A y z y norm F y - F z < x y z y norm F y - F z < A
5 4 rspccva x + y z y norm F y - F z < x A + y z y norm F y - F z < A
6 2 5 sylan F Cauchy A + y z y norm F y - F z < A