Metamath Proof Explorer

Theorem logbf

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

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

Proof

Step Hyp Ref Expression
1 logbmpt 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) = ( y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` B ) ) ) )
2 eldifsn 
 |-  ( y e. ( CC \ { 0 } ) <-> ( y e. CC /\ y =/= 0 ) )
3 logcl 
 |-  ( ( y e. CC /\ y =/= 0 ) -> ( log ` y ) e. CC )
4 2 3 sylbi 
 |-  ( y e. ( CC \ { 0 } ) -> ( log ` y ) e. CC )
5 4 adantl 
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ y e. ( CC \ { 0 } ) ) -> ( log ` y ) e. CC )
6 logcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
7 6 3adant3 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) e. CC )
8 7 adantr 
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ y e. ( CC \ { 0 } ) ) -> ( log ` B ) e. CC )
9 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
10 9 adantr 
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ y e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 )
11 5 8 10 divcld 
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ y e. ( CC \ { 0 } ) ) -> ( ( log ` y ) / ( log ` B ) ) e. CC )
12 1 11 fmpt3d 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( curry logb ` B ) : ( CC \ { 0 } ) --> CC )