Metamath Proof Explorer

Theorem logbchbase

Description: Change of base for logarithms. Property in Cohen4 p. 367. (Contributed by AV, 11-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
2 logcl 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( log ` X ) e. CC )
3 1 2 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( log ` X ) e. CC )
4 3 3ad2ant3 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` X ) e. CC )
5 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
6 5 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) e. CC )
7 logccne0 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( log ` A ) =/= 0 )
8 6 7 jca 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( ( log ` A ) e. CC /\ ( log ` A ) =/= 0 ) )
9 8 3ad2ant1 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( ( log ` A ) e. CC /\ ( log ` A ) =/= 0 ) )
10 logcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
11 10 3adant3 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) e. CC )
12 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
13 11 12 jca 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) )
14 13 3ad2ant2 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) )
15 divcan7 
 |-  ( ( ( log ` X ) e. CC /\ ( ( log ` A ) e. CC /\ ( log ` A ) =/= 0 ) /\ ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) ) -> ( ( ( log ` X ) / ( log ` B ) ) / ( ( log ` A ) / ( log ` B ) ) ) = ( ( log ` X ) / ( log ` A ) ) )
16 4 9 14 15 syl3anc 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( ( ( log ` X ) / ( log ` B ) ) / ( ( log ` A ) / ( log ` B ) ) ) = ( ( log ` X ) / ( log ` A ) ) )
17 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
18 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
19 17 18 sylanbr 
 |-  ( ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
20 19 3adant1 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
21 17 biimpri 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) )
22 eldifsn 
 |-  ( A e. ( CC \ { 0 } ) <-> ( A e. CC /\ A =/= 0 ) )
23 22 biimpri 
 |-  ( ( A e. CC /\ A =/= 0 ) -> A e. ( CC \ { 0 } ) )
24 23 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> A e. ( CC \ { 0 } ) )
25 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ A e. ( CC \ { 0 } ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
26 21 24 25 syl2anr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
27 26 3adant3 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
28 20 27 oveq12d 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( ( B logb X ) / ( B logb A ) ) = ( ( ( log ` X ) / ( log ` B ) ) / ( ( log ` A ) / ( log ` B ) ) ) )
29 eldifpr 
 |-  ( A e. ( CC \ { 0 , 1 } ) <-> ( A e. CC /\ A =/= 0 /\ A =/= 1 ) )
30 logbval 
 |-  ( ( A e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( A logb X ) = ( ( log ` X ) / ( log ` A ) ) )
31 29 30 sylanbr 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( A logb X ) = ( ( log ` X ) / ( log ` A ) ) )
32 31 3adant2 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( A logb X ) = ( ( log ` X ) / ( log ` A ) ) )
33 16 28 32 3eqtr4rd 
 |-  ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( A logb X ) = ( ( B logb X ) / ( B logb A ) ) )