This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → log B B M = M

Proof

Step Hyp Ref Expression
1 rpcn ⊢ B ∈ ℝ + → B ∈ ℂ
2 1 adantr ⊢ B ∈ ℝ + ∧ B ≠ 1 → B ∈ ℂ
3 rpne0 ⊢ B ∈ ℝ + → B ≠ 0
4 3 adantr ⊢ B ∈ ℝ + ∧ B ≠ 1 → B ≠ 0
5 simpr ⊢ B ∈ ℝ + ∧ B ≠ 1 → B ≠ 1
6 2 4 5 3jca ⊢ B ∈ ℝ + ∧ B ≠ 1 → B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
7 eldifpr ⊢ B ∈ ℂ ∖ 0 1 ↔ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
8 6 7 sylibr ⊢ B ∈ ℝ + ∧ B ≠ 1 → B ∈ ℂ ∖ 0 1
9 relogbzexp ⊢ B ∈ ℂ ∖ 0 1 ∧ B ∈ ℝ + ∧ M ∈ ℤ → log B B M = M ⁢ log B B
10 8 9 stoic4a ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → log B B M = M ⁢ log B B
11 6 3adant3 ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1
12 logbid1 ⊢ B ∈ ℂ ∧ B ≠ 0 ∧ B ≠ 1 → log B B = 1
13 11 12 syl ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → log B B = 1
14 13 oveq2d ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → M ⁢ log B B = M ⋅ 1
15 zcn ⊢ M ∈ ℤ → M ∈ ℂ
16 15 3ad2ant3 ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → M ∈ ℂ
17 16 mulridd ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → M ⋅ 1 = M
18 10 14 17 3eqtrd ⊢ B ∈ ℝ + ∧ B ≠ 1 ∧ M ∈ ℤ → log B B M = M