Metamath Proof Explorer

Theorem logbcl

Description: General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017)

Ref Expression
Assertion logbcl 
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) e. CC )

Proof

Step Hyp Ref Expression
1 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
2 eldifsn 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
3 logcl 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( log ` X ) e. CC )
4 2 3 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( log ` X ) e. CC )
5 4 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` X ) e. CC )
6 eldifi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> B e. CC )
7 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
8 7 simp2bi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> B =/= 0 )
9 6 8 logcld 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) e. CC )
10 9 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) e. CC )
11 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
12 7 11 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) =/= 0 )
13 12 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 )
14 5 10 13 divcld 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( ( log ` X ) / ( log ` B ) ) e. CC )
15 1 14 eqeltrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) e. CC )