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 \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to \log_{B} B^{M} = M$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
2	1	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in ℂ$
3		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
4	3	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 0$
5		simpr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 1$
6	2 4 5	3jca	$⊢ (B \in ℝ^{+} \land B \neq 1) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
7		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
8	6 7	sylibr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in (ℂ ∖ \{0, 1\})$
9		relogbzexp	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land B \in ℝ^{+} \land M \in ℤ) \to \log_{B} B^{M} = M \log_{B} B$
10	8 9	stoic4a	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to \log_{B} B^{M} = M \log_{B} B$
11	6	3adant3	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
12		logbid1	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log_{B} B = 1$
13	11 12	syl	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to \log_{B} B = 1$
14	13	oveq2d	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to M \log_{B} B = M \cdot 1$
15		zcn	$⊢ M \in ℤ \to M \in ℂ$
16	15	3ad2ant3	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to M \in ℂ$
17	16	mulid1d	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to M \cdot 1 = M$
18	10 14 17	3eqtrd	$⊢ (B \in ℝ^{+} \land B \neq 1 \land M \in ℤ) \to \log_{B} B^{M} = M$