Theorem eflog

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Paul Chapman, 21-Apr-2008)

	Ref	Expression
Assertion	eflog	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dflog2	⊢ log = ◡ ( exp ↾ ran log )
2	1	fveq1i	⊢ ( log ‘ 𝐴 ) = ( ◡ ( exp ↾ ran log ) ‘ 𝐴 )
3	2	fveq2i	⊢ ( ( exp ↾ ran log ) ‘ ( log ‘ 𝐴 ) ) = ( ( exp ↾ ran log ) ‘ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) )
4		logrncl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ran log )
5	4	fvresd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ↾ ran log ) ‘ ( log ‘ 𝐴 ) ) = ( exp ‘ ( log ‘ 𝐴 ) ) )
6		eldifsn	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
7		eff1o2	⊢ ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } )
8		f1ocnvfv2	⊢ ( ( ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( exp ↾ ran log ) ‘ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 )
9	7 8	mpan	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( ( exp ↾ ran log ) ‘ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 )
10	6 9	sylbir	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( ( exp ↾ ran log ) ‘ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 )
11	3 5 10	3eqtr3a	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( log ‘ 𝐴 ) ) = 𝐴 )