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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clog-	⊢ log_
1		vb	⊢ 𝑏
2		cc	⊢ ℂ
3		cc0	⊢ 0
4		c1	⊢ 1
5	3 4	cpr	⊢ { 0 , 1 }
6	2 5	cdif	⊢ ( ℂ ∖ { 0 , 1 } )
7		vx	⊢ 𝑥
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	7 9 16	cmpt	⊢ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑏 ) ) )
18	1 6 17	cmpt	⊢ ( 𝑏 ∈ ( ℂ ∖ { 0 , 1 } ) ↦ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑏 ) ) ) )
19	0 18	wceq	⊢ log_ = ( 𝑏 ∈ ( ℂ ∖ { 0 , 1 } ) ↦ ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( ( log ‘ 𝑥 ) / ( log ‘ 𝑏 ) ) ) )