This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logrncl

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

		Ref	Expression
	Assertion	logrncl	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ran log$

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ A \in (ℂ ∖ \{0\}) \leftrightarrow (A \in ℂ \land A \neq 0)$
2		logf1o	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log$
3		f1of	$⊢ log : ℂ ∖ \{0\} \underset{1-1 onto}{⟶} ran log \to log : ℂ ∖ \{0\} ⟶ ran log$
4	2 3	ax-mp	$⊢ log : ℂ ∖ \{0\} ⟶ ran log$
5	4	ffvelcdmi	$⊢ A \in (ℂ ∖ \{0\}) \to \log A \in ran log$
6	1 5	sylbir	$⊢ (A \in ℂ \land A \neq 0) \to \log A \in ran log$