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

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	$⊢ D = ℂ ∖ (−∞, 0]$
	Assertion	logdmn0	$⊢ A \in D \to A \neq 0$

Step	Hyp	Ref	Expression
1		logcn.d	$⊢ D = ℂ ∖ (−∞, 0]$
2		0nrp	$⊢ \neg 0 \in ℝ^{+}$
3		0re	$⊢ 0 \in ℝ$
4	1	ellogdm	$⊢ 0 \in D \leftrightarrow (0 \in ℂ \land (0 \in ℝ \to 0 \in ℝ^{+}))$
5	4	simprbi	$⊢ 0 \in D \to (0 \in ℝ \to 0 \in ℝ^{+})$
6	3 5	mpi	$⊢ 0 \in D \to 0 \in ℝ^{+}$
7	2 6	mto	$⊢ \neg 0 \in D$
8		eleq1	$⊢ A = 0 \to (A \in D \leftrightarrow 0 \in D)$
9	7 8	mtbiri	$⊢ A = 0 \to \neg A \in D$
10	9	necon2ai	$⊢ A \in D \to A \neq 0$