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
⊢ φ → B ∈ ℝ +
relogbexpd.2
⊢ φ → B ≠ 1
relogbexpd.3
⊢ φ → M ∈ ℤ
Assertion
relogbexpd
⊢ φ → log B B M = M
Proof
Step
Hyp
Ref
Expression
1
relogbexpd.1
⊢ φ → B ∈ ℝ +
2
relogbexpd.2
⊢ φ → B ≠ 1
3
relogbexpd.3
⊢ φ → M ∈ ℤ
4
1 2 3
3jca
⊢ φ → B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ
5
relogbexp
⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → log B B M = M
6
4 5
syl
⊢ φ → log B B M = M