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 )