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	syl5eq	|- ( A e. ( CC \ { 0 } ) -> ( ( log ` A ) / ( log ` _e ) ) = ( log ` A ) )
16	8 15	eqtrd	|- ( A e. ( CC \ { 0 } ) -> ( _e logb A ) = ( log ` A ) )