Metamath Proof Explorer

Theorem caucvgb

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

Ref Expression
Hypothesis caucvgb.1 
|- Z = ( ZZ>= ` M )
Assertion caucvgb 
|- ( ( 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 caucvgb.1 
 |-  Z = ( ZZ>= ` M )
2 eldm2g 
 |-  ( F e. dom ~~> -> ( F e. dom ~~> <-> E. m <. F , m >. e. ~~> ) )
3 2 ibi 
 |-  ( F e. dom ~~> -> E. m <. F , m >. e. ~~> )
4 df-br 
 |-  ( F ~~> m <-> <. F , m >. e. ~~> )
5 simpll 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> M e. ZZ )
6 1rp 
 |-  1 e. RR+
7 6 a1i 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> 1 e. RR+ )
8 eqidd 
 |-  ( ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) /\ k e. Z ) -> ( F ` k ) = ( F ` k ) )
9 simpr 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> F ~~> m )
10 1 5 7 8 9 climi 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) )
11 simpl 
 |-  ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) -> ( F ` k ) e. CC )
12 11 ralimi 
 |-  ( A. k e. ( ZZ>= ` n ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) -> A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC )
13 12 reximi 
 |-  ( E. n e. Z A. k e. ( ZZ>= ` n ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - m ) ) < 1 ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC )
14 10 13 syl 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ F ~~> m ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC )
15 14 ex 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F ~~> m -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
16 4 15 biimtrrid 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( <. F , m >. e. ~~> -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
17 16 exlimdv 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( E. m <. F , m >. e. ~~> -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
18 3 17 syl5 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F e. dom ~~> -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
19 fveq2 
 |-  ( j = n -> ( ZZ>= ` j ) = ( ZZ>= ` n ) )
20 19 raleqdv 
 |-  ( j = n -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
21 20 cbvrexvw 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC )
22 21 a1i 
 |-  ( x = 1 -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC <-> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
23 simpl 
 |-  ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( F ` k ) e. CC )
24 23 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
25 24 reximi 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
26 25 ralimi 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) e. CC )
27 6 a1i 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> 1 e. RR+ )
28 22 26 27 rspcdva 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC )
29 28 a1i 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) )
30 eluzelz 
 |-  ( n e. ( ZZ>= ` M ) -> n e. ZZ )
31 30 1 eleq2s 
 |-  ( n e. Z -> n e. ZZ )
32 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
33 32 climcau 
 |-  ( ( n e. ZZ /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
34 31 33 sylan 
 |-  ( ( n e. Z /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
35 32 r19.29uz 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC /\ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
36 35 ex 
 |-  ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC -> ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
37 36 ralimdv 
 |-  ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC -> ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
38 34 37 mpan9 
 |-  ( ( ( n e. Z /\ F e. dom ~~> ) /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
39 38 an32s 
 |-  ( ( ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
40 39 adantll 
 |-  ( ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ F e. dom ~~> ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
41 simplrr 
 |-  ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC )
42 fveq2 
 |-  ( k = m -> ( F ` k ) = ( F ` m ) )
43 42 eleq1d 
 |-  ( k = m -> ( ( F ` k ) e. CC <-> ( F ` m ) e. CC ) )
44 43 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. CC )
45 41 44 sylan 
 |-  ( ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) /\ m e. ( ZZ>= ` n ) ) -> ( F ` m ) e. CC )
46 simpr 
 |-  ( ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
47 46 ralimi 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
48 42 fvoveq1d 
 |-  ( k = m -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) = ( abs ` ( ( F ` m ) - ( F ` j ) ) ) )
49 48 breq1d 
 |-  ( k = m -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x ) )
50 49 cbvralvw 
 |-  ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x <-> A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x )
51 47 50 sylib 
 |-  ( A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x )
52 51 reximi 
 |-  ( E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x )
53 52 ralimi 
 |-  ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x )
54 53 adantl 
 |-  ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x )
55 fveq2 
 |-  ( j = i -> ( ZZ>= ` j ) = ( ZZ>= ` i ) )
56 fveq2 
 |-  ( j = i -> ( F ` j ) = ( F ` i ) )
57 56 oveq2d 
 |-  ( j = i -> ( ( F ` m ) - ( F ` j ) ) = ( ( F ` m ) - ( F ` i ) ) )
58 57 fveq2d 
 |-  ( j = i -> ( abs ` ( ( F ` m ) - ( F ` j ) ) ) = ( abs ` ( ( F ` m ) - ( F ` i ) ) ) )
59 58 breq1d 
 |-  ( j = i -> ( ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x ) )
60 55 59 raleqbidv 
 |-  ( j = i -> ( A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x ) )
61 60 cbvrexvw 
 |-  ( E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x )
62 breq2 
 |-  ( x = y -> ( ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x <-> ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) )
63 62 rexralbidv 
 |-  ( x = y -> ( E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < x <-> E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) )
64 61 63 bitrid 
 |-  ( x = y -> ( E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y ) )
65 64 cbvralvw 
 |-  ( A. x e. RR+ E. j e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` j ) ( abs ` ( ( F ` m ) - ( F ` j ) ) ) < x <-> A. y e. RR+ E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y )
66 54 65 sylib 
 |-  ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> A. y e. RR+ E. i e. ( ZZ>= ` n ) A. m e. ( ZZ>= ` i ) ( abs ` ( ( F ` m ) - ( F ` i ) ) ) < y )
67 simpll 
 |-  ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> F e. V )
68 32 45 66 67 caucvg 
 |-  ( ( ( F e. V /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> F e. dom ~~> )
69 68 adantlll 
 |-  ( ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) /\ A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) -> F e. dom ~~> )
70 40 69 impbida 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) -> ( F e. dom ~~> <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
71 1 32 cau4 
 |-  ( n e. Z -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
72 71 ad2antrl 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) <-> A. x e. RR+ E. j e. ( ZZ>= ` n ) A. k e. ( ZZ>= ` j ) ( ( F ` k ) e. CC /\ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) ) )
73 70 72 bitr4d 
 |-  ( ( ( M e. ZZ /\ F e. V ) /\ ( n e. Z /\ A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC ) ) -> ( 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 ) ) )
74 73 rexlimdvaa 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( E. n e. Z A. k e. ( ZZ>= ` n ) ( F ` k ) e. CC -> ( 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 ) ) ) )
75 18 29 74 pm5.21ndd 
 |-  ( ( 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 ) ) )