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