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 ⊢ D = ℂ ∖ −∞ 0
Assertion ellogdm ⊢ A ∈ D ↔ A ∈ ℂ ∧ A ∈ ℝ → A ∈ ℝ +

Proof

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