MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-bits Structured version   Visualization version   GIF version

Definition df-bits 14928
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
StepHypRef Expression
1 cbits 14925 . 2 class bits
2 vn . . 3 setvar 𝑛
3 cz 11210 . . 3 class
4 c2 10917 . . . . . 6 class 2
52cv 1473 . . . . . . . 8 class 𝑛
6 vm . . . . . . . . . 10 setvar 𝑚
76cv 1473 . . . . . . . . 9 class 𝑚
8 cexp 12677 . . . . . . . . 9 class
94, 7, 8co 6527 . . . . . . . 8 class (2↑𝑚)
10 cdiv 10533 . . . . . . . 8 class /
115, 9, 10co 6527 . . . . . . 7 class (𝑛 / (2↑𝑚))
12 cfl 12408 . . . . . . 7 class
1311, 12cfv 5790 . . . . . 6 class (⌊‘(𝑛 / (2↑𝑚)))
14 cdvds 14767 . . . . . 6 class
154, 13, 14wbr 4577 . . . . 5 wff 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))
1615wn 3 . . . 4 wff ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))
17 cn0 11139 . . . 4 class 0
1816, 6, 17crab 2899 . . 3 class {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))}
192, 3, 18cmpt 4637 . 2 class (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))})
201, 19wceq 1474 1 wff bits = (𝑛 ∈ ℤ ↦ {𝑚 ∈ ℕ0 ∣ ¬ 2 ∥ (⌊‘(𝑛 / (2↑𝑚)))})
Colors of variables: wff setvar class
This definition is referenced by:  bitsfval  14929  bitsval  14930  bitsf  14933
  Copyright terms: Public domain W3C validator