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

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 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
logimcld.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion logimclad ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) )

Proof

Step Hyp Ref Expression
1 logimcld.1 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2 logimcld.2 ⊢ ( 𝜑 → 𝑋 ≠ 0 )
3 1 2 logcld ⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )
4 3 imcld ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ )
5 1 2 logimcld ⊢ ( 𝜑 → ( - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )
6 5 simpld ⊢ ( 𝜑 → - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) )
7 5 simprd ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π )
8 pire ⊢ π ∈ ℝ
9 8 renegcli ⊢ - π ∈ ℝ
10 9 rexri ⊢ - π ∈ ℝ*
11 elioc2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) ) )
12 10 8 11 mp2an ⊢ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ℝ ∧ - π < ( ℑ ‘ ( log ‘ 𝑋 ) ) ∧ ( ℑ ‘ ( log ‘ 𝑋 ) ) ≤ π ) )
13 4 6 7 12 syl3anbrc ⊢ ( 𝜑 → ( ℑ ‘ ( log ‘ 𝑋 ) ) ∈ ( - π (,] π ) )