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

Metamath Proof Explorer

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 ‘ 𝐴 ) ) = 𝐴 )