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

Metamath Proof Explorer

Theorem ellogdm

Proof