Metamath Proof Explorer


Theorem logdmn0

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

Ref Expression
Hypothesis logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion logdmn0 ( 𝐴𝐷𝐴 ≠ 0 )

Proof

Step Hyp Ref Expression
1 logcn.d 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 0nrp ¬ 0 ∈ ℝ+
3 0re 0 ∈ ℝ
4 1 ellogdm ( 0 ∈ 𝐷 ↔ ( 0 ∈ ℂ ∧ ( 0 ∈ ℝ → 0 ∈ ℝ+ ) ) )
5 4 simprbi ( 0 ∈ 𝐷 → ( 0 ∈ ℝ → 0 ∈ ℝ+ ) )
6 3 5 mpi ( 0 ∈ 𝐷 → 0 ∈ ℝ+ )
7 2 6 mto ¬ 0 ∈ 𝐷
8 eleq1 ( 𝐴 = 0 → ( 𝐴𝐷 ↔ 0 ∈ 𝐷 ) )
9 7 8 mtbiri ( 𝐴 = 0 → ¬ 𝐴𝐷 )
10 9 necon2ai ( 𝐴𝐷𝐴 ≠ 0 )