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

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	imbitrid	\|- ( 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+ )

Metamath Proof Explorer