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 ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 zgt1rpn0n1 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
2 1 adantr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
3 2 simp1d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ∈ ℝ+ )
4 3 rpcnd ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ∈ ℂ )
5 4 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝐵 ∈ ℂ )
6 2 simp2d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ≠ 0 )
7 6 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝐵 ≠ 0 )
8 2 simp3d ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝐵 ≠ 1 )
9 8 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝐵 ≠ 1 )
10 logb1 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 1 ) = 0 )
11 5 7 9 10 syl3anc ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 logb 1 ) = 0 )
12 simpr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → 𝑀 = 0 )
13 12 oveq2d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 ↑ 𝑀 ) = ( 𝐵 ↑ 0 ) )
14 5 exp0d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 ↑ 0 ) = 1 )
15 13 14 eqtrd ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 ↑ 𝑀 ) = 1 )
16 15 oveq2d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( 𝐵 logb 1 ) )
17 11 16 12 3eqtr4d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 = 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )
18 4 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ∈ ℂ )
19 6 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ≠ 0 )
20 8 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ≠ 1 )
21 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
22 18 19 20 21 syl3anbrc ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
23 3 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝐵 ∈ ℝ+ )
24 simpr ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
25 24 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℤ )
26 23 25 rpexpcld ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 ↑ 𝑀 ) ∈ ℝ+ )
27 26 rpcnne0d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( ( 𝐵 ↑ 𝑀 ) ∈ ℂ ∧ ( 𝐵 ↑ 𝑀 ) ≠ 0 ) )
28 eldifsn ⊢ ( ( 𝐵 ↑ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝐵 ↑ 𝑀 ) ∈ ℂ ∧ ( 𝐵 ↑ 𝑀 ) ≠ 0 ) )
29 27 28 sylibr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 ↑ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) )
30 logbval ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ ( 𝐵 ↑ 𝑀 ) ∈ ( ℂ ∖ { 0 } ) ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( ( log ‘ ( 𝐵 ↑ 𝑀 ) ) / ( log ‘ 𝐵 ) ) )
31 22 29 30 syl2anc ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( ( log ‘ ( 𝐵 ↑ 𝑀 ) ) / ( log ‘ 𝐵 ) ) )
32 24 zred ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℝ )
33 32 adantr ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℝ )
34 23 33 logcxpd ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ ( 𝐵 ↑𝑐 𝑀 ) ) = ( 𝑀 · ( log ‘ 𝐵 ) ) )
35 18 19 25 cxpexpzd ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 ↑𝑐 𝑀 ) = ( 𝐵 ↑ 𝑀 ) )
36 35 fveq2d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ ( 𝐵 ↑𝑐 𝑀 ) ) = ( log ‘ ( 𝐵 ↑ 𝑀 ) ) )
37 34 36 eqtr3d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝑀 · ( log ‘ 𝐵 ) ) = ( log ‘ ( 𝐵 ↑ 𝑀 ) ) )
38 37 oveq1d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( ( 𝑀 · ( log ‘ 𝐵 ) ) / ( log ‘ 𝐵 ) ) = ( ( log ‘ ( 𝐵 ↑ 𝑀 ) ) / ( log ‘ 𝐵 ) ) )
39 33 recnd ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → 𝑀 ∈ ℂ )
40 18 19 logcld ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ 𝐵 ) ∈ ℂ )
41 logne0 ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( log ‘ 𝐵 ) ≠ 0 )
42 23 20 41 syl2anc ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( log ‘ 𝐵 ) ≠ 0 )
43 39 40 42 divcan4d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( ( 𝑀 · ( log ‘ 𝐵 ) ) / ( log ‘ 𝐵 ) ) = 𝑀 )
44 31 38 43 3eqtr2d ⊢ ( ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑀 ≠ 0 ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )
45 17 44 pm2.61dane ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )