Definition df-logbALT 42507

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.)

Assertion

Ref	Expression
df-logbALT	|- log_ = ( b e. ( CC \ { 0 , 1 } ) |-> ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` b ) ) ) )

Distinct variable group:   x, b

Detailed syntax breakdown of Definition df-logbALT

Step	Hyp	Ref	Expression
1		clog- 42506	. 2 class log_
2		vb	. . 3 setvar b
3		cc 9934	. . . 4 class CC
4		cc0 9936	. . . . 5 class 0
5		c1 9937	. . . . 5 class 1
6	4, 5	cpr 4179	. . . 4 class { 0 , 1 }
7	3, 6	cdif 3571	. . 3 class ( CC \ { 0 , 1 } )
8		vx	. . . 4 setvar x
9	4	csn 4177	. . . . 5 class { 0 }
10	3, 9	cdif 3571	. . . 4 class ( CC \ { 0 } )
11	8	cv 1482	. . . . . 6 class x
12		clog 24301	. . . . . 6 class log
13	11, 12	cfv 5888	. . . . 5 class ( log ` x )
14	2	cv 1482	. . . . . 6 class b
15	14, 12	cfv 5888	. . . . 5 class ( log ` b )
16		cdiv 10684	. . . . 5 class /
17	13, 15, 16	co 6650	. . . 4 class ( ( log ` x ) / ( log ` b ) )
18	8, 10, 17	cmpt 4729	. . 3 class ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` b ) ) )
19	2, 7, 18	cmpt 4729	. 2 class ( b e. ( CC \ { 0 , 1 } ) |-> ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` b ) ) ) )
20	1, 19	wceq 1483	1 wff log_ = ( b e. ( CC \ { 0 , 1 } ) |-> ( x e. ( CC \ { 0 } ) |-> ( ( log ` x ) / ( log ` b ) ) ) )

This definition is referenced by: (None)