Theorem hlimconvi

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

	Ref	Expression
Hypothesis	hlim.1	$$⊢A\in \mathrm{V}$$
Assertion	hlimconvi	$$⊢\left(F\underset{v}{⇝}A\wedge B\in {ℝ}^{+}\right)\to \exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(z\right){-}_{ℎ}A\right)<B$$

Proof

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