Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for metakunt
General helpful statements
relogbexpd
Metamath Proof Explorer
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 ( 𝐵 ↑ 𝑀 ) ) = 𝑀 )