Theorem imcncf

Description: Imaginary part is continuous. (Contributed by Paul Chapman, 21-Oct-2007) (Revised by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Assertion	imcncf	|- Im e. ( CC -cn-> RR )

Proof

Step	Hyp	Ref	Expression
1		imf	|- Im : CC --> RR
2		imcn2	|- ( ( x e. CC /\ y e. RR+ ) -> E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Im ` w ) - ( Im ` x ) ) ) < y ) )
3	2	rgen2	|- A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Im ` w ) - ( Im ` x ) ) ) < y )
4		ssid	|- CC C_ CC
5		ax-resscn	|- RR C_ CC
6		elcncf2	|- ( ( CC C_ CC /\ RR C_ CC ) -> ( Im e. ( CC -cn-> RR ) <-> ( Im : CC --> RR /\ A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Im ` w ) - ( Im ` x ) ) ) < y ) ) ) )
7	4 5 6	mp2an	|- ( Im e. ( CC -cn-> RR ) <-> ( Im : CC --> RR /\ A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Im ` w ) - ( Im ` x ) ) ) < y ) ) )
8	1 3 7	mpbir2an	|- Im e. ( CC -cn-> RR )