Theorem logrncl

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

	Ref	Expression
Assertion	logrncl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
2		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
3		f1of	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log : ( ℂ ∖ { 0 } ) ⟶ ran log )
4	2 3	ax-mp	⊢ log : ( ℂ ∖ { 0 } ) ⟶ ran log
5	4	ffvelrni	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝐴 ) ∈ ran log )
6	1 5	sylbir	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )