Definition df-bits 12460

Description: Define the binary bits of an integer. The expression M e. (bits ` N ) 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.)

Assertion

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

Distinct variable group:   m, n

Detailed syntax breakdown of Definition df-bits

Step	Hyp	Ref	Expression
1		cbits 12459	. 2 class bits
2		vn	. . 3 setvar n
3		cz 9454	. . 3 class ZZ
4		c2 9169	. . . . . 6 class 2
5	2	cv 1394	. . . . . . . 8 class n
6		vm	. . . . . . . . . 10 setvar m
7	6	cv 1394	. . . . . . . . 9 class m
8		cexp 10768	. . . . . . . . 9 class ^
9	4, 7, 8	co 6007	. . . . . . . 8 class ( 2 ^ m )
10		cdiv 8827	. . . . . . . 8 class /
11	5, 9, 10	co 6007	. . . . . . 7 class ( n / ( 2 ^ m ) )
12		cfl 10496	. . . . . . 7 class |_
13	11, 12	cfv 5318	. . . . . 6 class ( |_ ` ( n / ( 2 ^ m ) ) )
14		cdvds 12306	. . . . . 6 class ||
15	4, 13, 14	wbr 4083	. . . . 5 wff 2 || ( |_ ` ( n / ( 2 ^ m ) ) )
16	15	wn 3	. . . 4 wff -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) )
17		cn0 9377	. . . 4 class NN0
18	16, 6, 17	crab 2512	. . 3 class { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) }
19	2, 3, 18	cmpt 4145	. 2 class ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )
20	1, 19	wceq 1395	1 wff bits = ( n e. ZZ |-> { m e. NN0 | -. 2 || ( |_ ` ( n / ( 2 ^ m ) ) ) } )

This definition is referenced by:  bitsfval  12461  bitsval  12462  bitsf  12465