Metamath Proof Explorer

Theorem rlimim

Description: Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimabs.1 
|- ( ( ph /\ k e. A ) -> B e. V )
rlimabs.2 
|- ( ph -> ( k e. A |-> B ) ~~>r C )
Assertion rlimim 
|- ( ph -> ( k e. A |-> ( Im ` B ) ) ~~>r ( Im ` C ) )

Proof

Step Hyp Ref Expression
1 rlimabs.1 
 |-  ( ( ph /\ k e. A ) -> B e. V )
2 rlimabs.2 
 |-  ( ph -> ( k e. A |-> B ) ~~>r C )
3 1 2 rlimmptrcl 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 rlimcl 
 |-  ( ( k e. A |-> B ) ~~>r C -> C e. CC )
5 2 4 syl 
 |-  ( ph -> C e. CC )
6 imf 
 |-  Im : CC --> RR
7 ax-resscn 
 |-  RR C_ CC
8 fss 
 |-  ( ( Im : CC --> RR /\ RR C_ CC ) -> Im : CC --> CC )
9 6 7 8 mp2an 
 |-  Im : CC --> CC
10 9 a1i 
 |-  ( ph -> Im : CC --> CC )
11 imcn2 
 |-  ( ( C e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( Im ` z ) - ( Im ` C ) ) ) < x ) )
12 5 11 sylan 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( Im ` z ) - ( Im ` C ) ) ) < x ) )
13 3 5 2 10 12 rlimcn1b 
 |-  ( ph -> ( k e. A |-> ( Im ` B ) ) ~~>r ( Im ` C ) )