Metamath Proof Explorer

Theorem ellogrn

Description: Write out the property A e. ran log explicitly. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion ellogrn ⊢ A ∈ ran ⁡ log ↔ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π

Proof

Step Hyp Ref Expression
1 imf ⊢ ℑ : ℂ ⟶ ℝ
2 ffn ⊢ ℑ : ℂ ⟶ ℝ → ℑ Fn ℂ
3 elpreima ⊢ ℑ Fn ℂ → A ∈ ℑ -1 − π π ↔ A ∈ ℂ ∧ ℑ ⁡ A ∈ − π π
4 1 2 3 mp2b ⊢ A ∈ ℑ -1 − π π ↔ A ∈ ℂ ∧ ℑ ⁡ A ∈ − π π
5 pire ⊢ π ∈ ℝ
6 5 renegcli ⊢ − π ∈ ℝ
7 6 rexri ⊢ − π ∈ ℝ *
8 elioc2 ⊢ − π ∈ ℝ * ∧ π ∈ ℝ → ℑ ⁡ A ∈ − π π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
9 7 5 8 mp2an ⊢ ℑ ⁡ A ∈ − π π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
10 3anass ⊢ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
11 9 10 bitri ⊢ ℑ ⁡ A ∈ − π π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
12 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
13 12 biantrurd ⊢ A ∈ ℂ → − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
14 11 13 bitr4id ⊢ A ∈ ℂ → ℑ ⁡ A ∈ − π π ↔ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
15 14 pm5.32i ⊢ A ∈ ℂ ∧ ℑ ⁡ A ∈ − π π ↔ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
16 4 15 bitri ⊢ A ∈ ℑ -1 − π π ↔ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
17 logrn ⊢ ran ⁡ log = ℑ -1 − π π
18 17 eleq2i ⊢ A ∈ ran ⁡ log ↔ A ∈ ℑ -1 − π π
19 3anass ⊢ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π ↔ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
20 16 18 19 3bitr4i ⊢ A ∈ ran ⁡ log ↔ A ∈ ℂ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π