Metamath Proof Explorer


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 _ j F
caucvgbf.2 _ k F
caucvgbf.3 Z = M
Assertion caucvgbf M F V F dom x + j Z k j F k F k F j < x

Proof

Step Hyp Ref Expression
1 caucvgbf.1 _ j F
2 caucvgbf.2 _ k F
3 caucvgbf.3 Z = M
4 3 caucvgb M F V F dom x + i Z l i F l F l F i < x
5 nfcv _ j i
6 nfcv _ j l
7 1 6 nffv _ j F l
8 7 nfel1 j F l
9 nfcv _ j abs
10 nfcv _ j
11 nfcv _ j i
12 1 11 nffv _ j F i
13 7 10 12 nfov _ j F l F i
14 9 13 nffv _ j F l F i
15 nfcv _ j <
16 nfcv _ j x
17 14 15 16 nfbr j F l F i < x
18 8 17 nfan j F l F l F i < x
19 5 18 nfralw j l i F l F l F i < x
20 nfv i k j F k F k F j < x
21 nfcv _ k l
22 2 21 nffv _ k F l
23 22 nfel1 k F l
24 nfcv _ k abs
25 nfcv _ k
26 nfcv _ k i
27 2 26 nffv _ k F i
28 22 25 27 nfov _ k F l F i
29 24 28 nffv _ k F l F i
30 nfcv _ k <
31 nfcv _ k x
32 29 30 31 nfbr k F l F i < x
33 23 32 nfan k F l F l F i < x
34 nfv l F k F k F i < x
35 fveq2 l = k F l = F k
36 35 eleq1d l = k F l F k
37 35 fvoveq1d l = k F l F i = F k F i
38 37 breq1d l = k F l F i < x F k F i < x
39 36 38 anbi12d l = k F l F l F i < x F k F k F i < x
40 33 34 39 cbvralw l i F l F l F i < x k i F k F k F i < x
41 fveq2 i = j i = j
42 fveq2 i = j F i = F j
43 42 oveq2d i = j F k F i = F k F j
44 43 fveq2d i = j F k F i = F k F j
45 44 breq1d i = j F k F i < x F k F j < x
46 45 anbi2d i = j F k F k F i < x F k F k F j < x
47 41 46 raleqbidv i = j k i F k F k F i < x k j F k F k F j < x
48 40 47 bitrid i = j l i F l F l F i < x k j F k F k F j < x
49 19 20 48 cbvrexw i Z l i F l F l F i < x j Z k j F k F k F j < x
50 49 ralbii x + i Z l i F l F l F i < x x + j Z k j F k F k F j < x
51 4 50 bitrdi M F V F dom x + j Z k j F k F k F j < x