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 imcl ⊢ A ∈ ℂ → ℑ ⁡ A ∈ ℝ
6 5 biantrurd ⊢ A ∈ ℂ → − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
7 pire ⊢ π ∈ ℝ
8 7 renegcli ⊢ − π ∈ ℝ
9 8 rexri ⊢ − π ∈ ℝ *
10 elioc2 ⊢ − π ∈ ℝ * ∧ π ∈ ℝ → ℑ ⁡ A ∈ − π π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
11 9 7 10 mp2an ⊢ ℑ ⁡ A ∈ − π π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
12 3anass ⊢ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
13 11 12 bitri ⊢ ℑ ⁡ A ∈ − π π ↔ ℑ ⁡ A ∈ ℝ ∧ − π < ℑ ⁡ A ∧ ℑ ⁡ A ≤ π
14 6 13 syl6rbbr ⊢ 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 ≤ π