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 16307
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 16304 . 2 class bits
2 vn . . 3 setvar 𝑛
3 cz 12504 . . 3 class β„€
4 c2 12213 . . . . . 6 class 2
52cv 1541 . . . . . . . 8 class 𝑛
6 vm . . . . . . . . . 10 setvar π‘š
76cv 1541 . . . . . . . . 9 class π‘š
8 cexp 13973 . . . . . . . . 9 class ↑
94, 7, 8co 7358 . . . . . . . 8 class (2β†‘π‘š)
10 cdiv 11817 . . . . . . . 8 class /
115, 9, 10co 7358 . . . . . . 7 class (𝑛 / (2β†‘π‘š))
12 cfl 13701 . . . . . . 7 class ⌊
1311, 12cfv 6497 . . . . . 6 class (βŒŠβ€˜(𝑛 / (2β†‘π‘š)))
14 cdvds 16141 . . . . . 6 class βˆ₯
154, 13, 14wbr 5106 . . . . 5 wff 2 βˆ₯ (βŒŠβ€˜(𝑛 / (2β†‘π‘š)))
1615wn 3 . . . 4 wff Β¬ 2 βˆ₯ (βŒŠβ€˜(𝑛 / (2β†‘π‘š)))
17 cn0 12418 . . . 4 class β„•0
1816, 6, 17crab 3406 . . 3 class {π‘š ∈ β„•0 ∣ Β¬ 2 βˆ₯ (βŒŠβ€˜(𝑛 / (2β†‘π‘š)))}
192, 3, 18cmpt 5189 . 2 class (𝑛 ∈ β„€ ↦ {π‘š ∈ β„•0 ∣ Β¬ 2 βˆ₯ (βŒŠβ€˜(𝑛 / (2β†‘π‘š)))})
201, 19wceq 1542 1 wff bits = (𝑛 ∈ β„€ ↦ {π‘š ∈ β„•0 ∣ Β¬ 2 βˆ₯ (βŒŠβ€˜(𝑛 / (2β†‘π‘š)))})
Colors of variables: wff setvar class
This definition is referenced by:  bitsfval  16308  bitsval  16309  bitsf  16312
  Copyright terms: Public domain W3C validator