Metamath Proof Explorer

Theorem logimclad

Description: The imaginary part of the logarithm is in ( -upi (,] pi ) . Alternate form of logimcld . (Contributed by David Moews, 28-Feb-2017)

Ref Expression
Hypotheses logimcld.1 ⊢ φ → X ∈ ℂ
logimcld.2 ⊢ φ → X ≠ 0
Assertion logimclad ⊢ φ → ℑ ⁡ log ⁡ X ∈ − π π

Proof

Step Hyp Ref Expression
1 logimcld.1 ⊢ φ → X ∈ ℂ
2 logimcld.2 ⊢ φ → X ≠ 0
3 1 2 logcld ⊢ φ → log ⁡ X ∈ ℂ
4 3 imcld ⊢ φ → ℑ ⁡ log ⁡ X ∈ ℝ
5 1 2 logimcld ⊢ φ → − π < ℑ ⁡ log ⁡ X ∧ ℑ ⁡ log ⁡ X ≤ π
6 5 simpld ⊢ φ → − π < ℑ ⁡ log ⁡ X
7 5 simprd ⊢ φ → ℑ ⁡ log ⁡ X ≤ π
8 pire ⊢ π ∈ ℝ
9 8 renegcli ⊢ − π ∈ ℝ
10 9 rexri ⊢ − π ∈ ℝ *
11 elioc2 ⊢ − π ∈ ℝ * ∧ π ∈ ℝ → ℑ ⁡ log ⁡ X ∈ − π π ↔ ℑ ⁡ log ⁡ X ∈ ℝ ∧ − π < ℑ ⁡ log ⁡ X ∧ ℑ ⁡ log ⁡ X ≤ π
12 10 8 11 mp2an ⊢ ℑ ⁡ log ⁡ X ∈ − π π ↔ ℑ ⁡ log ⁡ X ∈ ℝ ∧ − π < ℑ ⁡ log ⁡ X ∧ ℑ ⁡ log ⁡ X ≤ π
13 4 6 7 12 syl3anbrc ⊢ φ → ℑ ⁡ log ⁡ X ∈ − π π