relogbcxp

Description: Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020)

		Ref	Expression
	Assertion	relogbcxp	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \log_{B} B^{X} = X$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ B \in (ℝ^{+} ∖ \{1\}) \leftrightarrow (B \in ℝ^{+} \land B \neq 1)$
2		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
3	2	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in ℂ$
4		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
5	4	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 0$
6		simpr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 1$
7		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
8	3 5 6 7	syl3anbrc	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in (ℂ ∖ \{0, 1\})$
9	1 8	sylbi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in (ℂ ∖ \{0, 1\})$
10		eldifi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in ℝ^{+}$
11	10 2	syl	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \in ℂ$
12		recn	$⊢ X \in ℝ \to X \in ℂ$
13		cxpcl	$⊢ (B \in ℂ \land X \in ℂ) \to B^{X} \in ℂ$
14	11 12 13	syl2an	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to B^{X} \in ℂ$
15	11	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to B \in ℂ$
16	1 5	sylbi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to B \neq 0$
17	16	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to B \neq 0$
18	12	adantl	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to X \in ℂ$
19	15 17 18	cxpne0d	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to B^{X} \neq 0$
20		eldifsn	$⊢ B^{X} \in (ℂ ∖ \{0\}) \leftrightarrow (B^{X} \in ℂ \land B^{X} \neq 0)$
21	14 19 20	sylanbrc	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to B^{X} \in (ℂ ∖ \{0\})$
22		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land B^{X} \in (ℂ ∖ \{0\})) \to \log_{B} B^{X} = \frac{\log B^{X}}{\log B}$
23	9 21 22	syl2an2r	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \log_{B} B^{X} = \frac{\log B^{X}}{\log B}$
24		logcxp	$⊢ (B \in ℝ^{+} \land X \in ℝ) \to \log B^{X} = X \log B$
25	10 24	sylan	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \log B^{X} = X \log B$
26	25	oveq1d	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \frac{\log B^{X}}{\log B} = \frac{X \log B}{\log B}$
27		eldif	$⊢ B \in (ℝ^{+} ∖ \{1\}) \leftrightarrow (B \in ℝ^{+} \land \neg B \in \{1\})$
28		rpcnne0	$⊢ B \in ℝ^{+} \to (B \in ℂ \land B \neq 0)$
29	28	adantr	$⊢ (B \in ℝ^{+} \land \neg B \in \{1\}) \to (B \in ℂ \land B \neq 0)$
30	27 29	sylbi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to (B \in ℂ \land B \neq 0)$
31		logcl	$⊢ (B \in ℂ \land B \neq 0) \to \log B \in ℂ$
32	30 31	syl	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to \log B \in ℂ$
33	32	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \log B \in ℂ$
34		logne0	$⊢ (B \in ℝ^{+} \land B \neq 1) \to \log B \neq 0$
35	1 34	sylbi	$⊢ B \in (ℝ^{+} ∖ \{1\}) \to \log B \neq 0$
36	35	adantr	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \log B \neq 0$
37	18 33 36	divcan4d	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \frac{X \log B}{\log B} = X$
38	23 26 37	3eqtrd	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land X \in ℝ) \to \log_{B} B^{X} = X$

Metamath Proof Explorer

Theorem relogbcxp

Proof