Description: Closure of the natural logarithm function. (Contributed by NM, 21Apr2008) (Revised by Mario Carneiro, 23Sep2014)
Ref  Expression  

Assertion  logcl   ( ( A e. CC /\ A =/= 0 ) > ( log ` A ) e. CC ) 
Step  Hyp  Ref  Expression 

1  logrncl   ( ( A e. CC /\ A =/= 0 ) > ( log ` A ) e. ran log ) 

2  logrncn   ( ( log ` A ) e. ran log > ( log ` A ) e. CC ) 

3  1 2  syl   ( ( A e. CC /\ A =/= 0 ) > ( log ` A ) e. CC ) 