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 = ( 𝑛 ∈ ℤ ↦ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cbits	⊢ bits
1		vn	⊢ 𝑛
2		cz	⊢ ℤ
3		vm	⊢ 𝑚
4		cn0	⊢ ℕ0
5		c2	⊢ 2
6		cdvds	⊢ ∥
7		cfl	⊢ ⌊
8	1	cv	⊢ 𝑛
9		cdiv	⊢ /
10		cexp	⊢ ↑
11	3	cv	⊢ 𝑚
12	5 11 10	co	⊢ ( 2 ↑ 𝑚 )
13	8 12 9	co	⊢ ( 𝑛 / ( 2 ↑ 𝑚 ) )
14	13 7	cfv	⊢ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) )
15	5 14 6	wbr	⊢ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) )
16	15	wn	⊢ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) )
17	16 3 4	crab	⊢ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) }
18	1 2 17	cmpt	⊢ ( 𝑛 ∈ ℤ ↦ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) } )
19	0 18	wceq	⊢ bits = ( 𝑛 ∈ ℤ ↦ { 𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ ( ⌊ ‘ ( 𝑛 / ( 2 ↑ 𝑚 ) ) ) } )