Metamath Proof Explorer

Theorem caucvg

Description: A Cauchy sequence of complex numbers converges to a complex number. Theorem 12-5.3 of Gleason p. 180 (sufficiency part). (Contributed by NM, 20-Dec-2006) (Proof shortened by Mario Carneiro, 15-Feb-2014) (Revised by Mario Carneiro, 8-May-2016)

Ref Expression
Hypotheses caucvg.1 
|- Z = ( ZZ>= ` M )
caucvg.2 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
caucvg.3 
|- ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
caucvg.4 
|- ( ph -> F e. V )
Assertion caucvg 
|- ( ph -> F e. dom ~~> )

Proof

Step Hyp Ref Expression
1 caucvg.1 
 |-  Z = ( ZZ>= ` M )
2 caucvg.2 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
3 caucvg.3 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
4 caucvg.4 
 |-  ( ph -> F e. V )
5 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
6 5 cbvmptv 
 |-  ( k e. Z |-> ( F ` k ) ) = ( n e. Z |-> ( F ` n ) )
7 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
8 1 7 eqsstri 
 |-  Z C_ ZZ
9 zssre 
 |-  ZZ C_ RR
10 8 9 sstri 
 |-  Z C_ RR
11 10 a1i 
 |-  ( ph -> Z C_ RR )
12 6 eqcomi 
 |-  ( n e. Z |-> ( F ` n ) ) = ( k e. Z |-> ( F ` k ) )
13 2 12 fmptd 
 |-  ( ph -> ( n e. Z |-> ( F ` n ) ) : Z --> CC )
14 1rp 
 |-  1 e. RR+
15 14 ne0ii 
 |-  RR+ =/= (/)
16 r19.2z 
 |-  ( ( RR+ =/= (/) /\ A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> E. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
17 15 3 16 sylancr 
 |-  ( ph -> E. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x )
18 eluzel2 
 |-  ( j e. ( ZZ>= ` M ) -> M e. ZZ )
19 18 1 eleq2s 
 |-  ( j e. Z -> M e. ZZ )
20 19 a1d 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> M e. ZZ ) )
21 20 rexlimiv 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> M e. ZZ )
22 21 rexlimivw 
 |-  ( E. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> M e. ZZ )
23 17 22 syl 
 |-  ( ph -> M e. ZZ )
24 1 uzsup 
 |-  ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
25 23 24 syl 
 |-  ( ph -> sup ( Z , RR* , < ) = +oo )
26 8 sseli 
 |-  ( j e. Z -> j e. ZZ )
27 8 sseli 
 |-  ( k e. Z -> k e. ZZ )
28 eluz 
 |-  ( ( j e. ZZ /\ k e. ZZ ) -> ( k e. ( ZZ>= ` j ) <-> j <_ k ) )
29 26 27 28 syl2an 
 |-  ( ( j e. Z /\ k e. Z ) -> ( k e. ( ZZ>= ` j ) <-> j <_ k ) )
30 29 biimprd 
 |-  ( ( j e. Z /\ k e. Z ) -> ( j <_ k -> k e. ( ZZ>= ` j ) ) )
31 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
32 eqid 
 |-  ( n e. Z |-> ( F ` n ) ) = ( n e. Z |-> ( F ` n ) )
33 fvex 
 |-  ( F ` n ) e. _V
34 31 32 33 fvmpt3i 
 |-  ( k e. Z -> ( ( n e. Z |-> ( F ` n ) ) ` k ) = ( F ` k ) )
35 fveq2 
 |-  ( n = j -> ( F ` n ) = ( F ` j ) )
36 35 32 33 fvmpt3i 
 |-  ( j e. Z -> ( ( n e. Z |-> ( F ` n ) ) ` j ) = ( F ` j ) )
37 34 36 oveqan12rd 
 |-  ( ( j e. Z /\ k e. Z ) -> ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) = ( ( F ` k ) - ( F ` j ) ) )
38 37 fveq2d 
 |-  ( ( j e. Z /\ k e. Z ) -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) = ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
39 38 breq1d 
 |-  ( ( j e. Z /\ k e. Z ) -> ( ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x <-> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
40 39 biimprd 
 |-  ( ( j e. Z /\ k e. Z ) -> ( ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) )
41 30 40 imim12d 
 |-  ( ( j e. Z /\ k e. Z ) -> ( ( k e. ( ZZ>= ` j ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) ) )
42 41 ex 
 |-  ( j e. Z -> ( k e. Z -> ( ( k e. ( ZZ>= ` j ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) ) ) )
43 42 com23 
 |-  ( j e. Z -> ( ( k e. ( ZZ>= ` j ) -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) -> ( k e. Z -> ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) ) ) )
44 43 ralimdv2 
 |-  ( j e. Z -> ( A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> A. k e. Z ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) ) )
45 44 reximia 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> E. j e. Z A. k e. Z ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) )
46 45 ralimi 
 |-  ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x -> A. x e. RR+ E. j e. Z A. k e. Z ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) )
47 3 46 syl 
 |-  ( ph -> A. x e. RR+ E. j e. Z A. k e. Z ( j <_ k -> ( abs ` ( ( ( n e. Z |-> ( F ` n ) ) ` k ) - ( ( n e. Z |-> ( F ` n ) ) ` j ) ) ) < x ) )
48 11 13 25 47 caucvgr 
 |-  ( ph -> ( n e. Z |-> ( F ` n ) ) e. dom ~~>r )
49 13 25 rlimdm 
 |-  ( ph -> ( ( n e. Z |-> ( F ` n ) ) e. dom ~~>r <-> ( n e. Z |-> ( F ` n ) ) ~~>r ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) ) )
50 48 49 mpbid 
 |-  ( ph -> ( n e. Z |-> ( F ` n ) ) ~~>r ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) )
51 6 50 eqbrtrid 
 |-  ( ph -> ( k e. Z |-> ( F ` k ) ) ~~>r ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) )
52 eqid 
 |-  ( k e. Z |-> ( F ` k ) ) = ( k e. Z |-> ( F ` k ) )
53 2 52 fmptd 
 |-  ( ph -> ( k e. Z |-> ( F ` k ) ) : Z --> CC )
54 1 23 53 rlimclim 
 |-  ( ph -> ( ( k e. Z |-> ( F ` k ) ) ~~>r ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) <-> ( k e. Z |-> ( F ` k ) ) ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) ) )
55 51 54 mpbid 
 |-  ( ph -> ( k e. Z |-> ( F ` k ) ) ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) )
56 1 52 climmpt 
 |-  ( ( M e. ZZ /\ F e. V ) -> ( F ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) <-> ( k e. Z |-> ( F ` k ) ) ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) ) )
57 23 4 56 syl2anc 
 |-  ( ph -> ( F ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) <-> ( k e. Z |-> ( F ` k ) ) ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) ) )
58 55 57 mpbird 
 |-  ( ph -> F ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) )
59 climrel 
 |-  Rel ~~>
60 59 releldmi 
 |-  ( F ~~> ( ~~>r ` ( n e. Z |-> ( F ` n ) ) ) -> F e. dom ~~> )
61 58 60 syl 
 |-  ( ph -> F e. dom ~~> )