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 ) ) ) )