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 
|- ( A e. ( CC \ { 0 } ) -> ( _e logb A ) = ( log ` A ) )

Proof

Step Hyp Ref Expression
1 ere 
 |-  _e e. RR
2 1 recni 
 |-  _e e. CC
3 ene0 
 |-  _e =/= 0
4 ene1 
 |-  _e =/= 1
5 eldifpr 
 |-  ( _e e. ( CC \ { 0 , 1 } ) <-> ( _e e. CC /\ _e =/= 0 /\ _e =/= 1 ) )
6 2 3 4 5 mpbir3an 
 |-  _e e. ( CC \ { 0 , 1 } )
7 logbval 
 |-  ( ( _e e. ( CC \ { 0 , 1 } ) /\ A e. ( CC \ { 0 } ) ) -> ( _e logb A ) = ( ( log ` A ) / ( log ` _e ) ) )
8 6 7 mpan 
 |-  ( A e. ( CC \ { 0 } ) -> ( _e logb A ) = ( ( log ` A ) / ( log ` _e ) ) )
9 loge 
 |-  ( log ` _e ) = 1
10 9 oveq2i 
 |-  ( ( log ` A ) / ( log ` _e ) ) = ( ( log ` A ) / 1 )
11 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
12 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
13 11 12 sylbi 
 |-  ( A e. ( CC \ { 0 } ) -> ( log ` A ) e. CC )
14 13 div1d 
 |-  ( A e. ( CC \ { 0 } ) -> ( ( log ` A ) / 1 ) = ( log ` A ) )
15 10 14 eqtrid 
 |-  ( A e. ( CC \ { 0 } ) -> ( ( log ` A ) / ( log ` _e ) ) = ( log ` A ) )
16 8 15 eqtrd 
 |-  ( A e. ( CC \ { 0 } ) -> ( _e logb A ) = ( log ` A ) )