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 birani 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
31 logccne0 
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
32 30 31 syl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 )
33 23 28 32 divcld 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( ( log ` X ) / ( log ` B ) ) e. CC )
34 4 13 33 cxpefd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( ( log ` X ) / ( log ` B ) ) ) = ( exp ` ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) ) )
35 eldifsn 
 |-  ( X e. ( CC \ { 0 } ) <-> ( X e. CC /\ X =/= 0 ) )
36 35 21 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( log ` X ) e. CC )
37 36 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` X ) e. CC )
38 29 31 sylbi 
 |-  ( B e. ( CC \ { 0 , 1 } ) -> ( log ` B ) =/= 0 )
39 38 adantr 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( log ` B ) =/= 0 )
40 37 28 39 divcan1d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) = ( log ` X ) )
41 40 fveq2d 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( exp ` ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) ) = ( exp ` ( log ` X ) ) )
42 eflog 
 |-  ( ( X e. CC /\ X =/= 0 ) -> ( exp ` ( log ` X ) ) = X )
43 35 42 sylbi 
 |-  ( X e. ( CC \ { 0 } ) -> ( exp ` ( log ` X ) ) = X )
44 43 adantl 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( exp ` ( log ` X ) ) = X )
45 41 44 eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( exp ` ( ( ( log ` X ) / ( log ` B ) ) x. ( log ` B ) ) ) = X )
46 2 34 45 3eqtrd 
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B ^c ( B logb X ) ) = X )