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 ) |