Metamath Proof Explorer

Theorem caucvgr

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) (Revised by Mario Carneiro, 8-May-2016)

Ref Expression
Hypotheses caucvgr.1 
|- ( ph -> A C_ RR )
caucvgr.2 
|- ( ph -> F : A --> CC )
caucvgr.3 
|- ( ph -> sup ( A , RR* , < ) = +oo )
caucvgr.4 
|- ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
Assertion caucvgr 
|- ( ph -> F e. dom ~~>r )

Proof

Step Hyp Ref Expression
1 caucvgr.1 
 |-  ( ph -> A C_ RR )
2 caucvgr.2 
 |-  ( ph -> F : A --> CC )
3 caucvgr.3 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
4 caucvgr.4 
 |-  ( ph -> A. x e. RR+ E. j e. A A. k e. A ( j <_ k -> ( abs ` ( ( F ` k ) - ( F ` j ) ) ) < x ) )
5 2 feqmptd 
 |-  ( ph -> F = ( n e. A |-> ( F ` n ) ) )
6 2 ffvelrnda 
 |-  ( ( ph /\ n e. A ) -> ( F ` n ) e. CC )
7 6 replimd 
 |-  ( ( ph /\ n e. A ) -> ( F ` n ) = ( ( Re ` ( F ` n ) ) + ( _i x. ( Im ` ( F ` n ) ) ) ) )
8 7 mpteq2dva 
 |-  ( ph -> ( n e. A |-> ( F ` n ) ) = ( n e. A |-> ( ( Re ` ( F ` n ) ) + ( _i x. ( Im ` ( F ` n ) ) ) ) ) )
9 5 8 eqtrd 
 |-  ( ph -> F = ( n e. A |-> ( ( Re ` ( F ` n ) ) + ( _i x. ( Im ` ( F ` n ) ) ) ) ) )
10 fvexd 
 |-  ( ( ph /\ n e. A ) -> ( Re ` ( F ` n ) ) e. _V )
11 ovexd 
 |-  ( ( ph /\ n e. A ) -> ( _i x. ( Im ` ( F ` n ) ) ) e. _V )
12 ref 
 |-  Re : CC --> RR
13 resub 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( Re ` ( ( F ` k ) - ( F ` j ) ) ) = ( ( Re ` ( F ` k ) ) - ( Re ` ( F ` j ) ) ) )
14 13 fveq2d 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( Re ` ( ( F ` k ) - ( F ` j ) ) ) ) = ( abs ` ( ( Re ` ( F ` k ) ) - ( Re ` ( F ` j ) ) ) ) )
15 subcl 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( ( F ` k ) - ( F ` j ) ) e. CC )
16 absrele 
 |-  ( ( ( F ` k ) - ( F ` j ) ) e. CC -> ( abs ` ( Re ` ( ( F ` k ) - ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
17 15 16 syl 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( Re ` ( ( F ` k ) - ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
18 14 17 eqbrtrrd 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( Re ` ( F ` k ) ) - ( Re ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
19 1 2 3 4 12 18 caucvgrlem2 
 |-  ( ph -> ( n e. A |-> ( Re ` ( F ` n ) ) ) ~~>r ( ~~>r ` ( Re o. F ) ) )
20 ax-icn 
 |-  _i e. CC
21 20 elexi 
 |-  _i e. _V
22 21 a1i 
 |-  ( ( ph /\ n e. A ) -> _i e. _V )
23 fvexd 
 |-  ( ( ph /\ n e. A ) -> ( Im ` ( F ` n ) ) e. _V )
24 rlimconst 
 |-  ( ( A C_ RR /\ _i e. CC ) -> ( n e. A |-> _i ) ~~>r _i )
25 1 20 24 sylancl 
 |-  ( ph -> ( n e. A |-> _i ) ~~>r _i )
26 imf 
 |-  Im : CC --> RR
27 imsub 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( Im ` ( ( F ` k ) - ( F ` j ) ) ) = ( ( Im ` ( F ` k ) ) - ( Im ` ( F ` j ) ) ) )
28 27 fveq2d 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( Im ` ( ( F ` k ) - ( F ` j ) ) ) ) = ( abs ` ( ( Im ` ( F ` k ) ) - ( Im ` ( F ` j ) ) ) ) )
29 absimle 
 |-  ( ( ( F ` k ) - ( F ` j ) ) e. CC -> ( abs ` ( Im ` ( ( F ` k ) - ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
30 15 29 syl 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( Im ` ( ( F ` k ) - ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
31 28 30 eqbrtrrd 
 |-  ( ( ( F ` k ) e. CC /\ ( F ` j ) e. CC ) -> ( abs ` ( ( Im ` ( F ` k ) ) - ( Im ` ( F ` j ) ) ) ) <_ ( abs ` ( ( F ` k ) - ( F ` j ) ) ) )
32 1 2 3 4 26 31 caucvgrlem2 
 |-  ( ph -> ( n e. A |-> ( Im ` ( F ` n ) ) ) ~~>r ( ~~>r ` ( Im o. F ) ) )
33 22 23 25 32 rlimmul 
 |-  ( ph -> ( n e. A |-> ( _i x. ( Im ` ( F ` n ) ) ) ) ~~>r ( _i x. ( ~~>r ` ( Im o. F ) ) ) )
34 10 11 19 33 rlimadd 
 |-  ( ph -> ( n e. A |-> ( ( Re ` ( F ` n ) ) + ( _i x. ( Im ` ( F ` n ) ) ) ) ) ~~>r ( ( ~~>r ` ( Re o. F ) ) + ( _i x. ( ~~>r ` ( Im o. F ) ) ) ) )
35 9 34 eqbrtrd 
 |-  ( ph -> F ~~>r ( ( ~~>r ` ( Re o. F ) ) + ( _i x. ( ~~>r ` ( Im o. F ) ) ) ) )
36 rlimrel 
 |-  Rel ~~>r
37 36 releldmi 
 |-  ( F ~~>r ( ( ~~>r ` ( Re o. F ) ) + ( _i x. ( ~~>r ` ( Im o. F ) ) ) ) -> F e. dom ~~>r )
38 35 37 syl 
 |-  ( ph -> F e. dom ~~>r )