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	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
Assertion	logdmss	⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		logcn.d	⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2	1	ellogdm	⊢ ( 𝑥 ∈ 𝐷 ↔ ( 𝑥 ∈ ℂ ∧ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ+ ) ) )
3	2	simplbi	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ℂ )
4	1	logdmn0	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ≠ 0 )
5		eldifsn	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
6	3 4 5	sylanbrc	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ( ℂ ∖ { 0 } ) )
7	6	ssriv	⊢ 𝐷 ⊆ ( ℂ ∖ { 0 } )