This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )