nnlogbexp

Description: Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014) (Revised by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	nnlogbexp	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to \log_{B} B^{M} = M$

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	$⊢ B \in ℤ_{\geq 2} \to (B \in ℝ^{+} \land B \neq 0 \land B \neq 1)$
2	1	adantr	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to (B \in ℝ^{+} \land B \neq 0 \land B \neq 1)$
3	2	simp1d	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to B \in ℝ^{+}$
4	3	rpcnd	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to B \in ℂ$
5	4	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to B \in ℂ$
6	2	simp2d	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to B \neq 0$
7	6	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to B \neq 0$
8	2	simp3d	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to B \neq 1$
9	8	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to B \neq 1$
10		logb1	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log_{B} 1 = 0$
11	5 7 9 10	syl3anc	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to \log_{B} 1 = 0$
12		simpr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to M = 0$
13	12	oveq2d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to B^{M} = B^{0}$
14	5	exp0d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to B^{0} = 1$
15	13 14	eqtrd	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to B^{M} = 1$
16	15	oveq2d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to \log_{B} B^{M} = \log_{B} 1$
17	11 16 12	3eqtr4d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M = 0) \to \log_{B} B^{M} = M$
18	4	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B \in ℂ$
19	6	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B \neq 0$
20	8	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B \neq 1$
21		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
22	18 19 20 21	syl3anbrc	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B \in (ℂ ∖ \{0, 1\})$
23	3	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B \in ℝ^{+}$
24		simpr	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to M \in ℤ$
25	24	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to M \in ℤ$
26	23 25	rpexpcld	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B^{M} \in ℝ^{+}$
27	26	rpcnne0d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to (B^{M} \in ℂ \land B^{M} \neq 0)$
28		eldifsn	$⊢ B^{M} \in (ℂ ∖ \{0\}) \leftrightarrow (B^{M} \in ℂ \land B^{M} \neq 0)$
29	27 28	sylibr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B^{M} \in (ℂ ∖ \{0\})$
30		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land B^{M} \in (ℂ ∖ \{0\})) \to \log_{B} B^{M} = \frac{\log B^{M}}{\log B}$
31	22 29 30	syl2anc	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \log_{B} B^{M} = \frac{\log B^{M}}{\log B}$
32	24	zred	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to M \in ℝ$
33	32	adantr	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to M \in ℝ$
34	23 33	logcxpd	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \log B^{M} = M \log B$
35	18 19 25	cxpexpzd	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to B^{M} = B^{M}$
36	35	fveq2d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \log B^{M} = \log B^{M}$
37	34 36	eqtr3d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to M \log B = \log B^{M}$
38	37	oveq1d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \frac{M \log B}{\log B} = \frac{\log B^{M}}{\log B}$
39	33	recnd	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to M \in ℂ$
40	18 19	logcld	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \log B \in ℂ$
41		logne0	$⊢ (B \in ℝ^{+} \land B \neq 1) \to \log B \neq 0$
42	23 20 41	syl2anc	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \log B \neq 0$
43	39 40 42	divcan4d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \frac{M \log B}{\log B} = M$
44	31 38 43	3eqtr2d	$⊢ ((B \in ℤ_{\geq 2} \land M \in ℤ) \land M \neq 0) \to \log_{B} B^{M} = M$
45	17 44	pm2.61dane	$⊢ (B \in ℤ_{\geq 2} \land M \in ℤ) \to \log_{B} B^{M} = M$

Metamath Proof Explorer

Theorem nnlogbexp

Proof