Metamath Proof Explorer


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