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 ( 𝐴 ∈ ran log ↔ ( 𝐴 ∈ ℂ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) )

Proof

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