Theorem logimcl

Description: Closure of the imaginary part of the logarithm function. (Contributed by Mario Carneiro, 23-Sep-2014) (Revised by Mario Carneiro, 1-Apr-2015)

	Ref	Expression
Assertion	logimcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$

Proof

Step	Hyp	Ref	Expression
1		logrncl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in \mathrm{ran}log$$
2		ellogrn	$$⊢\log A\in \mathrm{ran}log\leftrightarrow \left(\log A\in ℂ\wedge -\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$
3	1 2	sylib	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\log A\in ℂ\wedge -\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$
4		3simpc	$$⊢\left(\log A\in ℂ\wedge -\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$
5	3 4	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(-\mathrm{\pi }<\Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)$$