Metamath Proof Explorer

Theorem relogbcxp

Description: Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020)

Ref Expression
Assertion relogbcxp 
|- ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( B logb ( B ^c X ) ) = X )

Proof

Step Hyp Ref Expression
1 eldifsn 
 |-  ( B e. ( RR+ \ { 1 } ) <-> ( B e. RR+ /\ B =/= 1 ) )
2 rpcn 
 |-  ( B e. RR+ -> B e. CC )
3 2 adantr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B e. CC )
4 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
5 4 adantr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 0 )
6 simpr 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B =/= 1 )
7 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
8 3 5 6 7 syl3anbrc 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> B e. ( CC \ { 0 , 1 } ) )
9 1 8 sylbi 
 |-  ( B e. ( RR+ \ { 1 } ) -> B e. ( CC \ { 0 , 1 } ) )
10 eldifi 
 |-  ( B e. ( RR+ \ { 1 } ) -> B e. RR+ )
11 10 2 syl 
 |-  ( B e. ( RR+ \ { 1 } ) -> B e. CC )
12 recn 
 |-  ( X e. RR -> X e. CC )
13 cxpcl 
 |-  ( ( B e. CC /\ X e. CC ) -> ( B ^c X ) e. CC )
14 11 12 13 syl2an 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( B ^c X ) e. CC )
15 11 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> B e. CC )
16 1 5 sylbi 
 |-  ( B e. ( RR+ \ { 1 } ) -> B =/= 0 )
17 16 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> B =/= 0 )
18 12 adantl 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> X e. CC )
19 15 17 18 cxpne0d 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( B ^c X ) =/= 0 )
20 eldifsn 
 |-  ( ( B ^c X ) e. ( CC \ { 0 } ) <-> ( ( B ^c X ) e. CC /\ ( B ^c X ) =/= 0 ) )
21 14 19 20 sylanbrc 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( B ^c X ) e. ( CC \ { 0 } ) )
22 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( B ^c X ) e. ( CC \ { 0 } ) ) -> ( B logb ( B ^c X ) ) = ( ( log ` ( B ^c X ) ) / ( log ` B ) ) )
23 9 21 22 syl2an2r 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( B logb ( B ^c X ) ) = ( ( log ` ( B ^c X ) ) / ( log ` B ) ) )
24 logcxp 
 |-  ( ( B e. RR+ /\ X e. RR ) -> ( log ` ( B ^c X ) ) = ( X x. ( log ` B ) ) )
25 10 24 sylan 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( log ` ( B ^c X ) ) = ( X x. ( log ` B ) ) )
26 25 oveq1d 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( ( log ` ( B ^c X ) ) / ( log ` B ) ) = ( ( X x. ( log ` B ) ) / ( log ` B ) ) )
27 eldif 
 |-  ( B e. ( RR+ \ { 1 } ) <-> ( B e. RR+ /\ -. B e. { 1 } ) )
28 rpcnne0 
 |-  ( B e. RR+ -> ( B e. CC /\ B =/= 0 ) )
29 28 adantr 
 |-  ( ( B e. RR+ /\ -. B e. { 1 } ) -> ( B e. CC /\ B =/= 0 ) )
30 27 29 sylbi 
 |-  ( B e. ( RR+ \ { 1 } ) -> ( B e. CC /\ B =/= 0 ) )
31 logcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
32 30 31 syl 
 |-  ( B e. ( RR+ \ { 1 } ) -> ( log ` B ) e. CC )
33 32 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( log ` B ) e. CC )
34 logne0 
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
35 1 34 sylbi 
 |-  ( B e. ( RR+ \ { 1 } ) -> ( log ` B ) =/= 0 )
36 35 adantr 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( log ` B ) =/= 0 )
37 18 33 36 divcan4d 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( ( X x. ( log ` B ) ) / ( log ` B ) ) = X )
38 23 26 37 3eqtrd 
 |-  ( ( B e. ( RR+ \ { 1 } ) /\ X e. RR ) -> ( B logb ( B ^c X ) ) = X )