Theorem logb2aval

Description: Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb <. B , X >. (Contributed by David A. Wheeler, 21-Jan-2017) (Revised by David A. Wheeler, 16-Jul-2017)

	Ref	Expression
Assertion	logb2aval	$$⊢\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}$$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$$⊢{\log }_{B}X={\log }_{⟨B,X⟩}$$
2		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}$$
3	1 2	eqtr3id	$$⊢\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}$$