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 syl5bir
 |-  ( ( 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 syl5bb
 |-  ( 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 ) ) )