Metamath Proof Explorer

Theorem relogbmulbexp

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

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

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( B e. RR+ -> B e. CC )
2 1 adantr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B e. CC )
3 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
4 3 adantr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 0 )
5 simpr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 1 )
6 2 4 5 3jca 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
7 eldifsn 
 |-  ( B e. ( RR+ \ { 1 } ) <-> ( B e. RR+ /\ B =/= 1 ) )
8 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
9 6 7 8 3imtr4i 
 |-  ( B e. ( RR+ \ { 1 } ) -> B e. ( CC \ { 0 , 1 } ) )
10 9 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> B e. ( CC \ { 0 , 1 } ) )
11 simprl 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> A e. RR+ )
12 eldifi 
 |-  ( B e. ( RR+ \ { 1 } ) -> B e. RR+ )
13 12 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> B e. RR+ )
14 simpr 
 |-  ( ( A e. RR+ /\ C e. RR ) -> C e. RR )
15 14 adantl 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> C e. RR )
16 relogbmulexp 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ B e. RR+ /\ C e. RR ) ) -> ( B logb ( A x. ( B ^c C ) ) ) = ( ( B logb A ) + ( C x. ( B logb B ) ) ) )
17 10 11 13 15 16 syl13anc 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( B logb ( A x. ( B ^c C ) ) ) = ( ( B logb A ) + ( C x. ( B logb B ) ) ) )
18 7 6 sylbi 
 |-  ( B e. ( RR+ \ { 1 } ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
19 logbid1 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb B ) = 1 )
20 18 19 syl 
 |-  ( B e. ( RR+ \ { 1 } ) -> ( B logb B ) = 1 )
21 20 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( B logb B ) = 1 )
22 21 oveq2d 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( C x. ( B logb B ) ) = ( C x. 1 ) )
23 ax-1rid 
 |-  ( C e. RR -> ( C x. 1 ) = C )
24 23 adantl 
 |-  ( ( A e. RR+ /\ C e. RR ) -> ( C x. 1 ) = C )
25 24 adantl 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( C x. 1 ) = C )
26 22 25 eqtrd 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( C x. ( B logb B ) ) = C )
27 26 oveq2d 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( ( B logb A ) + ( C x. ( B logb B ) ) ) = ( ( B logb A ) + C ) )
28 17 27 eqtrd 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( B logb ( A x. ( B ^c C ) ) ) = ( ( B logb A ) + C ) )