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	$$⊢\phi \to X\in ℂ$$
	logcld.2	$$⊢\phi \to X\ne 0$$
Assertion	logcld	$$⊢\phi \to \log X\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		logcld.1	$$⊢\phi \to X\in ℂ$$
2		logcld.2	$$⊢\phi \to X\ne 0$$
3		logcl	$$⊢\left(X\in ℂ\wedge X\ne 0\right)\to \log X\in ℂ$$
4	1 2 3	syl2anc	$$⊢\phi \to \log X\in ℂ$$