Theorem relogbexpd

Description: Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024)

	Ref	Expression
Hypotheses	relogbexpd.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	relogbexpd.2	⊢ ( 𝜑 → 𝐵 ≠ 1 )
	relogbexpd.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
Assertion	relogbexpd	⊢ ( 𝜑 → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		relogbexpd.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
2		relogbexpd.2	⊢ ( 𝜑 → 𝐵 ≠ 1 )
3		relogbexpd.3	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4	1 2 3	3jca	⊢ ( 𝜑 → ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) )
5		relogbexp	⊢ ( ( 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1 ∧ 𝑀 ∈ ℤ ) → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )
6	4 5	syl	⊢ ( 𝜑 → ( 𝐵 logb ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )