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	⊢ Ⅎ 𝑗 𝐹
	caucvgbf.2	⊢ Ⅎ 𝑘 𝐹
	caucvgbf.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	caucvgbf	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		caucvgbf.1	⊢ Ⅎ 𝑗 𝐹
2		caucvgbf.2	⊢ Ⅎ 𝑘 𝐹
3		caucvgbf.3	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4	3	caucvgb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ) )
5		nfcv	⊢ Ⅎ 𝑗 ( ℤ≥ ‘ 𝑖 )
6		nfcv	⊢ Ⅎ 𝑗 𝑙
7	1 6	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
8	7	nfel1	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 ) ∈ ℂ
9		nfcv	⊢ Ⅎ 𝑗 abs
10		nfcv	⊢ Ⅎ 𝑗 −
11		nfcv	⊢ Ⅎ 𝑗 𝑖
12	1 11	nffv	⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑖 )
13	7 10 12	nfov	⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) )
14	9 13	nffv	⊢ Ⅎ 𝑗 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) )
15		nfcv	⊢ Ⅎ 𝑗 <
16		nfcv	⊢ Ⅎ 𝑗 𝑥
17	14 15 16	nfbr	⊢ Ⅎ 𝑗 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥
18	8 17	nfan	⊢ Ⅎ 𝑗 ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
19	5 18	nfralw	⊢ Ⅎ 𝑗 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
20		nfv	⊢ Ⅎ 𝑖 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 )
21		nfcv	⊢ Ⅎ 𝑘 𝑙
22	2 21	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
23	22	nfel1	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 ) ∈ ℂ
24		nfcv	⊢ Ⅎ 𝑘 abs
25		nfcv	⊢ Ⅎ 𝑘 −
26		nfcv	⊢ Ⅎ 𝑘 𝑖
27	2 26	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑖 )
28	22 25 27	nfov	⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) )
29	24 28	nffv	⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) )
30		nfcv	⊢ Ⅎ 𝑘 <
31		nfcv	⊢ Ⅎ 𝑘 𝑥
32	29 30 31	nfbr	⊢ Ⅎ 𝑘 ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥
33	23 32	nfan	⊢ Ⅎ 𝑘 ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
34		nfv	⊢ Ⅎ 𝑙 ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 )
35		fveq2	⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
36	35	eleq1d	⊢ ( 𝑙 = 𝑘 → ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑘 ) ∈ ℂ ) )
37	35	fvoveq1d	⊢ ( 𝑙 = 𝑘 → ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) )
38	37	breq1d	⊢ ( 𝑙 = 𝑘 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) )
39	36 38	anbi12d	⊢ ( 𝑙 = 𝑘 → ( ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ) )
40	33 34 39	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) )
41		fveq2	⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
42		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑗 ) )
43	42	oveq2d	⊢ ( 𝑖 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) = ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) )
44	43	fveq2d	⊢ ( 𝑖 = 𝑗 → ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) )
45	44	breq1d	⊢ ( 𝑖 = 𝑗 → ( ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
46	45	anbi2d	⊢ ( 𝑖 = 𝑗 → ( ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
47	41 46	raleqbidv	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
48	40 47	bitrid	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )
49	19 20 48	cbvrexw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
50	49	ralbii	⊢ ( ∀ 𝑥 ∈ ℝ+ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( ( 𝐹 ‘ 𝑙 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑙 ) − ( 𝐹 ‘ 𝑖 ) ) ) < 𝑥 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) )
51	4 50	bitrdi	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ∈ dom ⇝ ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ∧ ( abs ‘ ( ( 𝐹 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑗 ) ) ) < 𝑥 ) ) )