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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( ( log ‘ 𝐴 ) / ( log ‘ e ) ) = ( log ‘ 𝐴 ) )
16 8 15 eqtrd ⊢ ( 𝐴 ∈ ( ℂ ∖ { 0 } ) → ( e logb 𝐴 ) = ( log ‘ 𝐴 ) )