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	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	logdmn0	$$⊢A\in D\to A\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		0nrp	$$⊢\neg 0\in {ℝ}^{+}$$
3		0re	$$⊢0\in ℝ$$
4	1	ellogdm	$$⊢0\in D\leftrightarrow \left(0\in ℂ\wedge \left(0\in ℝ\to 0\in {ℝ}^{+}\right)\right)$$
5	4	simprbi	$$⊢0\in D\to \left(0\in ℝ\to 0\in {ℝ}^{+}\right)$$
6	3 5	mpi	$$⊢0\in D\to 0\in {ℝ}^{+}$$
7	2 6	mto	$$⊢\neg 0\in D$$
8		eleq1	$$⊢A=0\to \left(A\in D\leftrightarrow 0\in D\right)$$
9	7 8	mtbiri	$$⊢A=0\to \neg A\in D$$
10	9	necon2ai	$$⊢A\in D\to A\ne 0$$