Metamath Proof Explorer


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 ‘ 𝐴 ) ) ) ≤ π )