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	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion	logdmnrp	⊢ ( 𝐴 ∈ 𝐷 → ¬ - 𝐴 ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		logcn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2		eldifn	⊢ ( 𝐴 ∈ ( ℂ ∖ ( -∞ (,] 0 ) ) → ¬ 𝐴 ∈ ( -∞ (,] 0 ) )
3	2 1	eleq2s	⊢ ( 𝐴 ∈ 𝐷 → ¬ 𝐴 ∈ ( -∞ (,] 0 ) )
4		rpre	⊢ ( - 𝐴 ∈ ℝ+ → - 𝐴 ∈ ℝ )
5	1	ellogdm	⊢ ( 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )
6	5	simplbi	⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ∈ ℂ )
7		negreb	⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ ) )
8	6 7	syl	⊢ ( 𝐴 ∈ 𝐷 → ( - 𝐴 ∈ ℝ ↔ 𝐴 ∈ ℝ ) )
9	4 8	imbitrid	⊢ ( 𝐴 ∈ 𝐷 → ( - 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ ) )
10	9	imp	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
11	10	mnfltd	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → -∞ < 𝐴 )
12		rpgt0	⊢ ( - 𝐴 ∈ ℝ+ → 0 < - 𝐴 )
13	12	adantl	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → 0 < - 𝐴 )
14	10	lt0neg1d	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) )
15	13 14	mpbird	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → 𝐴 < 0 )
16		0re	⊢ 0 ∈ ℝ
17		ltle	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
18	10 16 17	sylancl	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → ( 𝐴 < 0 → 𝐴 ≤ 0 ) )
19	15 18	mpd	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → 𝐴 ≤ 0 )
20		mnfxr	⊢ -∞ ∈ ℝ*
21		elioc2	⊢ ( ( -∞ ∈ ℝ* ∧ 0 ∈ ℝ ) → ( 𝐴 ∈ ( -∞ (,] 0 ) ↔ ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴 ∧ 𝐴 ≤ 0 ) ) )
22	20 16 21	mp2an	⊢ ( 𝐴 ∈ ( -∞ (,] 0 ) ↔ ( 𝐴 ∈ ℝ ∧ -∞ < 𝐴 ∧ 𝐴 ≤ 0 ) )
23	10 11 19 22	syl3anbrc	⊢ ( ( 𝐴 ∈ 𝐷 ∧ - 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ( -∞ (,] 0 ) )
24	3 23	mtand	⊢ ( 𝐴 ∈ 𝐷 → ¬ - 𝐴 ∈ ℝ+ )