relogbval

Description: Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017)

		Ref	Expression
	Assertion	relogbval	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to \log_{B} X = \frac{\log X}{\log B}$

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 X \in ℝ^{+}) \to (B \in ℝ^{+} \land B \neq 0 \land B \neq 1)$
3	2	simp1d	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to B \in ℝ^{+}$
4	3	rpcnd	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to B \in ℂ$
5	2	simp2d	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to B \neq 0$
6	2	simp3d	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to B \neq 1$
7		eldifpr	$⊢ B \in (ℂ ∖ \{0, 1\}) \leftrightarrow (B \in ℂ \land B \neq 0 \land B \neq 1)$
8	4 5 6 7	syl3anbrc	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to B \in (ℂ ∖ \{0, 1\})$
9		simpr	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to X \in ℝ^{+}$
10	9	rpcnne0d	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to (X \in ℂ \land X \neq 0)$
11		eldifsn	$⊢ X \in (ℂ ∖ \{0\}) \leftrightarrow (X \in ℂ \land X \neq 0)$
12	10 11	sylibr	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to X \in (ℂ ∖ \{0\})$
13		logbval	$⊢ (B \in (ℂ ∖ \{0, 1\}) \land X \in (ℂ ∖ \{0\})) \to \log_{B} X = \frac{\log X}{\log B}$
14	8 12 13	syl2anc	$⊢ (B \in ℤ_{\geq 2} \land X \in ℝ^{+}) \to \log_{B} X = \frac{\log X}{\log B}$

Metamath Proof Explorer