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 | |
|
rlimabs.2 | |
||
Assertion | rlimim | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rlimabs.1 | |
|
2 | rlimabs.2 | |
|
3 | 1 2 | rlimmptrcl | |
4 | rlimcl | |
|
5 | 2 4 | syl | |
6 | imf | |
|
7 | ax-resscn | |
|
8 | fss | |
|
9 | 6 7 8 | mp2an | |
10 | 9 | a1i | |
11 | imcn2 | |
|
12 | 5 11 | sylan | |
13 | 3 5 2 10 12 | rlimcn1b | |