Theorem elogb

Description: The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using _e as the base in logb is the same as log . Definition in Cohen4 p. 352. (Contributed by David A. Wheeler, 17-Oct-2017) (Revised by David A. Wheeler and AV, 16-Jun-2020)

	Ref	Expression
Assertion	elogb	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( e logb 𝐴 ) = ( log ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ere	⊢ e ∈ ℝ
2	1	recni	⊢ e ∈ ℂ
3		ene0	⊢ e ≠ 0
4		ene1	⊢ e ≠ 1
5		eldifpr	⊢ ( e ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( e ∈ ℂ ∧ e ≠ 0 ∧ e ≠ 1 ) )
6	2 3 4 5	mpbir3an	⊢ e ∈ ( ℂ ∖ { 0 , 1 } )
7		logbval	⊢ ( ( e ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐴 ∈ ( ℂ ∖ { 0 } ) ) → ( e logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ e ) ) )
8	6 7	mpan	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( e logb 𝐴 ) = ( ( log ‘ 𝐴 ) / ( log ‘ e ) ) )
9		loge	⊢ ( log ‘ e ) = 1
10	9	oveq2i	⊢ ( ( log ‘ 𝐴 ) / ( log ‘ e ) ) = ( ( log ‘ 𝐴 ) / 1 )
11		eldifsn	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
12		logcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℂ )
13	11 12	sylbi	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝐴 ) ∈ ℂ )
14	13	div1d	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( ( log ‘ 𝐴 ) / 1 ) = ( log ‘ 𝐴 ) )
15	10 14	syl5eq	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( ( log ‘ 𝐴 ) / ( log ‘ e ) ) = ( log ‘ 𝐴 ) )
16	8 15	eqtrd	⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( e logb 𝐴 ) = ( log ‘ 𝐴 ) )