Metamath Proof Explorer

Theorem relogbmulexp

Description: The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR+ /\ C e. RR+ /\ E e. RR ) -> A e. RR+ )
2 rpcxpcl 
 |-  ( ( C e. RR+ /\ E e. RR ) -> ( C ^c E ) e. RR+ )
3 2 3adant1 
 |-  ( ( A e. RR+ /\ C e. RR+ /\ E e. RR ) -> ( C ^c E ) e. RR+ )
4 1 3 jca 
 |-  ( ( A e. RR+ /\ C e. RR+ /\ E e. RR ) -> ( A e. RR+ /\ ( C ^c E ) e. RR+ ) )
5 relogbmul 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ ( C ^c E ) e. RR+ ) ) -> ( B logb ( A x. ( C ^c E ) ) ) = ( ( B logb A ) + ( B logb ( C ^c E ) ) ) )
6 4 5 sylan2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ /\ E e. RR ) ) -> ( B logb ( A x. ( C ^c E ) ) ) = ( ( B logb A ) + ( B logb ( C ^c E ) ) ) )
7 relogbreexp 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( B logb ( C ^c E ) ) = ( E x. ( B logb C ) ) )
8 7 3adant3r1 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ /\ E e. RR ) ) -> ( B logb ( C ^c E ) ) = ( E x. ( B logb C ) ) )
9 8 oveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ /\ E e. RR ) ) -> ( ( B logb A ) + ( B logb ( C ^c E ) ) ) = ( ( B logb A ) + ( E x. ( B logb C ) ) ) )
10 6 9 eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ /\ E e. RR ) ) -> ( B logb ( A x. ( C ^c E ) ) ) = ( ( B logb A ) + ( E x. ( B logb C ) ) ) )