relogbcxpb

Description: The logarithm is the inverse of the exponentiation. Observation in Cohen4 p. 348. (Contributed by AV, 11-Jun-2020)

		Ref	Expression
	Assertion	relogbcxpb	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \to (\log_{B} X = Y \leftrightarrow B^{Y} = X)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ Y = \log_{B} X \to B^{Y} = B^{\log_{B} X}$
2	1	eqcoms	$⊢ \log_{B} X = Y \to B^{Y} = B^{\log_{B} X}$
3		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
4	3	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in ℂ$
5		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
6	5	adantr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 0$
7		simpr	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \neq 1$
8		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
9	4 6 7 8	syl3anbrc	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in (ℂ ∖ \{0, 1\})$
10		rpcndif0	$⊢ X \in ℝ^{+} \to X \in (ℂ ∖ \{0\})$
11	9 10	anim12i	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+}) \to (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\}))$
12	11	3adant3	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \to (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\}))$
13		cxplogb	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to B^{\log_{B} X} = X$
14	12 13	syl	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \to B^{\log_{B} X} = X$
15	2 14	sylan9eqr	$⊢ (((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \land \log_{B} X = Y) \to B^{Y} = X$
16		oveq2	$⊢ X = B^{Y} \to \log_{B} X = \log_{B} B^{Y}$
17	16	eqcoms	$⊢ B^{Y} = X \to \log_{B} X = \log_{B} B^{Y}$
18		eldifsn	$⊢ B \in (ℝ^{+} ∖ \{1\}) \leftrightarrow (B \in ℝ^{+} \land B \neq 1)$
19	18	biimpri	$⊢ (B \in ℝ^{+} \land B \neq 1) \to B \in (ℝ^{+} ∖ \{1\})$
20	19	anim1i	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land Y \in ℝ) \to (B \in (ℝ^{+} ∖ \{1\}) \land Y \in ℝ)$
21	20	3adant2	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \to (B \in (ℝ^{+} ∖ \{1\}) \land Y \in ℝ)$
22		relogbcxp	$⊢ (B \in (ℝ^{+} ∖ \{1\}) \land Y \in ℝ) \to \log_{B} B^{Y} = Y$
23	21 22	syl	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \to \log_{B} B^{Y} = Y$
24	17 23	sylan9eqr	$⊢ (((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \land B^{Y} = X) \to \log_{B} X = Y$
25	15 24	impbida	$⊢ ((B \in ℝ^{+} \land B \neq 1) \land X \in ℝ^{+} \land Y \in ℝ) \to (\log_{B} X = Y \leftrightarrow B^{Y} = X)$

Metamath Proof Explorer

Theorem relogbcxpb

Proof