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	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ e ) = 1 )
3	2	oveq2d	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( ( log ‘ 𝑦 ) / ( log ‘ e ) ) = ( ( log ‘ 𝑦 ) / 1 ) )
4		eldifsn	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
5		logcl	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( log ‘ 𝑦 ) ∈ ℂ )
6	4 5	sylbi	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( log ‘ 𝑦 ) ∈ ℂ )
7	6	div1d	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( ( log ‘ 𝑦 ) / 1 ) = ( log ‘ 𝑦 ) )
8	3 7	eqtrd	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → ( ( log ‘ 𝑦 ) / ( log ‘ e ) ) = ( log ‘ 𝑦 ) )
9	8	mpteq2ia	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ e ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) )
10		ere	⊢ e ∈ ℝ
11	10	recni	⊢ e ∈ ℂ
12		ene0	⊢ e ≠ 0
13		ene1	⊢ e ≠ 1
14		logbmpt	⊢ ( ( e ∈ ℂ ∧ e ≠ 0 ∧ e ≠ 1 ) → ( curry logb ‘ e ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ e ) ) ) )
15	11 12 13 14	mp3an	⊢ ( curry logb ‘ e ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ e ) ) )
16		logf1o	⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
17		f1ofn	⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log → log Fn ( ℂ ∖ { 0 } ) )
18	16 17	ax-mp	⊢ log Fn ( ℂ ∖ { 0 } )
19		dffn5	⊢ ( log Fn ( ℂ ∖ { 0 } ) ↔ log = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) ) )
20	18 19	mpbi	⊢ log = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( log ‘ 𝑦 ) )
21	9 15 20	3eqtr4i	⊢ ( curry logb ‘ e ) = log