Definition df-bits 16456

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

Assertion

Ref	Expression
df-bits	⊢ bits = (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))})

Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Definition df-bits

Step	Hyp	Ref	Expression
1		cbits 16453	. 2 class bits
2		vn	. . 3 setvar 𝑛
3		cz 12611	. . 3 class ℤ
4		c2 12319	. . . . . 6 class 2
5	2	cv 1536	. . . . . . . 8 class 𝑛
6		vm	. . . . . . . . . 10 setvar 𝑚
7	6	cv 1536	. . . . . . . . 9 class 𝑚
8		cexp 14099	. . . . . . . . 9 class ↑
9	4, 7, 8	co 7431	. . . . . . . 8 class (2↑𝑚)
10		cdiv 11918	. . . . . . . 8 class /
11	5, 9, 10	co 7431	. . . . . . 7 class (𝑛 / (2↑𝑚))
12		cfl 13827	. . . . . . 7 class ⌊
13	11, 12	cfv 6563	. . . . . 6 class (⌊‘(𝑛 / (2↑𝑚)))
14		cdvds 16287	. . . . . 6 class ∥
15	4, 13, 14	wbr 5148	. . . . 5 wff 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))
16	15	wn 3	. . . 4 wff ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))
17		cn0 12524	. . . 4 class ℕ0
18	16, 6, 17	crab 3433	. . 3 class {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))}
19	2, 3, 18	cmpt 5231	. 2 class (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))})
20	1, 19	wceq 1537	1 wff bits = (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))})

This definition is referenced by:  bitsfval  16457  bitsval  16458  bitsf  16461