Metamath Proof Explorer


Theorem logimcl

Description: Closure of the imaginary part of the logarithm function. (Contributed by Mario Carneiro, 23-Sep-2014) (Revised by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion logimcl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )

Proof

Step Hyp Ref Expression
1 logrncl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )
2 ellogrn ( ( log ‘ 𝐴 ) ∈ ran log ↔ ( ( log ‘ 𝐴 ) ∈ ℂ ∧ - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
3 1 2 sylib ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( log ‘ 𝐴 ) ∈ ℂ ∧ - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
4 3simpc ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )
5 3 4 syl ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( - π < ( ℑ ‘ ( log ‘ 𝐴 ) ) ∧ ( ℑ ‘ ( log ‘ 𝐴 ) ) ≤ π ) )