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 ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )