cxplogb

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

		Ref	Expression
	Assertion	cxplogb	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B^{\log_{B} X} = X$

Proof

Step	Hyp	Ref	Expression
1		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
2	1	oveq2d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B^{\log_{B} X} = B^{\frac{\log X}{\log B}}$
3		eldifi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to B \in ℂ$
4	3	adantr	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B \in ℂ$
5		eldif	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land \neg B \in \{0, 1\})$
6		0elpr01	$⊢ 0 \in \{0, 1\}$
7		eleq1	$⊢ B = 0 \to (B \in \{0, 1\} \leftrightarrow 0 \in \{0, 1\})$
8	6 7	mpbiri	$⊢ B = 0 \to B \in \{0, 1\}$
9	8	necon3bi	$⊢ \neg B \in \{0, 1\} \to B \neq 0$
10	9	adantl	$⊢ (B \in ℂ \land \neg B \in \{0, 1\}) \to B \neq 0$
11	5 10	sylbi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to B \neq 0$
12	11	adantr	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B \neq 0$
13		eldif	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land \neg X \in \{0\})$
14		c0ex	$⊢ 0 \in V$
15	14	snid	$⊢ 0 \in \{0\}$
16		eleq1	$⊢ X = 0 \to (X \in \{0\} \leftrightarrow 0 \in \{0\})$
17	15 16	mpbiri	$⊢ X = 0 \to X \in \{0\}$
18	17	necon3bi	$⊢ \neg X \in \{0\} \to X \neq 0$
19	18	anim2i	$⊢ (X \in ℂ \land \neg X \in \{0\}) \to (X \in ℂ \land X \neq 0)$
20	13 19	sylbi	$⊢ X \in (ℂ ∖ \{0\}) \to (X \in ℂ \land X \neq 0)$
21		logcl	$⊢ (X \in ℂ \land X \neq 0) \to \log X \in ℂ$
22	20 21	syl	$⊢ X \in (ℂ ∖ \{0\}) \to \log X \in ℂ$
23	22	adantl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log X \in ℂ$
24	9	anim2i	$⊢ (B \in ℂ \land \neg B \in \{0, 1\}) \to (B \in ℂ \land B \neq 0)$
25	5 24	sylbi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to (B \in ℂ \land B \neq 0)$
26		logcl	$⊢ (B \in ℂ \land B \neq 0) \to \log B \in ℂ$
27	25 26	syl	$⊢ B \in (ℂ ∖ \{0, 1\}) \to \log B \in ℂ$
28	27	adantr	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log B \in ℂ$
29		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
30	29	birani	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to (B \in ℂ \land B \neq 0 \land B \neq 1)$
31		logccne0	$⊢ (B \in ℂ \land B \neq 0 \land B \neq 1) \to \log B \neq 0$
32	30 31	syl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log B \neq 0$
33	23 28 32	divcld	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \frac{\log X}{\log B} \in ℂ$
34	4 12 33	cxpefd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B^{\frac{\log X}{\log B}} = e^{(\frac{\log X}{\log B}) \log B}$
35		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
36	35 21	sylbi	$⊢ X \in (ℂ ∖ \{0\}) \to \log X \in ℂ$
37	36	adantl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log X \in ℂ$
38	29 31	sylbi	$⊢ B \in (ℂ ∖ \{0, 1\}) \to \log B \neq 0$
39	38	adantr	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log B \neq 0$
40	37 28 39	divcan1d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to (\frac{\log X}{\log B}) \log B = \log X$
41	40	fveq2d	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to e^{(\frac{\log X}{\log B}) \log B} = e^{\log X}$
42		eflog	$⊢ (X \in ℂ \land X \neq 0) \to e^{\log X} = X$
43	35 42	sylbi	$⊢ X \in (ℂ ∖ \{0\}) \to e^{\log X} = X$
44	43	adantl	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to e^{\log X} = X$
45	41 44	eqtrd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to e^{(\frac{\log X}{\log B}) \log B} = X$
46	2 34 45	3eqtrd	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B^{\log_{B} X} = X$

Metamath Proof Explorer

Theorem cxplogb

Proof