Metamath Proof Explorer


Theorem nnlogbexp

Description: Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

Ref Expression
Assertion nnlogbexp
|- ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )

Proof

Step Hyp Ref Expression
1 zgt1rpn0n1
 |-  ( B e. ( ZZ>= ` 2 ) -> ( B e. RR+ /\ B =/= 0 /\ B =/= 1 ) )
2 1 adantr
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( B e. RR+ /\ B =/= 0 /\ B =/= 1 ) )
3 2 simp1d
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> B e. RR+ )
4 3 rpcnd
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> B e. CC )
5 4 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> B e. CC )
6 2 simp2d
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> B =/= 0 )
7 6 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> B =/= 0 )
8 2 simp3d
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> B =/= 1 )
9 8 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> B =/= 1 )
10 logb1
 |-  ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb 1 ) = 0 )
11 5 7 9 10 syl3anc
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> ( B logb 1 ) = 0 )
12 simpr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> M = 0 )
13 12 oveq2d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> ( B ^ M ) = ( B ^ 0 ) )
14 5 exp0d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> ( B ^ 0 ) = 1 )
15 13 14 eqtrd
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> ( B ^ M ) = 1 )
16 15 oveq2d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> ( B logb ( B ^ M ) ) = ( B logb 1 ) )
17 11 16 12 3eqtr4d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M = 0 ) -> ( B logb ( B ^ M ) ) = M )
18 4 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> B e. CC )
19 6 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> B =/= 0 )
20 8 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> B =/= 1 )
21 eldifpr
 |-  ( B e. ( CC \ { 0 , 1 } ) <-> ( B e. CC /\ B =/= 0 /\ B =/= 1 ) )
22 18 19 20 21 syl3anbrc
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> B e. ( CC \ { 0 , 1 } ) )
23 3 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> B e. RR+ )
24 simpr
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> M e. ZZ )
25 24 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> M e. ZZ )
26 23 25 rpexpcld
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( B ^ M ) e. RR+ )
27 26 rpcnne0d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( ( B ^ M ) e. CC /\ ( B ^ M ) =/= 0 ) )
28 eldifsn
 |-  ( ( B ^ M ) e. ( CC \ { 0 } ) <-> ( ( B ^ M ) e. CC /\ ( B ^ M ) =/= 0 ) )
29 27 28 sylibr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( B ^ M ) e. ( CC \ { 0 } ) )
30 logbval
 |-  ( ( B e. ( CC \ { 0 , 1 } ) /\ ( B ^ M ) e. ( CC \ { 0 } ) ) -> ( B logb ( B ^ M ) ) = ( ( log ` ( B ^ M ) ) / ( log ` B ) ) )
31 22 29 30 syl2anc
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( B logb ( B ^ M ) ) = ( ( log ` ( B ^ M ) ) / ( log ` B ) ) )
32 24 zred
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> M e. RR )
33 32 adantr
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> M e. RR )
34 23 33 logcxpd
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( log ` ( B ^c M ) ) = ( M x. ( log ` B ) ) )
35 18 19 25 cxpexpzd
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( B ^c M ) = ( B ^ M ) )
36 35 fveq2d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( log ` ( B ^c M ) ) = ( log ` ( B ^ M ) ) )
37 34 36 eqtr3d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( M x. ( log ` B ) ) = ( log ` ( B ^ M ) ) )
38 37 oveq1d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( ( M x. ( log ` B ) ) / ( log ` B ) ) = ( ( log ` ( B ^ M ) ) / ( log ` B ) ) )
39 33 recnd
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> M e. CC )
40 18 19 logcld
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( log ` B ) e. CC )
41 logne0
 |-  ( ( B e. RR+ /\ B =/= 1 ) -> ( log ` B ) =/= 0 )
42 23 20 41 syl2anc
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( log ` B ) =/= 0 )
43 39 40 42 divcan4d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( ( M x. ( log ` B ) ) / ( log ` B ) ) = M )
44 31 38 43 3eqtr2d
 |-  ( ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) /\ M =/= 0 ) -> ( B logb ( B ^ M ) ) = M )
45 17 44 pm2.61dane
 |-  ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )