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 φkABV
rlimabs.2 φkABC
Assertion rlimim φkABC

Proof

Step Hyp Ref Expression
1 rlimabs.1 φkABV
2 rlimabs.2 φkABC
3 1 2 rlimmptrcl φkAB
4 rlimcl kABCC
5 2 4 syl φC
6 imf :
7 ax-resscn
8 fss ::
9 6 7 8 mp2an :
10 9 a1i φ:
11 imcn2 Cx+y+zzC<yzC<x
12 5 11 sylan φx+y+zzC<yzC<x
13 3 5 2 10 12 rlimcn1b φkABC