Metamath Proof Explorer

Theorem cxplogb

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

Ref Expression
Assertion cxplogb 
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb X ) ) = X )

Proof

Step Hyp Ref Expression
1 logbval 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
2 1 oveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb X ) ) = ( B ^c ( ( log ` X ) / ( log ` B ) ) ) )
3 eldifi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> B e. CC )
4 3 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> B e. CC )
5 eldif 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ -. B e. { 0 , 1 } ) )
6 c0ex 
 |-  0 e. _V
7 6 prid1 
 |-  0 e. { 0 , 1 }
8 eleq1 
 |-  ( B = 0 -> ( B e. { 0 , 1 } <-> 0 e. { 0 , 1 } ) )
9 7 8 mpbiri 
 |-  ( B = 0 -> B e. { 0 , 1 } )
10 9 necon3bi 
 |-  ( -. B e. { 0 , 1 } -> B =/= 0 )
11 10 adantl 
 |-  ( ( B e. CC /\ -. B e. { 0 , 1 } ) -> B =/= 0 )
12 5 11 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> B =/= 0 )
13 12 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> B =/= 0 )
14 eldif 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ -. X e. { 0 } ) )
15 6 snid 
 |-  0 e. { 0 }
16 eleq1 
 |-  ( X = 0 -> ( X e. { 0 } <-> 0 e. { 0 } ) )
17 15 16 mpbiri 
 |-  ( X = 0 -> X e. { 0 } )
18 17 necon3bi 
 |-  ( -. X e. { 0 } -> X =/= 0 )
19 18 anim2i 
 |-  ( ( X e. CC /\ -. X e. { 0 } ) -> ( X e. CC /\ X =/= 0 ) )
20 14 19 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( X e. CC /\ X =/= 0 ) )
21 logcl 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( log ` X ) e. CC )
22 20 21 syl 
 |-  ( X e. ( CC \ { 0 } ) -> ( log ` X ) e. CC )
23 22 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` X ) e. CC )
24 10 anim2i 
 |-  ( ( B e. CC /\ -. B e. { 0 , 1 } ) -> ( B e. CC /\ B =/= 0 ) )
25 5 24 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( B e. CC /\ B =/= 0 ) )
26 logcl 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( log ` B ) e. CC )
27 25 26 syl 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) e. CC )
28 27 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) e. CC )
29 eldifpr 
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
30 29 biimpi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
31 30 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
32 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
33 31 32 syl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 )
34 23 28 33 divcld 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( ( log ` X ) / ( log ` B ) ) e. CC )
35 4 13 34 cxpefd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( ( log ` X ) / ( log ` B ) ) ) = ( exp ` ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) ) )
36 eldifsn 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
37 36 21 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( log ` X ) e. CC )
38 37 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` X ) e. CC )
39 29 32 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) =/= 0 )
40 39 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 )
41 38 28 40 divcan1d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) = ( log ` X ) )
42 41 fveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( exp ` ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) ) = ( exp ` ( log ` X ) ) )
43 eflog 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( exp ` ( log ` X ) ) = X )
44 36 43 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( exp ` ( log ` X ) ) = X )
45 44 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( exp ` ( log ` X ) ) = X )
46 42 45 eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( exp ` ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) ) = X )
47 2 35 46 3eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb X ) ) = X )