Theorem cau4

Description: Change the base of a Cauchy criterion. (Contributed by Mario Carneiro, 18-Mar-2014)

	Ref	Expression
Hypotheses	cau3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	cau4.2	$$⊢W={\mathbb{Z}}_{\ge N}$$
Assertion	cau4	$$⊢N\in Z\to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cau3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		cau4.2	$$⊢W={\mathbb{Z}}_{\ge N}$$
3		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
4	1	rexuz3	$$⊢M\in \mathbb{Z}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
5	3 4	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
6		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
7	2	rexuz3	$$⊢N\in \mathbb{Z}\to \left(\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
8	6 7	syl	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \exists j\in \mathbb{Z}\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
9	5 8	bitr4d	$$⊢N\in {\mathbb{Z}}_{\ge M}\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
10	9 1	eleq2s	$$⊢N\in Z\to \left(\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
11	10	ralbidv	$$⊢N\in Z\to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)\right)$$
12	1	cau3	$$⊢\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)$$
13	2	cau3	$$⊢\forall x\in {ℝ}^{+}\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall y\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(y\right)\right|<x\right)$$
14	11 12 13	3bitr4g	$$⊢N\in Z\to \left(\forall x\in {ℝ}^{+}\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\leftrightarrow \forall x\in {ℝ}^{+}\exists j\in W\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\right)$$