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

Metamath Proof Explorer

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