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 FCauchyA+yzynormFy-Fz<A

Proof

Step Hyp Ref Expression
1 hcau FCauchyF:x+yzynormFy-Fz<x
2 1 simprbi FCauchyx+yzynormFy-Fz<x
3 breq2 x=AnormFy-Fz<xnormFy-Fz<A
4 3 rexralbidv x=AyzynormFy-Fz<xyzynormFy-Fz<A
5 4 rspccva x+yzynormFy-Fz<xA+yzynormFy-Fz<A
6 2 5 sylan FCauchyA+yzynormFy-Fz<A