Step |
Hyp |
Ref |
Expression |
1 |
|
logcn.d |
|- D = ( CC \ ( -oo (,] 0 ) ) |
2 |
1
|
eleq2i |
|- ( A e. D <-> A e. ( CC \ ( -oo (,] 0 ) ) ) |
3 |
|
eldif |
|- ( A e. ( CC \ ( -oo (,] 0 ) ) <-> ( A e. CC /\ -. A e. ( -oo (,] 0 ) ) ) |
4 |
|
mnfxr |
|- -oo e. RR* |
5 |
|
0re |
|- 0 e. RR |
6 |
|
elioc2 |
|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( A e. ( -oo (,] 0 ) <-> ( A e. RR /\ -oo < A /\ A <_ 0 ) ) ) |
7 |
4 5 6
|
mp2an |
|- ( A e. ( -oo (,] 0 ) <-> ( A e. RR /\ -oo < A /\ A <_ 0 ) ) |
8 |
|
df-3an |
|- ( ( A e. RR /\ -oo < A /\ A <_ 0 ) <-> ( ( A e. RR /\ -oo < A ) /\ A <_ 0 ) ) |
9 |
|
mnflt |
|- ( A e. RR -> -oo < A ) |
10 |
9
|
pm4.71i |
|- ( A e. RR <-> ( A e. RR /\ -oo < A ) ) |
11 |
10
|
anbi1i |
|- ( ( A e. RR /\ A <_ 0 ) <-> ( ( A e. RR /\ -oo < A ) /\ A <_ 0 ) ) |
12 |
|
lenlt |
|- ( ( A e. RR /\ 0 e. RR ) -> ( A <_ 0 <-> -. 0 < A ) ) |
13 |
5 12
|
mpan2 |
|- ( A e. RR -> ( A <_ 0 <-> -. 0 < A ) ) |
14 |
|
elrp |
|- ( A e. RR+ <-> ( A e. RR /\ 0 < A ) ) |
15 |
14
|
baib |
|- ( A e. RR -> ( A e. RR+ <-> 0 < A ) ) |
16 |
15
|
notbid |
|- ( A e. RR -> ( -. A e. RR+ <-> -. 0 < A ) ) |
17 |
13 16
|
bitr4d |
|- ( A e. RR -> ( A <_ 0 <-> -. A e. RR+ ) ) |
18 |
17
|
pm5.32i |
|- ( ( A e. RR /\ A <_ 0 ) <-> ( A e. RR /\ -. A e. RR+ ) ) |
19 |
11 18
|
bitr3i |
|- ( ( ( A e. RR /\ -oo < A ) /\ A <_ 0 ) <-> ( A e. RR /\ -. A e. RR+ ) ) |
20 |
7 8 19
|
3bitri |
|- ( A e. ( -oo (,] 0 ) <-> ( A e. RR /\ -. A e. RR+ ) ) |
21 |
20
|
notbii |
|- ( -. A e. ( -oo (,] 0 ) <-> -. ( A e. RR /\ -. A e. RR+ ) ) |
22 |
|
iman |
|- ( ( A e. RR -> A e. RR+ ) <-> -. ( A e. RR /\ -. A e. RR+ ) ) |
23 |
21 22
|
bitr4i |
|- ( -. A e. ( -oo (,] 0 ) <-> ( A e. RR -> A e. RR+ ) ) |
24 |
23
|
anbi2i |
|- ( ( A e. CC /\ -. A e. ( -oo (,] 0 ) ) <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) ) |
25 |
2 3 24
|
3bitri |
|- ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) ) |