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

Metamath Proof Explorer

Theorem relogbexp

Description: Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of Cohen4 p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by AV, 9-Jun-2020)

Ref Expression
Assertion relogbexp ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
2 1 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ℂ )
3 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
4 3 adantr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 0 )
5 simpr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ≠ 1 )
6 2 4 5 3jca ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
7 eldifpr ⊢ ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ↔ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
8 6 7 sylibr ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ) → 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) )
9 relogbzexp ⊢ ( ( 𝐵 ∈ ( ℂ ∖ { 0 , 1 } ) ∧ 𝐵 ∈ ℝ+ ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( 𝑀 · ( 𝐵 logb 𝐵 ) ) )
10 8 9 stoic4a ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = ( 𝑀 · ( 𝐵 logb 𝐵 ) ) )
11 6 3adant3 ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) )
12 logbid1 ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ∧ 𝐵 ≠ 1 ) → ( 𝐵 logb 𝐵 ) = 1 )
13 11 12 syl ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb 𝐵 ) = 1 )
14 13 oveq2d ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝑀 · ( 𝐵 logb 𝐵 ) ) = ( 𝑀 · 1 ) )
15 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
16 15 3ad2ant3 ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℂ )
17 16 mulridd ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝑀 · 1 ) = 𝑀 )
18 10 14 17 3eqtrd ⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )