Theorem logdmss

Description: The continuity domain of log is a subset of the regular domain of log . (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypothesis	logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
Assertion	logdmss	$$⊢D\subseteq ℂ\setminus \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2	1	ellogdm	$$⊢x\in D\leftrightarrow \left(x\in ℂ\wedge \left(x\in ℝ\to x\in {ℝ}^{+}\right)\right)$$
3	2	simplbi	$$⊢x\in D\to x\in ℂ$$
4	1	logdmn0	$$⊢x\in D\to x\ne 0$$
5		eldifsn	$$⊢x\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(x\in ℂ\wedge x\ne 0\right)$$
6	3 4 5	sylanbrc	$$⊢x\in D\to x\in \left(ℂ\setminus \left\{0\right\}\right)$$
7	6	ssriv	$$⊢D\subseteq ℂ\setminus \left\{0\right\}$$