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	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clogb	|- logb
1		vx	|- x
2		cc	|- CC
3		cc0	|- 0
4		c1	|- 1
5	3 4	cpr	|- { 0 , 1 }
6	2 5	cdif	|- ( CC \ { 0 , 1 } )
7		vy	|- y
8	3	csn	|- { 0 }
9	2 8	cdif	|- ( CC \ { 0 } )
10		clog	|- log
11	7	cv	|- y
12	11 10	cfv	|- ( log ` y )
13		cdiv	|- /
14	1	cv	|- x
15	14 10	cfv	|- ( log ` x )
16	12 15 13	co	|- ( ( log ` y ) / ( log ` x ) )
17	1 7 6 9 16	cmpo	|- ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
18	0 17	wceq	|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )