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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π )

Proof

Step	Hyp	Ref	Expression
1		pire	⊢ π ∈ ℝ
2	1	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → π ∈ ℝ )
3	2	renegcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π ∈ ℝ )
4		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
5	4	imcld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ∈ ℝ )
6		logimcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
7	6	simpld	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) )
8	3 5 7	ltled	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) )
9	6	simprd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π )
10	5 2	absled	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π ↔ ( - π ≤ ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) ) )
11	8 9 10	mpbir2and	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( abs ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) ≤ π )