Metamath Proof Explorer


Theorem climim

Description: Limit of the imaginary part of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by NM, 7-Jun-2006) (Revised by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses climcn1lem.1 Z = M
climcn1lem.2 φ F A
climcn1lem.4 φ G W
climcn1lem.5 φ M
climcn1lem.6 φ k Z F k
climim.7 φ k Z G k = F k
Assertion climim φ G A

Proof

Step Hyp Ref Expression
1 climcn1lem.1 Z = M
2 climcn1lem.2 φ F A
3 climcn1lem.4 φ G W
4 climcn1lem.5 φ M
5 climcn1lem.6 φ k Z F k
6 climim.7 φ k Z G k = F k
7 imf :
8 ax-resscn
9 fss : :
10 7 8 9 mp2an :
11 imcn2 A x + y + z z A < y z A < x
12 1 2 3 4 5 10 11 6 climcn1lem φ G A