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	$$⊢\left(F\in \mathrm{Cauchy}\wedge A\in {ℝ}^{+}\right)\to \exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<A$$

Proof

Step	Hyp	Ref	Expression
1		hcau	$$⊢F\in \mathrm{Cauchy}\leftrightarrow \left(F:\mathbb{N}⟶\mathscr{H}\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
2	1	simprbi	$$⊢F\in \mathrm{Cauchy}\to \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x$$
3		breq2	$$⊢x=A\to \left({norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\leftrightarrow {norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<A\right)$$
4	3	rexralbidv	$$⊢x=A\to \left(\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\leftrightarrow \exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<A\right)$$
5	4	rspccva	$$⊢\left(\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\wedge A\in {ℝ}^{+}\right)\to \exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<A$$
6	2 5	sylan	$$⊢\left(F\in \mathrm{Cauchy}\wedge A\in {ℝ}^{+}\right)\to \exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<A$$