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	$$⊢\phi \to X\in ℂ$$
	logimcld.2	$$⊢\phi \to X\ne 0$$
Assertion	logimcld	$$⊢\phi \to \left(-\mathrm{\pi }<\Im \left(\log X\right)\wedge \Im \left(\log X\right)\le \mathrm{\pi }\right)$$

Proof

Step	Hyp	Ref	Expression
1		logimcld.1	$$⊢\phi \to X\in ℂ$$
2		logimcld.2	$$⊢\phi \to X\ne 0$$
3		logimcl	$$⊢\left(X\in ℂ\wedge X\ne 0\right)\to \left(-\mathrm{\pi }<\Im \left(\log X\right)\wedge \Im \left(\log X\right)\le \mathrm{\pi }\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(-\mathrm{\pi }<\Im \left(\log X\right)\wedge \Im \left(\log X\right)\le \mathrm{\pi }\right)$$