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

Metamath Proof Explorer

Theorem logblog

Description: The general logarithm to the base being Euler's constant regarded as function is the natural logarithm. (Contributed by AV, 12-Jun-2020)

Ref Expression
Assertion logblog 
|- ( curry logb ` _e ) = log

Proof

Step Hyp Ref Expression
1 loge 
 |-  ( log ` _e ) = 1
2 1 a1i 
 |-  ( y e. ( CC \ { 0 } ) -> ( log ` _e ) = 1 )
3 2 oveq2d 
 |-  ( y e. ( CC \ { 0 } ) -> ( ( log ` y ) / ( log ` _e ) ) = ( ( log ` y ) / 1 ) )
4 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
5 logcl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( log ` y ) e. CC )
6 4 5 sylbi 
 |-  ( y e. ( CC \ { 0 } ) -> ( log ` y ) e. CC )
7 6 div1d 
 |-  ( y e. ( CC \ { 0 } ) -> ( ( log ` y ) / 1 ) = ( log ` y ) )
8 3 7 eqtrd 
 |-  ( y e. ( CC \ { 0 } ) -> ( ( log ` y ) / ( log ` _e ) ) = ( log ` y ) )
9 8 mpteq2ia 
 |-  ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` _e ) ) ) = ( y e. ( CC \ { 0 } ) |-> ( log ` y ) )
10 ere 
 |-  _e e. RR
11 10 recni 
 |-  _e e. CC
12 ene0 
 |-  _e =/= 0
13 ene1 
 |-  _e =/= 1
14 logbmpt 
 |-  ( ( _e e. CC /\ _e =/= 0 /\ _e =/= 1 ) -> ( curry logb ` _e ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` _e ) ) ) )
15 11 12 13 14 mp3an 
 |-  ( curry logb ` _e ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` _e ) ) )
16 logf1o 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log
17 f1ofn 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log -> log Fn ( CC \ { 0 } ) )
18 16 17 ax-mp 
 |-  log Fn ( CC \ { 0 } )
19 dffn5 
 |-  ( log Fn ( CC \ { 0 } ) <-> log = ( y e. ( CC \ { 0 } ) |-> ( log ` y ) ) )
20 18 19 mpbi 
 |-  log = ( y e. ( CC \ { 0 } ) |-> ( log ` y ) )
21 9 15 20 3eqtr4i 
 |-  ( curry logb ` _e ) = log