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	|- ( ph -> X e. CC )
	logcld.2	|- ( ph -> X =/= 0 )
Assertion	logcld	|- ( ph -> ( log ` X ) e. CC )

Proof

Step	Hyp	Ref	Expression
1		logcld.1	|- ( ph -> X e. CC )
2		logcld.2	|- ( ph -> X =/= 0 )
3		logcl	|- ( ( X e. CC /\ X =/= 0 ) -> ( log ` X ) e. CC )
4	1 2 3	syl2anc	|- ( ph -> ( log ` X ) e. CC )