This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )