Theorem logcld

Description: The logarithm of a nonzero complex number is a complex number. Deduction form of logcl . (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	logcld.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	logcld.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
Assertion	logcld	⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		logcld.1	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
2		logcld.2	⊢ ( 𝜑 → 𝑋 ≠ 0 )
3		logcl	⊢ ( ( 𝑋 ∈ ℂ ∧ 𝑋 ≠ 0 ) → ( log ‘ 𝑋 ) ∈ ℂ )
4	1 2 3	syl2anc	⊢ ( 𝜑 → ( log ‘ 𝑋 ) ∈ ℂ )