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

Detailed syntax breakdown

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