Definition df-logb

Description: Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as ( B logb X ) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition is according to Wikipedia "Complex logarithm": https://en.wikipedia.org/wiki/Complex_logarithm#Logarithms_to_other_bases (10-Jun-2020). (Contributed by David A. Wheeler, 21-Jan-2017)

	Ref	Expression
Assertion	df-logb	$$⊢\mathrm{logb}=\left(x\in \left(ℂ\setminus \left\{0,1\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{\log y}{\log x}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clogb	$$class\mathrm{logb}$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		cc0	$$class0$$
4		c1	$$class1$$
5	3 4	cpr	$$class\left\{0,1\right\}$$
6	2 5	cdif	$$class\left(ℂ\setminus \left\{0,1\right\}\right)$$
7		vy	$$setvary$$
8	3	csn	$$class\left\{0\right\}$$
9	2 8	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
10		clog	$$classlog$$
11	7	cv	$$setvary$$
12	11 10	cfv	$$class\log y$$
13		cdiv	$$class÷$$
14	1	cv	$$setvarx$$
15	14 10	cfv	$$class\log x$$
16	12 15 13	co	$$class\left(\frac{\log y}{\log x}\right)$$
17	1 7 6 9 16	cmpo	$$class\left(x\in \left(ℂ\setminus \left\{0,1\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{\log y}{\log x}\right)$$
18	0 17	wceq	$$wff\mathrm{logb}=\left(x\in \left(ℂ\setminus \left\{0,1\right\}\right),y\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{\log y}{\log x}\right)$$