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