Metamath Proof Explorer


Theorem ellogdm

Description: Elementhood in the "continuous domain" of the complex logarithm. (Contributed by Mario Carneiro, 18-Feb-2015)

Ref Expression
Hypothesis logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion ellogdm ( 𝐴𝐷 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )

Proof

Step Hyp Ref Expression
1 logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 1 eleq2i ( 𝐴𝐷𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) )
3 eldif ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) ↔ ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ( -∞ (,] 0 ) ) )
4 mnfxr -∞ ∈ ℝ*
5 0re 0 ∈ ℝ
6 elioc2 ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( 𝐴 ∈ ( -∞ (,] 0 ) ↔ ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴𝐴 ≤ 0 ) ) )
7 4 5 6 mp2an ( 𝐴 ∈ ( -∞ (,] 0 ) ↔ ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴𝐴 ≤ 0 ) )
8 df-3an ( ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴𝐴 ≤ 0 ) ↔ ( ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴 ) ∧ 𝐴 ≤ 0 ) )
9 mnflt ( 𝐴 ∈ ℝ → -∞ < 𝐴 )
10 9 pm4.71i ( 𝐴 ∈ ℝ ↔ ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴 ) )
11 10 anbi1i ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) ↔ ( ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴 ) ∧ 𝐴 ≤ 0 ) )
12 lenlt ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 ≤ 0 ↔ ¬ 0 < 𝐴 ) )
13 5 12 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 0 ↔ ¬ 0 < 𝐴 ) )
14 elrp ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
15 14 baib ( 𝐴 ∈ ℝ → ( 𝐴 ∈ ℝ+ ↔ 0 < 𝐴 ) )
16 15 notbid ( 𝐴 ∈ ℝ → ( ¬ 𝐴 ∈ ℝ+ ↔ ¬ 0 < 𝐴 ) )
17 13 16 bitr4d ( 𝐴 ∈ ℝ → ( 𝐴 ≤ 0 ↔ ¬ 𝐴 ∈ ℝ+ ) )
18 17 pm5.32i ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≤ 0 ) ↔ ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ+ ) )
19 11 18 bitr3i ( ( ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴 ) ∧ 𝐴 ≤ 0 ) ↔ ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ+ ) )
20 7 8 19 3bitri ( 𝐴 ∈ ( -∞ (,] 0 ) ↔ ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ+ ) )
21 20 notbii ( ¬ 𝐴 ∈ ( -∞ (,] 0 ) ↔ ¬ ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ+ ) )
22 iman ( ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ↔ ¬ ( 𝐴 ∈ ℝ ∧ ¬ 𝐴 ∈ ℝ+ ) )
23 21 22 bitr4i ( ¬ 𝐴 ∈ ( -∞ (,] 0 ) ↔ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) )
24 23 anbi2i ( ( 𝐴 ∈ ℂ ∧ ¬ 𝐴 ∈ ( -∞ (,] 0 ) ) ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )
25 2 3 24 3bitri ( 𝐴𝐷 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )