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