Theorem abslogle

Description: Bound on the magnitude of the complex logarithm function. (Contributed by Mario Carneiro, 3-Jul-2017)

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

Proof

Step	Hyp	Ref	Expression
1		logcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in ℂ$$
2	1	abscld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log A\right|\in ℝ$$
3		absrpcl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|A\right|\in {ℝ}^{+}$$
4		relogcl	$$⊢\left|A\right|\in {ℝ}^{+}\to \log \left|A\right|\in ℝ$$
5	3 4	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log \left|A\right|\in ℝ$$
6	5	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log \left|A\right|\in ℂ$$
7	6	abscld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log \left|A\right|\right|\in ℝ$$
8	1	imcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℝ$$
9	8	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Im \left(\log A\right)\in ℂ$$
10	9	abscld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\Im \left(\log A\right)\right|\in ℝ$$
11	7 10	readdcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log \left|A\right|\right|+\left|\Im \left(\log A\right)\right|\in ℝ$$
12		pire	$$⊢\mathrm{\pi }\in ℝ$$
13	12	a1i	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \mathrm{\pi }\in ℝ$$
14	7 13	readdcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log \left|A\right|\right|+\mathrm{\pi }\in ℝ$$
15	1	recld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℝ$$
16	15	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)\in ℂ$$
17		ax-icn	$$⊢\mathrm{i}\in ℂ$$
18	17	a1i	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \mathrm{i}\in ℂ$$
19	18 9	mulcld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \mathrm{i}\Im \left(\log A\right)\in ℂ$$
20	16 19	abstrid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)\right|\le \left|\Re \left(\log A\right)\right|+\left|\mathrm{i}\Im \left(\log A\right)\right|$$
21	1	replimd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A=\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)$$
22	21	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log A\right|=\left|\Re \left(\log A\right)+\mathrm{i}\Im \left(\log A\right)\right|$$
23		relog	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \Re \left(\log A\right)=\log \left|A\right|$$
24	23	eqcomd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log \left|A\right|=\Re \left(\log A\right)$$
25	24	fveq2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log \left|A\right|\right|=\left|\Re \left(\log A\right)\right|$$
26	18 9	absmuld	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\mathrm{i}\Im \left(\log A\right)\right|=\left|\mathrm{i}\right|\left|\Im \left(\log A\right)\right|$$
27		absi	$$⊢\left|\mathrm{i}\right|=1$$
28	27	oveq1i	$$⊢\left|\mathrm{i}\right|\left|\Im \left(\log A\right)\right|=1\left|\Im \left(\log A\right)\right|$$
29	10	recnd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\Im \left(\log A\right)\right|\in ℂ$$
30	29	mulid2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to 1\left|\Im \left(\log A\right)\right|=\left|\Im \left(\log A\right)\right|$$
31	28 30	eqtrid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\mathrm{i}\right|\left|\Im \left(\log A\right)\right|=\left|\Im \left(\log A\right)\right|$$
32	26 31	eqtr2d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\Im \left(\log A\right)\right|=\left|\mathrm{i}\Im \left(\log A\right)\right|$$
33	25 32	oveq12d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log \left|A\right|\right|+\left|\Im \left(\log A\right)\right|=\left|\Re \left(\log A\right)\right|+\left|\mathrm{i}\Im \left(\log A\right)\right|$$
34	20 22 33	3brtr4d	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log A\right|\le \left|\log \left|A\right|\right|+\left|\Im \left(\log A\right)\right|$$
35		abslogimle	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\Im \left(\log A\right)\right|\le \mathrm{\pi }$$
36	10 13 7 35	leadd2dd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log \left|A\right|\right|+\left|\Im \left(\log A\right)\right|\le \left|\log \left|A\right|\right|+\mathrm{\pi }$$
37	2 11 14 34 36	letrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left|\log A\right|\le \left|\log \left|A\right|\right|+\mathrm{\pi }$$