Definition df-bits

Description: Define the binary bits of an integer. The expression M e. ( bitsN ) means that the M -th bit of N is 1 (and its negation means the bit is 0). (Contributed by Mario Carneiro, 4-Sep-2016)

	Ref	Expression
Assertion	df-bits	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbits	|- bits
1		vn	|- n
2		cz	|- ZZ
3		vm	|- m
4		cn0	|- NN0
5		c2	|- 2
6		cdvds	|- ||
7		cfl	|- |_
8	1	cv	|- n
9		cdiv	|- /
10		cexp	|- ^
11	3	cv	|- m
12	5 11 10	co	|- ( 2 ^ m )
13	8 12 9	co	|- ( n / ( 2 ^ m ) )
14	13 7	cfv	|- ( |_ ` ( n / ( 2 ^ m ) ) )
15	5 14 6	wbr	|- 2 || ( |_ ` ( n / ( 2 ^ m ) ) )
16	15	wn	|- -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) )
17	16 3 4	crab	|- { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) }
18	1 2 17	cmpt	|- ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
19	0 18	wceq	|- bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )