Theorem logrncl

Description: Closure of the natural logarithm function. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	logrncl	|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
2		logf1o	|- log : ( CC \ { 0 } ) -1-1-onto-> ran log
3		f1of	|- ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log : ( CC \ { 0 } ) --> ran log )
4	2 3	ax-mp	|- log : ( CC \ { 0 } ) --> ran log
5	4	ffvelrni	|- ( A e. ( CC \ { 0 } ) -> ( log ` A ) e. ran log )
6	1 5	sylbir	|- ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. ran log )