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 = ℂ ∖ (−∞, 0]$
	Assertion	logdmnrp	$⊢ A \in D \to \neg - A \in ℝ^{+}$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		eldifn	$⊢ A \in (ℂ ∖ (−∞, 0]) \to \neg A \in (−∞, 0]$
3	2 1	eleq2s	$⊢ A \in D \to \neg A \in (−∞, 0]$
4		rpre	$⊢ - A \in ℝ^{+} \to - A \in ℝ$
5	1	ellogdm	$⊢ A \in D \leftrightarrow (A \in ℂ \land (A \in ℝ \to A \in ℝ^{+}))$
6	5	simplbi	$⊢ A \in D \to A \in ℂ$
7		negreb	$⊢ A \in ℂ \to (- A \in ℝ \leftrightarrow A \in ℝ)$
8	6 7	syl	$⊢ A \in D \to (- A \in ℝ \leftrightarrow A \in ℝ)$
9	4 8	syl5ib	$⊢ A \in D \to (- A \in ℝ^{+} \to A \in ℝ)$
10	9	imp	$⊢ (A \in D \land - A \in ℝ^{+}) \to A \in ℝ$
11	10	mnfltd	$⊢ (A \in D \land - A \in ℝ^{+}) \to −∞ < A$
12		rpgt0	$⊢ - A \in ℝ^{+} \to 0 < - A$
13	12	adantl	$⊢ (A \in D \land - A \in ℝ^{+}) \to 0 < - A$
14	10	lt0neg1d	$⊢ (A \in D \land - A \in ℝ^{+}) \to (A < 0 \leftrightarrow 0 < - A)$
15	13 14	mpbird	$⊢ (A \in D \land - A \in ℝ^{+}) \to A < 0$
16		0re	$⊢ 0 \in ℝ$
17		ltle	$⊢ (A \in ℝ \land 0 \in ℝ) \to (A < 0 \to A \leq 0)$
18	10 16 17	sylancl	$⊢ (A \in D \land - A \in ℝ^{+}) \to (A < 0 \to A \leq 0)$
19	15 18	mpd	$⊢ (A \in D \land - A \in ℝ^{+}) \to A \leq 0$
20		mnfxr	$⊢ −∞ \in ℝ^{*}$
21		elioc2	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (A \in (−∞, 0] \leftrightarrow (A \in ℝ \land −∞ < A \land A \leq 0))$
22	20 16 21	mp2an	$⊢ A \in (−∞, 0] \leftrightarrow (A \in ℝ \land −∞ < A \land A \leq 0)$
23	10 11 19 22	syl3anbrc	$⊢ (A \in D \land - A \in ℝ^{+}) \to A \in (−∞, 0]$
24	3 23	mtand	$⊢ A \in D \to \neg - A \in ℝ^{+}$

Metamath Proof Explorer

Theorem logdmnrp

Proof