Theorem argrege0

Description: Closure of the argument of a complex number with nonnegative real part. (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	argrege0	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
2	1	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
3	2	imcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
4		simp3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ 𝐴 ) )
5		simp1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
6	5	abscld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ )
7	6	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℂ )
8	7	mul01d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) = 0 )
9		absrpcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
10	9	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ∈ ℝ+ )
11	10	rpne0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ 𝐴 ) ≠ 0 )
12	5 7 11	divcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 𝐴 / ( abs ‘ 𝐴 ) ) ∈ ℂ )
13	6 12	remul2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) )
14	5 7 11	divcan2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) = 𝐴 )
15	14	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( ( abs ‘ 𝐴 ) · ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℜ ‘ 𝐴 ) )
16	13 15	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) = ( ℜ ‘ 𝐴 ) )
17	4 8 16	3brtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ 𝐴 ) · 0 ) ≤ ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) )
18		0re	⊢ 0 ∈ ℝ
19	18	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ∈ ℝ )
20	12	recld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ∈ ℝ )
21	19 20 10	lemul2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 0 ≤ ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ↔ ( ( abs ‘ 𝐴 ) · 0 ) ≤ ( ( abs ‘ 𝐴 ) · ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) ) ) )
22	17 21	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) )
23		efiarg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
24	23	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( 𝐴 / ( abs ‘ 𝐴 ) ) )
25	24	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) = ( ℜ ‘ ( 𝐴 / ( abs ‘ 𝐴 ) ) ) )
26	22 25	breqtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
27		recosval	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
28	3 27	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℜ ‘ ( exp ‘ ( i · ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) ) )
29	26 28	breqtrrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
30		halfpire	⊢ ( π / 2 ) ∈ ℝ
31		pirp	⊢ π ∈ ℝ+
32		rphalfcl	⊢ ( π ∈ ℝ+ → ( π / 2 ) ∈ ℝ+ )
33		rpge0	⊢ ( ( π / 2 ) ∈ ℝ+ → 0 ≤ ( π / 2 ) )
34	31 32 33	mp2b	⊢ 0 ≤ ( π / 2 )
35		pire	⊢ π ∈ ℝ
36		rphalflt	⊢ ( π ∈ ℝ+ → ( π / 2 ) < π )
37	31 36	ax-mp	⊢ ( π / 2 ) < π
38	30 35 37	ltleii	⊢ ( π / 2 ) ≤ π
39	18 35	elicc2i	⊢ ( ( π / 2 ) ∈ ( 0 [,] π ) ↔ ( ( π / 2 ) ∈ ℝ ∧ 0 ≤ ( π / 2 ) ∧ ( π / 2 ) ≤ π ) )
40	30 34 38 39	mpbir3an	⊢ ( π / 2 ) ∈ ( 0 [,] π )
41	3	recnd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ )
42	41	abscld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
43	41	absge0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
44		logimcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
45	44	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
46	45	simpld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
47	35	renegcli	⊢ - π ∈ ℝ
48		ltle	⊢ ( ( - π ∈ ℝ ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
49	47 3 48	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
50	46 49	mpd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
51	45	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
52		absle	⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
53	3 35 52	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
54	50 51 53	mpbir2and	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π )
55	18 35	elicc2i	⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ↔ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∧ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ) )
56	42 43 54 55	syl3anbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) )
57		cosord	⊢ ( ( ( π / 2 ) ∈ ( 0 [,] π ) ∧ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ( 0 [,] π ) ) → ( ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) < ( cos ‘ ( π / 2 ) ) ) )
58	40 56 57	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) < ( cos ‘ ( π / 2 ) ) ) )
59		fveq2	⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
60	59	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
61		cosneg	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℂ → ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
62	41 61	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
63		fveqeq2	⊢ ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
64	62 63	syl5ibrcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
65	3	absord	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ℑ ‘ ( log ‘ 𝐴 ) ) ∨ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = - ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
66	60 64 65	mpjaod	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) = ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) )
67		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
68	67	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( π / 2 ) ) = 0 )
69	66 68	breq12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( cos ‘ ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) < ( cos ‘ ( π / 2 ) ) ↔ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) )
70	58 69	bitrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) )
71	70	notbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ¬ ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ¬ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) )
72		lenlt	⊢ ( ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ¬ ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
73	42 30 72	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ¬ ( π / 2 ) < ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
74	3	recoscld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ )
75		lenlt	⊢ ( ( 0 ∈ ℝ ∧ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ∈ ℝ ) → ( 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ¬ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) )
76	18 74 75	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ↔ ¬ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) < 0 ) )
77	71 73 76	3bitr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ 0 ≤ ( cos ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ) )
78	29 77	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) )
79		absle	⊢ ( ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ( - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) ) )
80	3 30 79	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ ( π / 2 ) ↔ ( - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) ) )
81	78 80	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
82	81	simpld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
83	81	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) )
84	30	renegcli	⊢ - ( π / 2 ) ∈ ℝ
85	84 30	elicc2i	⊢ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) ↔ ( ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ ∧ - ( π / 2 ) ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ ( π / 2 ) ) )
86	3 82 83 85	syl3anbrc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )