Metamath Proof Explorer


Theorem logbmpt

Description: The general logarithm to a fixed base regarded as mapping. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion logbmpt
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 df-logb
 |-  logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
2 ovexd
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ ( x e. ( CC \ { 0 , 1 } ) /\ y e. ( CC \ { 0 } ) ) ) -> ( ( log ` y ) / ( log ` x ) ) e. _V )
3 2 ralrimivva
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> A. x e. ( CC \ { 0 , 1 } ) A. y e. ( CC \ { 0 } ) ( ( log ` y ) / ( log ` x ) ) e. _V )
4 ax-1cn
 |-  1 e. CC
5 ax-1ne0
 |-  1 =/= 0
6 elsng
 |-  ( 1 e. CC -> ( 1 e. { 0 } <-> 1 = 0 ) )
7 4 6 ax-mp
 |-  ( 1 e. { 0 } <-> 1 = 0 )
8 5 7 nemtbir
 |-  -. 1 e. { 0 }
9 eldif
 |-  ( 1 e. ( CC \ { 0 } ) <-> ( 1 e. CC /\ -. 1 e. { 0 } ) )
10 4 8 9 mpbir2an
 |-  1 e. ( CC \ { 0 } )
11 10 ne0ii
 |-  ( CC \ { 0 } ) =/= (/)
12 11 a1i
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( CC \ { 0 } ) =/= (/) )
13 cnex
 |-  CC e. _V
14 13 difexi
 |-  ( CC \ { 0 } ) e. _V
15 14 a1i
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( CC \ { 0 } ) e. _V )
16 eldifpr
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
17 16 biimpri
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) )
18 1 3 12 15 17 mpocurryvald
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( y e. ( CC \ { 0 } ) |-> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) ) )
19 csbov2g
 |-  ( B e. CC -> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / [_ B / x ]_ ( log ` x ) ) )
20 csbfv
 |-  [_ B / x ]_ ( log ` x ) = ( log ` B )
21 20 a1i
 |-  ( B e. CC -> [_ B / x ]_ ( log ` x ) = ( log ` B ) )
22 21 oveq2d
 |-  ( B e. CC -> ( ( log ` y ) / [_ B / x ]_ ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) )
23 19 22 eqtrd
 |-  ( B e. CC -> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) )
24 23 3ad2ant1
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) = ( ( log ` y ) / ( log ` B ) ) )
25 24 mpteq2dv
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( y e. ( CC \ { 0 } ) |-> [_ B / x ]_ ( ( log ` y ) / ( log ` x ) ) ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` B ) ) ) )
26 18 25 eqtrd
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` B ) ) ) )