Definition df-logbALT

Description: Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as ( ( log_B )X ) for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017) (New usage is discouraged.)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clog-	$$class\mathrm{log\_}$$
1		vb	$$setvarb$$
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		vx	$$setvarx$$
8	3	csn	$$class\left\{0\right\}$$
9	2 8	cdif	$$class\left(ℂ\setminus \left\{0\right\}\right)$$
10		clog	$$classlog$$
11	7	cv	$$setvarx$$
12	11 10	cfv	$$class\log x$$
13		cdiv	$$class÷$$
14	1	cv	$$setvarb$$
15	14 10	cfv	$$class\log b$$
16	12 15 13	co	$$class\left(\frac{\log x}{\log b}\right)$$
17	7 9 16	cmpt	$$class\left(x\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{\log x}{\log b}\right)$$
18	1 6 17	cmpt	$$class\left(b\in \left(ℂ\setminus \left\{0,1\right\}\right)⟼\left(x\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{\log x}{\log b}\right)\right)$$
19	0 18	wceq	$$wff\mathrm{log\_}=\left(b\in \left(ℂ\setminus \left\{0,1\right\}\right)⟼\left(x\in \left(ℂ\setminus \left\{0\right\}\right)⟼\frac{\log x}{\log b}\right)\right)$$