Theorem relogbval

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

	Ref	Expression
Assertion	relogbval	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$

Proof

Step	Hyp	Ref	Expression
1		zgt1rpn0n1	$$⊢B\in {\mathbb{Z}}_{\ge 2}\to \left(B\in {ℝ}^{+}\wedge B\ne 0\wedge B\ne 1\right)$$
2	1	adantr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(B\in {ℝ}^{+}\wedge B\ne 0\wedge B\ne 1\right)$$
3	2	simp1d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to B\in {ℝ}^{+}$$
4	3	rpcnd	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to B\in ℂ$$
5	2	simp2d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to B\ne 0$$
6	2	simp3d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to B\ne 1$$
7		eldifpr	$$⊢B\in \left(ℂ\setminus \left\{0,1\right\}\right)\leftrightarrow \left(B\in ℂ\wedge B\ne 0\wedge B\ne 1\right)$$
8	4 5 6 7	syl3anbrc	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to B\in \left(ℂ\setminus \left\{0,1\right\}\right)$$
9		simpr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to X\in {ℝ}^{+}$$
10	9	rpcnne0d	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to \left(X\in ℂ\wedge X\ne 0\right)$$
11		eldifsn	$$⊢X\in \left(ℂ\setminus \left\{0\right\}\right)\leftrightarrow \left(X\in ℂ\wedge X\ne 0\right)$$
12	10 11	sylibr	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to X\in \left(ℂ\setminus \left\{0\right\}\right)$$
13		logbval	$$⊢\left(B\in \left(ℂ\setminus \left\{0,1\right\}\right)\wedge X\in \left(ℂ\setminus \left\{0\right\}\right)\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$
14	8 12 13	syl2anc	$$⊢\left(B\in {\mathbb{Z}}_{\ge 2}\wedge X\in {ℝ}^{+}\right)\to {\log }_{B}X=\frac{\log X}{\log B}$$