This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℂ ∧ A ≠ 0 → ℑ ⁡ log ⁡ A ≤ π

Proof

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