Metamath Proof Explorer

Theorem relogbreexp

Description: Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of Cohen4 p. 361. (Contributed by AV, 9-Jun-2020)

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

Proof

Step Hyp Ref Expression
1 logcxp 
 |-  ( ( C e. RR+ /\ E e. RR ) -> ( log ` ( C ^c E ) ) = ( E x. ( log ` C ) ) )
2 1 3adant1 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( log ` ( C ^c E ) ) = ( E x. ( log ` C ) ) )
3 2 oveq1d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( ( log ` ( C ^c E ) ) / ( log ` B ) ) = ( ( E x. ( log ` C ) ) / ( log ` B ) ) )
4 recn 
 |-  ( E e. RR -> E e. CC )
5 4 3ad2ant3 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> E e. CC )
6 rpcn 
 |-  ( C e. RR+ -> C e. CC )
7 rpne0 
 |-  ( C e. RR+ -> C =/= 0 )
8 6 7 logcld 
 |-  ( C e. RR+ -> ( log ` C ) e. CC )
9 8 3ad2ant2 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( log ` C ) e. CC )
10 eldifi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> B e. CC )
11 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
12 11 simp2bi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> B =/= 0 )
13 10 12 logcld 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) e. CC )
14 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
15 11 14 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) =/= 0 )
16 13 15 jca 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) )
17 16 3ad2ant1 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) )
18 divass 
 |-  ( ( E e. CC /\ ( log ` C ) e. CC /\ ( ( log ` B ) e. CC /\ ( log ` B ) =/= 0 ) ) -> ( ( E x. ( log ` C ) ) / ( log ` B ) ) = ( E x. ( ( log ` C ) / ( log ` B ) ) ) )
19 5 9 17 18 syl3anc 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( ( E x. ( log ` C ) ) / ( log ` B ) ) = ( E x. ( ( log ` C ) / ( log ` B ) ) ) )
20 3 19 eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( ( log ` ( C ^c E ) ) / ( log ` B ) ) = ( E x. ( ( log ` C ) / ( log ` B ) ) ) )
21 simp1 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> B e. ( CC \ { 0 , 1 } ) )
22 6 adantr 
 |-  ( ( C e. RR+ /\ E e. RR ) -> C e. CC )
23 4 adantl 
 |-  ( ( C e. RR+ /\ E e. RR ) -> E e. CC )
24 22 23 cxpcld 
 |-  ( ( C e. RR+ /\ E e. RR ) -> ( C ^c E ) e. CC )
25 7 adantr 
 |-  ( ( C e. RR+ /\ E e. RR ) -> C =/= 0 )
26 22 25 23 cxpne0d 
 |-  ( ( C e. RR+ /\ E e. RR ) -> ( C ^c E ) =/= 0 )
27 eldifsn 
 |-  ( ( C ^c E ) e. ( CC \ { 0 } ) <-> ( ( C ^c E ) e. CC /\ ( C ^c E ) =/= 0 ) )
28 24 26 27 sylanbrc 
 |-  ( ( C e. RR+ /\ E e. RR ) -> ( C ^c E ) e. ( CC \ { 0 } ) )
29 28 3adant1 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( C ^c E ) e. ( CC \ { 0 } ) )
30 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( C ^c E ) e. ( CC \ { 0 } ) ) -> ( B logb ( C ^c E ) ) = ( ( log ` ( C ^c E ) ) / ( log ` B ) ) )
31 21 29 30 syl2anc 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( B logb ( C ^c E ) ) = ( ( log ` ( C ^c E ) ) / ( log ` B ) ) )
32 rpcndif0 
 |-  ( C e. RR+ -> C e. ( CC \ { 0 } ) )
33 32 anim2i 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ ) -> ( B e. ( CC \ { 0 , 1 } ) /\ C e. ( CC \ { 0 } ) ) )
34 33 3adant3 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( B e. ( CC \ { 0 , 1 } ) /\ C e. ( CC \ { 0 } ) ) )
35 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. ( CC \ { 0 } ) ) -> ( B logb C ) = ( ( log ` C ) / ( log ` B ) ) )
36 34 35 syl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( B logb C ) = ( ( log ` C ) / ( log ` B ) ) )
37 36 oveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( E x. ( B logb C ) ) = ( E x. ( ( log ` C ) / ( log ` B ) ) ) )
38 20 31 37 3eqtr4d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( B logb ( C ^c E ) ) = ( E x. ( B logb C ) ) )