Theorem logef

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

	Ref	Expression
Assertion	logef	⊢ ( 𝐴 ∈ ran log → ( log ‘ ( exp ‘ 𝐴 ) ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dflog2	⊢ log = ◡ ( exp ↾ ran log )
2	1	fveq1i	⊢ ( log ‘ ( ( exp ↾ ran log ) ‘ 𝐴 ) ) = ( ◡ ( exp ↾ ran log ) ‘ ( ( exp ↾ ran log ) ‘ 𝐴 ) )
3		fvres	⊢ ( 𝐴 ∈ ran log → ( ( exp ↾ ran log ) ‘ 𝐴 ) = ( exp ‘ 𝐴 ) )
4	3	fveq2d	⊢ ( 𝐴 ∈ ran log → ( log ‘ ( ( exp ↾ ran log ) ‘ 𝐴 ) ) = ( log ‘ ( exp ‘ 𝐴 ) ) )
5		eff1o2	⊢ ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } )
6		f1ocnvfv1	⊢ ( ( ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } ) ∧ 𝐴 ∈ ran log ) → ( ◡ ( exp ↾ ran log ) ‘ ( ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 )
7	5 6	mpan	⊢ ( 𝐴 ∈ ran log → ( ◡ ( exp ↾ ran log ) ‘ ( ( exp ↾ ran log ) ‘ 𝐴 ) ) = 𝐴 )
8	2 4 7	3eqtr3a	⊢ ( 𝐴 ∈ ran log → ( log ‘ ( exp ‘ 𝐴 ) ) = 𝐴 )