Theorem logimcld

Description: The imaginary part of the logarithm is in ( -upi (,] pi ) . Deduction form of logimcl . Compare logimclad . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	logimcld.1	|- ( ph -> X e. CC )
	logimcld.2	|- ( ph -> X =/= 0 )
Assertion	logimcld	|- ( ph -> ( -u _pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ _pi ) )

Proof

Step	Hyp	Ref	Expression
1		logimcld.1	|- ( ph -> X e. CC )
2		logimcld.2	|- ( ph -> X =/= 0 )
3		logimcl	|- ( ( X e. CC /\ X =/= 0 ) -> ( -u _pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ _pi ) )
4	1 2 3	syl2anc	|- ( ph -> ( -u _pi < ( Im ` ( log ` X ) ) /\ ( Im ` ( log ` X ) ) <_ _pi ) )