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 = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clogb	⊢ logb
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		cc0	⊢ 0
4		c1	⊢ 1
5	3 4	cpr	⊢ { 0 , 1 }
6	2 5	cdif	⊢ ( ℂ ∖ { 0 , 1 } )
7		vy	⊢ 𝑦
8	3	csn	⊢ { 0 }
9	2 8	cdif	⊢ ( ℂ ∖ { 0 } )
10		clog	⊢ log
11	7	cv	⊢ 𝑦
12	11 10	cfv	⊢ ( log ‘ 𝑦 )
13		cdiv	⊢ /
14	1	cv	⊢ 𝑥
15	14 10	cfv	⊢ ( log ‘ 𝑥 )
16	12 15 13	co	⊢ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) )
17	1 7 6 9 16	cmpo	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )
18	0 17	wceq	⊢ logb = ( 𝑥 ∈ ( ℂ ∖ { 0 , 1 } ) , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑦 ) / ( log ‘ 𝑥 ) ) )