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 = ( CC \ ( -oo (,] 0 ) )
Assertion ellogdm
|- ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )

Proof

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+ ) ) )