Theorem iscau

Description: Express the property " F is a Cauchy sequence of metric D ". Part of Definition 1.4-3 of Kreyszig p. 28. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Assertion	iscau	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(F\in \mathrm{Cau}\left(D\right)\leftrightarrow \left(F\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)\wedge \forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶F\left(k\right)\mathrm{ball}\left(D\right)x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		caufval	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \mathrm{Cau}\left(D\right)=\left\{f\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶f\left(k\right)\mathrm{ball}\left(D\right)x\right\}$$
2	1	eleq2d	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(F\in \mathrm{Cau}\left(D\right)\leftrightarrow F\in \left\{f\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶f\left(k\right)\mathrm{ball}\left(D\right)x\right\}\right)$$
3		reseq1	$$⊢f=F\to {f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}={F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}$$
4		eqidd	$$⊢f=F\to {\mathbb{Z}}_{\ge k}={\mathbb{Z}}_{\ge k}$$
5		fveq1	$$⊢f=F\to f\left(k\right)=F\left(k\right)$$
6	5	oveq1d	$$⊢f=F\to f\left(k\right)\mathrm{ball}\left(D\right)x=F\left(k\right)\mathrm{ball}\left(D\right)x$$
7	3 4 6	feq123d	$$⊢f=F\to \left(\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶f\left(k\right)\mathrm{ball}\left(D\right)x\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶F\left(k\right)\mathrm{ball}\left(D\right)x\right)$$
8	7	rexbidv	$$⊢f=F\to \left(\exists k\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶f\left(k\right)\mathrm{ball}\left(D\right)x\leftrightarrow \exists k\in \mathbb{Z}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶F\left(k\right)\mathrm{ball}\left(D\right)x\right)$$
9	8	ralbidv	$$⊢f=F\to \left(\forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶f\left(k\right)\mathrm{ball}\left(D\right)x\leftrightarrow \forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶F\left(k\right)\mathrm{ball}\left(D\right)x\right)$$
10	9	elrab	$$⊢F\in \left\{f\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)|\forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({f\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶f\left(k\right)\mathrm{ball}\left(D\right)x\right\}\leftrightarrow \left(F\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)\wedge \forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶F\left(k\right)\mathrm{ball}\left(D\right)x\right)$$
11	2 10	syl6bb	$$⊢D\in \mathrm{\infty Met}\left(X\right)\to \left(F\in \mathrm{Cau}\left(D\right)\leftrightarrow \left(F\in \left(X{\uparrow }_{𝑝𝑚}ℂ\right)\wedge \forall x\in {ℝ}^{+}\exists k\in \mathbb{Z}\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge k}}\right):{\mathbb{Z}}_{\ge k}⟶F\left(k\right)\mathrm{ball}\left(D\right)x\right)\right)$$