Theorem logimclad

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

	Ref	Expression
Hypotheses	logimcld.1	$$⊢\phi \to X\in ℂ$$
	logimcld.2	$$⊢\phi \to X\ne 0$$
Assertion	logimclad	$$⊢\phi \to \Im \left(\log X\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$$

Proof

Step	Hyp	Ref	Expression
1		logimcld.1	$$⊢\phi \to X\in ℂ$$
2		logimcld.2	$$⊢\phi \to X\ne 0$$
3	1 2	logcld	$$⊢\phi \to \log X\in ℂ$$
4	3	imcld	$$⊢\phi \to \Im \left(\log X\right)\in ℝ$$
5	1 2	logimcld	$$⊢\phi \to \left(-\mathrm{\pi }<\Im \left(\log X\right)\wedge \Im \left(\log X\right)\le \mathrm{\pi }\right)$$
6	5	simpld	$$⊢\phi \to -\mathrm{\pi }<\Im \left(\log X\right)$$
7	5	simprd	$$⊢\phi \to \Im \left(\log X\right)\le \mathrm{\pi }$$
8		pire	$$⊢\mathrm{\pi }\in ℝ$$
9	8	renegcli	$$⊢-\mathrm{\pi }\in ℝ$$
10	9	rexri	$$⊢-\mathrm{\pi }\in {ℝ}^{*}$$
11		elioc2	$$⊢\left(-\mathrm{\pi }\in {ℝ}^{*}\wedge \mathrm{\pi }\in ℝ\right)\to \left(\Im \left(\log X\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\leftrightarrow \left(\Im \left(\log X\right)\in ℝ\wedge -\mathrm{\pi }<\Im \left(\log X\right)\wedge \Im \left(\log X\right)\le \mathrm{\pi }\right)\right)$$
12	10 8 11	mp2an	$$⊢\Im \left(\log X\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]\leftrightarrow \left(\Im \left(\log X\right)\in ℝ\wedge -\mathrm{\pi }<\Im \left(\log X\right)\wedge \Im \left(\log X\right)\le \mathrm{\pi }\right)$$
13	4 6 7 12	syl3anbrc	$$⊢\phi \to \Im \left(\log X\right)\in \left(-\mathrm{\pi },\mathrm{\pi }\right]$$