Metamath Proof Explorer

Theorem relogbmul

Description: The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 29-May-2020)

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

Proof

Step Hyp Ref Expression
1 relogmul 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( log ` ( A x. C ) ) = ( ( log ` A ) + ( log ` C ) ) )
2 1 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( log ` ( A x. C ) ) = ( ( log ` A ) + ( log ` C ) ) )
3 2 oveq1d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( log ` ( A x. C ) ) / ( log ` B ) ) = ( ( ( log ` A ) + ( log ` C ) ) / ( log ` B ) ) )
4 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
5 4 recnd 
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
6 5 adantr 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( log ` A ) e. CC )
7 relogcl 
 |-  ( C e. RR+ -> ( log ` C ) e. RR )
8 7 recnd 
 |-  ( C e. RR+ -> ( log ` C ) e. CC )
9 8 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( log ` C ) e. CC )
10 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
11 3simpa 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 ) )
12 10 11 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( B e. CC /\ B =/= 0 ) )
13 logcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
14 12 13 syl 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) e. CC )
15 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
16 10 15 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) =/= 0 )
17 14 16 jca 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) )
18 17 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) )
19 divdir 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` C ) e. CC /\ ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) ) -> ( ( ( log ` A ) + ( log ` C ) ) / ( log ` B ) ) = ( ( ( log ` A ) / ( log ` B ) ) + ( ( log ` C ) / ( log ` B ) ) ) )
20 6 9 18 19 syl2an23an 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( ( log ` A ) + ( log ` C ) ) / ( log ` B ) ) = ( ( ( log ` A ) / ( log ` B ) ) + ( ( log ` C ) / ( log ` B ) ) ) )
21 3 20 eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( log ` ( A x. C ) ) / ( log ` B ) ) = ( ( ( log ` A ) / ( log ` B ) ) + ( ( log ` C ) / ( log ` B ) ) ) )
22 rpcn 
 |-  ( A e. RR+ -> A e. CC )
23 rpcn 
 |-  ( C e. RR+ -> C e. CC )
24 mulcl 
 |-  ( ( A e. CC /\ C e. CC ) -> ( A x. C ) e. CC )
25 22 23 24 syl2an 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A x. C ) e. CC )
26 22 adantr 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> A e. CC )
27 23 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> C e. CC )
28 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
29 28 adantr 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> A =/= 0 )
30 rpne0 
 |-  ( C e. RR+ -> C =/= 0 )
31 30 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> C =/= 0 )
32 26 27 29 31 mulne0d 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A x. C ) =/= 0 )
33 eldifsn 
 |-  ( ( A x. C ) e. ( CC \ { 0 } ) <-> ( ( A x. C ) e. CC /\ ( A x. C ) =/= 0 ) )
34 25 32 33 sylanbrc 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> ( A x. C ) e. ( CC \ { 0 } ) )
35 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A x. C ) e. ( CC \ { 0 } ) ) -> ( B logb ( A x. C ) ) = ( ( log ` ( A x. C ) ) / ( log ` B ) ) )
36 34 35 sylan2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A x. C ) ) = ( ( log ` ( A x. C ) ) / ( log ` B ) ) )
37 rpcndif0 
 |-  ( A e. RR+ -> A e. ( CC \ { 0 } ) )
38 37 adantr 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> A e. ( CC \ { 0 } ) )
39 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ A e. ( CC \ { 0 } ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
40 38 39 sylan2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb A ) = ( ( log ` A ) / ( log ` B ) ) )
41 rpcndif0 
 |-  ( C e. RR+ -> C e. ( CC \ { 0 } ) )
42 41 adantl 
 |-  ( ( A e. RR+ /\ C e. RR+ ) -> C e. ( CC \ { 0 } ) )
43 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. ( CC \ { 0 } ) ) -> ( B logb C ) = ( ( log ` C ) / ( log ` B ) ) )
44 42 43 sylan2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb C ) = ( ( log ` C ) / ( log ` B ) ) )
45 40 44 oveq12d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( ( B logb A ) + ( B logb C ) ) = ( ( ( log ` A ) / ( log ` B ) ) + ( ( log ` C ) / ( log ` B ) ) ) )
46 21 36 45 3eqtr4d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A x. C ) ) = ( ( B logb A ) + ( B logb C ) ) )