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 
|- F/_ j F
caucvgbf.2 
|- F/_ k F
caucvgbf.3 
|- Z = ( ZZ>= ` M )
Assertion caucvgbf 
|- ( ( M e. ZZ /\ F e. V ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )

Proof

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