Metamath Proof Explorer

Theorem relogbdiv

Description: The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of Cohen4 p. 361. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion relogbdiv 
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A / C ) ) = ( ( B logb A ) - ( B logb C ) ) )

Proof

Step Hyp Ref Expression
1 neg1rr 
 |-  -u 1 e. RR
2 relogbmulexp 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ /\ -u 1 e. RR ) ) -> ( B logb ( A x. ( C ^c -u 1 ) ) ) = ( ( B logb A ) + ( -u 1 x. ( B logb C ) ) ) )
3 1 2 mp3anr3 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A x. ( C ^c -u 1 ) ) ) = ( ( B logb A ) + ( -u 1 x. ( B logb C ) ) ) )
4 rpcn 
 |-  ( A e. RR+ -> A e. CC )
5 4 adantr 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> A e. CC )
6 rpcn 
 |-  ( C e. RR+ -> C e. CC )
7 6 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> C e. CC )
8 rpne0 
 |-  ( C e. RR+ -> C =/= 0 )
9 8 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> C =/= 0 )
10 5 7 9 divrecd 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A / C ) = ( A x. ( 1 / C ) ) )
11 1cnd 
 |-  ( C e. RR+ -> 1 e. CC )
12 6 8 11 cxpnegd 
 |-  ( C e. RR+ -> ( C ^c -u 1 ) = ( 1 / ( C ^c 1 ) ) )
13 6 cxp1d 
 |-  ( C e. RR+ -> ( C ^c 1 ) = C )
14 13 oveq2d 
 |-  ( C e. RR+ -> ( 1 / ( C ^c 1 ) ) = ( 1 / C ) )
15 12 14 eqtrd 
 |-  ( C e. RR+ -> ( C ^c -u 1 ) = ( 1 / C ) )
16 15 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( C ^c -u 1 ) = ( 1 / C ) )
17 16 oveq2d 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A x. ( C ^c -u 1 ) ) = ( A x. ( 1 / C ) ) )
18 10 17 eqtr4d 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A / C ) = ( A x. ( C ^c -u 1 ) ) )
19 18 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( A / C ) = ( A x. ( C ^c -u 1 ) ) )
20 19 oveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A / C ) ) = ( B logb ( A x. ( C ^c -u 1 ) ) ) )
21 rpcndif0 
 |-  ( C e. RR+ -> C e. ( CC \ { 0 } ) )
22 21 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> C e. ( CC \ { 0 } ) )
23 logbcl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. ( CC \ { 0 } ) ) -> ( B logb C ) e. CC )
24 22 23 sylan2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb C ) e. CC )
25 mulm1 
 |-  ( ( B logb C ) e. CC -> ( -u 1 x. ( B logb C ) ) = -u ( B logb C ) )
26 25 oveq2d 
 |-  ( ( B logb C ) e. CC -> ( ( B logb A ) + ( -u 1 x. ( B logb C ) ) ) = ( ( B logb A ) + -u ( B logb C ) ) )
27 24 26 syl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( B logb A ) + ( -u 1 x. ( B logb C ) ) ) = ( ( B logb A ) + -u ( B logb C ) ) )
28 rpcndif0 
 |-  ( A e. RR+ -> A e. ( CC \ { 0 } ) )
29 28 adantr 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> A e. ( CC \ { 0 } ) )
30 logbcl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ A e. ( CC \ { 0 } ) ) -> ( B logb A ) e. CC )
31 29 30 sylan2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb A ) e. CC )
32 31 24 negsubd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( B logb A ) + -u ( B logb C ) ) = ( ( B logb A ) - ( B logb C ) ) )
33 27 32 eqtr2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( B logb A ) - ( B logb C ) ) = ( ( B logb A ) + ( -u 1 x. ( B logb C ) ) ) )
34 3 20 33 3eqtr4d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A / C ) ) = ( ( B logb A ) - ( B logb C ) ) )