Theorem cau3

Description: Convert between three-quantifier and four-quantifier versions of the Cauchy criterion. (In particular, the four-quantifier version has no occurrence of j in the assertion, so it can be used with rexanuz and friends.) (Contributed by Mario Carneiro, 15-Feb-2014)

	Ref	Expression
Hypothesis	cau3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	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 m\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(m\right)\right|<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		cau3.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
3	1 2	eqsstri	$$⊢Z\subseteq \mathbb{Z}$$
4		id	$$⊢F\left(k\right)\in ℂ\to F\left(k\right)\in ℂ$$
5		eleq1	$$⊢F\left(k\right)=F\left(j\right)\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(j\right)\in ℂ\right)$$
6		eleq1	$$⊢F\left(k\right)=F\left(m\right)\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(m\right)\in ℂ\right)$$
7		abssub	$$⊢\left(F\left(j\right)\in ℂ\wedge F\left(k\right)\in ℂ\right)\to \left|F\left(j\right)-F\left(k\right)\right|=\left|F\left(k\right)-F\left(j\right)\right|$$
8	7	3adant1	$$⊢\left(\top \wedge F\left(j\right)\in ℂ\wedge F\left(k\right)\in ℂ\right)\to \left|F\left(j\right)-F\left(k\right)\right|=\left|F\left(k\right)-F\left(j\right)\right|$$
9		abssub	$$⊢\left(F\left(m\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|F\left(m\right)-F\left(j\right)\right|=\left|F\left(j\right)-F\left(m\right)\right|$$
10	9	3adant1	$$⊢\left(\top \wedge F\left(m\right)\in ℂ\wedge F\left(j\right)\in ℂ\right)\to \left|F\left(m\right)-F\left(j\right)\right|=\left|F\left(j\right)-F\left(m\right)\right|$$
11		abs3lem	$$⊢\left(\left(F\left(k\right)\in ℂ\wedge F\left(m\right)\in ℂ\right)\wedge \left(F\left(j\right)\in ℂ\wedge x\in ℝ\right)\right)\to \left(\left(\left|F\left(k\right)-F\left(j\right)\right|<\frac{x}{2}\wedge \left|F\left(j\right)-F\left(m\right)\right|<\frac{x}{2}\right)\to \left|F\left(k\right)-F\left(m\right)\right|<x\right)$$
12	11	3adant1	$$⊢\left(\top \wedge \left(F\left(k\right)\in ℂ\wedge F\left(m\right)\in ℂ\right)\wedge \left(F\left(j\right)\in ℂ\wedge x\in ℝ\right)\right)\to \left(\left(\left|F\left(k\right)-F\left(j\right)\right|<\frac{x}{2}\wedge \left|F\left(j\right)-F\left(m\right)\right|<\frac{x}{2}\right)\to \left|F\left(k\right)-F\left(m\right)\right|<x\right)$$
13	3 4 5 6 8 10 12	cau3lem	$$⊢\top \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 Z\forall k\in {\mathbb{Z}}_{\ge j}\left(F\left(k\right)\in ℂ\wedge \forall m\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(m\right)\right|<x\right)\right)$$
14	13	mptru	$$⊢\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 m\in {\mathbb{Z}}_{\ge k}\left|F\left(k\right)-F\left(m\right)\right|<x\right)$$