Theorem caucvgbf

Description: A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of Gleason p. 180. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	caucvgbf.1	$$⊢\underset{\_}{Ⅎ}jF$$
	caucvgbf.2	$$⊢\underset{\_}{Ⅎ}kF$$
	caucvgbf.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	caucvgbf	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(F\in \mathrm{dom}⇝\leftrightarrow \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)\right)$$

Proof

Step	Hyp	Ref	Expression
1		caucvgbf.1	$$⊢\underset{\_}{Ⅎ}jF$$
2		caucvgbf.2	$$⊢\underset{\_}{Ⅎ}kF$$
3		caucvgbf.3	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4	3	caucvgb	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(F\in \mathrm{dom}⇝\leftrightarrow \forall x\in {ℝ}^{+}\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)\right)$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}j{\mathbb{Z}}_{\ge i}$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}jl$$
7	1 6	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(l\right)$$
8	7	nfel1	$$⊢ℲjF\left(l\right)\in ℂ$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}j\mathrm{abs}$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}j-$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}ji$$
12	1 11	nffv	$$⊢\underset{\_}{Ⅎ}jF\left(i\right)$$
13	7 10 12	nfov	$$⊢\underset{\_}{Ⅎ}j\left(F\left(l\right)-F\left(i\right)\right)$$
14	9 13	nffv	$$⊢\underset{\_}{Ⅎ}j\left|F\left(l\right)-F\left(i\right)\right|$$
15		nfcv	$$⊢\underset{\_}{Ⅎ}j<$$
16		nfcv	$$⊢\underset{\_}{Ⅎ}jx$$
17	14 15 16	nfbr	$$⊢Ⅎj\left|F\left(l\right)-F\left(i\right)\right|<x$$
18	8 17	nfan	$$⊢Ⅎj\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)$$
19	5 18	nfralw	$$⊢Ⅎj\forall l\in {\mathbb{Z}}_{\ge i}\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)$$
20		nfv	$$⊢Ⅎi\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)$$
21		nfcv	$$⊢\underset{\_}{Ⅎ}kl$$
22	2 21	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(l\right)$$
23	22	nfel1	$$⊢ℲkF\left(l\right)\in ℂ$$
24		nfcv	$$⊢\underset{\_}{Ⅎ}k\mathrm{abs}$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}k-$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}ki$$
27	2 26	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(i\right)$$
28	22 25 27	nfov	$$⊢\underset{\_}{Ⅎ}k\left(F\left(l\right)-F\left(i\right)\right)$$
29	24 28	nffv	$$⊢\underset{\_}{Ⅎ}k\left|F\left(l\right)-F\left(i\right)\right|$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}k<$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
32	29 30 31	nfbr	$$⊢Ⅎk\left|F\left(l\right)-F\left(i\right)\right|<x$$
33	23 32	nfan	$$⊢Ⅎk\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)$$
34		nfv	$$⊢Ⅎl\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(i\right)\right|<x\right)$$
35		fveq2	$$⊢l=k\to F\left(l\right)=F\left(k\right)$$
36	35	eleq1d	$$⊢l=k\to \left(F\left(l\right)\in ℂ\leftrightarrow F\left(k\right)\in ℂ\right)$$
37	35	fvoveq1d	$$⊢l=k\to \left|F\left(l\right)-F\left(i\right)\right|=\left|F\left(k\right)-F\left(i\right)\right|$$
38	37	breq1d	$$⊢l=k\to \left(\left|F\left(l\right)-F\left(i\right)\right|<x\leftrightarrow \left|F\left(k\right)-F\left(i\right)\right|<x\right)$$
39	36 38	anbi12d	$$⊢l=k\to \left(\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)\leftrightarrow \left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(i\right)\right|<x\right)\right)$$
40	33 34 39	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge i}\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge i}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(i\right)\right|<x\right)$$
41		fveq2	$$⊢i=j\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge j}$$
42		fveq2	$$⊢i=j\to F\left(i\right)=F\left(j\right)$$
43	42	oveq2d	$$⊢i=j\to F\left(k\right)-F\left(i\right)=F\left(k\right)-F\left(j\right)$$
44	43	fveq2d	$$⊢i=j\to \left|F\left(k\right)-F\left(i\right)\right|=\left|F\left(k\right)-F\left(j\right)\right|$$
45	44	breq1d	$$⊢i=j\to \left(\left|F\left(k\right)-F\left(i\right)\right|<x\leftrightarrow \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
46	45	anbi2d	$$⊢i=j\to \left(\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(i\right)\right|<x\right)\leftrightarrow \left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(j\right)\right|<x\right)\right)$$
47	41 46	raleqbidv	$$⊢i=j\to \left(\forall k\in {\mathbb{Z}}_{\ge i}\left(F\left(k\right)\in ℂ\wedge \left|F\left(k\right)-F\left(i\right)\right|<x\right)\leftrightarrow \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)$$
48	40 47	bitrid	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)\leftrightarrow \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)$$
49	19 20 48	cbvrexw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\right)\right|<x\right)\leftrightarrow \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)$$
50	49	ralbii	$$⊢\forall x\in {ℝ}^{+}\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}\left(F\left(l\right)\in ℂ\wedge \left|F\left(l\right)-F\left(i\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 \left|F\left(k\right)-F\left(j\right)\right|<x\right)$$
51	4 50	bitrdi	$$⊢\left(M\in \mathbb{Z}\wedge F\in V\right)\to \left(F\in \mathrm{dom}⇝\leftrightarrow \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)\right)$$