This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ∈ 𝐷 → ¬ - 𝐴 ∈ ℝ+ )