Theorem logdmnrp

Description: A number in the continuous domain of log is not a strictly negative number. (Contributed by Mario Carneiro, 18-Feb-2015)

	Ref	Expression
Hypothesis	logcn.d	|- D = ( CC \ ( -oo (,] 0 ) )
Assertion	logdmnrp	|- ( A e. D -> -. -u A e. RR+ )

Proof

Step	Hyp	Ref	Expression
1		logcn.d	|- D = ( CC \ ( -oo (,] 0 ) )
2		eldifn	|- ( A e. ( CC \ ( -oo (,] 0 ) ) -> -. A e. ( -oo (,] 0 ) )
3	2 1	eleq2s	|- ( A e. D -> -. A e. ( -oo (,] 0 ) )
4		rpre	|- ( -u A e. RR+ -> -u A e. RR )
5	1	ellogdm	|- ( A e. D <-> ( A e. CC /\ ( A e. RR -> A e. RR+ ) ) )
6	5	simplbi	|- ( A e. D -> A e. CC )
7		negreb	|- ( A e. CC -> ( -u A e. RR <-> A e. RR ) )
8	6 7	syl	|- ( A e. D -> ( -u A e. RR <-> A e. RR ) )
9	4 8	syl5ib	|- ( A e. D -> ( -u A e. RR+ -> A e. RR ) )
10	9	imp	|- ( ( A e. D /\ -u A e. RR+ ) -> A e. RR )
11	10	mnfltd	|- ( ( A e. D /\ -u A e. RR+ ) -> -oo < A )
12		rpgt0	|- ( -u A e. RR+ -> 0 < -u A )
13	12	adantl	|- ( ( A e. D /\ -u A e. RR+ ) -> 0 < -u A )
14	10	lt0neg1d	|- ( ( A e. D /\ -u A e. RR+ ) -> ( A < 0 <-> 0 < -u A ) )
15	13 14	mpbird	|- ( ( A e. D /\ -u A e. RR+ ) -> A < 0 )
16		0re	|- 0 e. RR
17		ltle	|- ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 -> A <_ 0 ) )
18	10 16 17	sylancl	|- ( ( A e. D /\ -u A e. RR+ ) -> ( A < 0 -> A <_ 0 ) )
19	15 18	mpd	|- ( ( A e. D /\ -u A e. RR+ ) -> A <_ 0 )
20		mnfxr	|- -oo e. RR*
21		elioc2	|- ( ( -oo e. RR* /\ 0 e. RR ) -> ( A e. ( -oo (,] 0 ) <-> ( A e. RR /\ -oo < A /\ A <_ 0 ) ) )
22	20 16 21	mp2an	|- ( A e. ( -oo (,] 0 ) <-> ( A e. RR /\ -oo < A /\ A <_ 0 ) )
23	10 11 19 22	syl3anbrc	|- ( ( A e. D /\ -u A e. RR+ ) -> A e. ( -oo (,] 0 ) )
24	3 23	mtand	|- ( A e. D -> -. -u A e. RR+ )