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 ⊢ ( 𝑦 ∈ ( ℂ ∖ { 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