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 = ( ZZ>= ` M )
	climcn1lem.2	|- ( ph -> F ~~> A )
	climcn1lem.4	|- ( ph -> G e. W )
	climcn1lem.5	|- ( ph -> M e. ZZ )
	climcn1lem.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
	climim.7	|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Im ` ( F ` k ) ) )
Assertion	climim	|- ( ph -> G ~~> ( Im ` A ) )

Proof

Step	Hyp	Ref	Expression
1		climcn1lem.1	|- Z = ( ZZ>= ` M )
2		climcn1lem.2	|- ( ph -> F ~~> A )
3		climcn1lem.4	|- ( ph -> G e. W )
4		climcn1lem.5	|- ( ph -> M e. ZZ )
5		climcn1lem.6	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6		climim.7	|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Im ` ( F ` k ) ) )
7		imf	|- Im : CC --> RR
8		ax-resscn	|- RR C_ CC
9		fss	|- ( ( Im : CC --> RR /\ RR C_ CC ) -> Im : CC --> CC )
10	7 8 9	mp2an	|- Im : CC --> CC
11		imcn2	|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Im ` z ) - ( Im ` A ) ) ) < x ) )
12	1 2 3 4 5 10 11 6	climcn1lem	|- ( ph -> G ~~> ( Im ` A ) )