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