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