Theorem logrncl

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

	Ref	Expression
Assertion	logrncl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in \mathrm{ran}log$$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(A\in ℂ\wedge A\ne 0\right)$$
2		logf1o	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
3		f1of	$$⊢log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\to log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
4	2 3	ax-mp	$$⊢log:ℂ\setminus \left\{0\right\}⟶\mathrm{ran}log$$
5	4	ffvelrni	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to \log A\in \mathrm{ran}log$$
6	1 5	sylbir	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \log A\in \mathrm{ran}log$$