Theorem abslogimle

Description: The imaginary part of the logarithm function has absolute value less than pi. (Contributed by Mario Carneiro, 3-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		pire	$$⊢\mathrm{\pi }\in ℝ$$
2	1	a1i	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \mathrm{\pi }\in ℝ$$
3	2	renegcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -\mathrm{\pi }\in ℝ$$
4		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
5	4	imcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℝ$$
6		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)$$
7	6	simpld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -\mathrm{\pi }<\Im \left(\log A\right)$$
8	3 5 7	ltled	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to -\mathrm{\pi }\le \Im \left(\log A\right)$$
9	6	simprd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\le \mathrm{\pi }$$
10	5 2	absled	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(\left|\Im \left(\log A\right)\right|\le \mathrm{\pi }\leftrightarrow \left(-\mathrm{\pi }\le \Im \left(\log A\right)\wedge \Im \left(\log A\right)\le \mathrm{\pi }\right)\right)$$
11	8 9 10	mpbir2and	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\Im \left(\log A\right)\right|\le \mathrm{\pi }$$