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 pire π ∈ ℝ
6 5 renegcli - π ∈ ℝ
7 6 rexri - π ∈ ℝ*
8 elioc2 ( ( - π ∈ ℝ* ∧ π ∈ ℝ ) → ( ( ℑ ‘ 𝐴 ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ) )
9 7 5 8 mp2an ( ( ℑ ‘ 𝐴 ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) )
10 3anass ( ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ↔ ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ ( - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ) )
11 9 10 bitri ( ( ℑ ‘ 𝐴 ) ∈ ( - π (,] π ) ↔ ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ ( - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ) )
12 imcl ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) ∈ ℝ )
13 12 biantrurd ( 𝐴 ∈ ℂ → ( ( - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ↔ ( ( ℑ ‘ 𝐴 ) ∈ ℝ ∧ ( - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ) ) )
14 11 13 bitr4id ( 𝐴 ∈ ℂ → ( ( ℑ ‘ 𝐴 ) ∈ ( - π (,] π ) ↔ ( - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) ) )
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 ↔ ( 𝐴 ∈ ℂ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) )