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 ) )