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

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

Proof

Step Hyp Ref Expression
1 logrncl ⊢ A ∈ ℂ ∧ A ≠ 0 → log ⁡ A ∈ ran ⁡ log
2 ellogrn ⊢ log ⁡ A ∈ ran ⁡ log ↔ log ⁡ A ∈ ℂ ∧ − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
3 1 2 sylib ⊢ A ∈ ℂ ∧ A ≠ 0 → log ⁡ A ∈ ℂ ∧ − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
4 3simpc ⊢ log ⁡ A ∈ ℂ ∧ − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π
5 3 4 syl ⊢ A ∈ ℂ ∧ A ≠ 0 → − π < ℑ ⁡ log ⁡ A ∧ ℑ ⁡ log ⁡ A ≤ π