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

Metamath Proof Explorer

Theorem logeftb

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

Ref Expression
Assertion logeftb ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log ) → ( ( log ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ 𝐵 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
2 dflog2 ⊢ log = ◡ ( exp ↾ ran log )
3 2 fveq1i ⊢ ( log ‘ 𝐴 ) = ( ◡ ( exp ↾ ran log ) ‘ 𝐴 )
4 3 eqeq1i ⊢ ( ( log ‘ 𝐴 ) = 𝐵 ↔ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) = 𝐵 )
5 fvres ⊢ ( 𝐵 ∈ ran log → ( ( exp ↾ ran log ) ‘ 𝐵 ) = ( exp ‘ 𝐵 ) )
6 5 eqeq1d ⊢ ( 𝐵 ∈ ran log → ( ( ( exp ↾ ran log ) ‘ 𝐵 ) = 𝐴 ↔ ( exp ‘ 𝐵 ) = 𝐴 ) )
7 6 adantr ⊢ ( ( 𝐵 ∈ ran log ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( exp ↾ ran log ) ‘ 𝐵 ) = 𝐴 ↔ ( exp ‘ 𝐵 ) = 𝐴 ) )
8 eff1o2 ⊢ ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } )
9 f1ocnvfvb ⊢ ( ( ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ran log ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( exp ↾ ran log ) ‘ 𝐵 ) = 𝐴 ↔ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) = 𝐵 ) )
10 8 9 mp3an1 ⊢ ( ( 𝐵 ∈ ran log ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( exp ↾ ran log ) ‘ 𝐵 ) = 𝐴 ↔ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) = 𝐵 ) )
11 7 10 bitr3d ⊢ ( ( 𝐵 ∈ ran log ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( ( exp ‘ 𝐵 ) = 𝐴 ↔ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) = 𝐵 ) )
12 11 ancoms ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ran log ) → ( ( exp ‘ 𝐵 ) = 𝐴 ↔ ( ◡ ( exp ↾ ran log ) ‘ 𝐴 ) = 𝐵 ) )
13 4 12 bitr4id ⊢ ( ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ∧ 𝐵 ∈ ran log ) → ( ( log ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ 𝐵 ) = 𝐴 ) )
14 1 13 sylanbr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ran log ) → ( ( log ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ 𝐵 ) = 𝐴 ) )
15 14 3impa ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ran log ) → ( ( log ‘ 𝐴 ) = 𝐵 ↔ ( exp ‘ 𝐵 ) = 𝐴 ) )