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	$$⊢\mathrm{bits}=\left(n\in \mathbb{Z}⟼\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^m}⌋\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbits	$$class\mathrm{bits}$$
1		vn	$$setvarn$$
2		cz	$$class\mathbb{Z}$$
3		vm	$$setvarm$$
4		cn0	$$class{\mathbb{N}}_0$$
5		c2	$$class2$$
6		cdvds	$$class\parallel$$
7		cfl	$$class⌊.⌋$$
8	1	cv	$$setvarn$$
9		cdiv	$$class÷$$
10		cexp	$$class^$$
11	3	cv	$$setvarm$$
12	5 11 10	co	$$class{2}^m$$
13	8 12 9	co	$$class\left(\frac{n}{2^m}\right)$$
14	13 7	cfv	$$class⌊\frac{n}{2^m}⌋$$
15	5 14 6	wbr	$$wff2\parallel ⌊\frac{n}{2^m}⌋$$
16	15	wn	$$wff\neg 2\parallel ⌊\frac{n}{2^m}⌋$$
17	16 3 4	crab	$$class\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^m}⌋\right\}$$
18	1 2 17	cmpt	$$class\left(n\in \mathbb{Z}⟼\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^m}⌋\right\}\right)$$
19	0 18	wceq	$$wff\mathrm{bits}=\left(n\in \mathbb{Z}⟼\left\{m\in {\mathbb{N}}_0|\neg 2\parallel ⌊\frac{n}{2^m}⌋\right\}\right)$$