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 ) ) ) )