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