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

Definition df-bits 12613
Description: Define the binary bits of an integer. The expression  M  e.  (bits `  N ) 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.)
Assertion
Ref Expression
df-bits  |- bits  =  ( n  e.  ZZ  |->  { m  e.  NN0  |  -.  2  ||  ( |_
`  ( n  / 
( 2 ^ m
) ) ) } )
Distinct variable group:    m, n

Detailed syntax breakdown of Definition df-bits
StepHypRef Expression
1 cbits 12610 . 2  class bits
2 vn . . 3  set  n
3 cz 10024 . . 3  class  ZZ
4 c2 9795 . . . . . 6  class  2
52cv 1622 . . . . . . . 8  class  n
6 vm . . . . . . . . . 10  set  m
76cv 1622 . . . . . . . . 9  class  m
8 cexp 11104 . . . . . . . . 9  class  ^
94, 7, 8co 5858 . . . . . . . 8  class  ( 2 ^ m )
10 cdiv 9423 . . . . . . . 8  class  /
115, 9, 10co 5858 . . . . . . 7  class  ( n  /  ( 2 ^ m ) )
12 cfl 10924 . . . . . . 7  class  |_
1311, 12cfv 5255 . . . . . 6  class  ( |_
`  ( n  / 
( 2 ^ m
) ) )
14 cdivides 12531 . . . . . 6  class  ||
154, 13, 14wbr 4023 . . . . 5  wff  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) )
1615wn 3 . . . 4  wff  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) )
17 cn0 9965 . . . 4  class  NN0
1816, 6, 17crab 2547 . . 3  class  { m  e.  NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) }
192, 3, 18cmpt 4077 . 2  class  ( n  e.  ZZ  |->  { m  e.  NN0  |  -.  2  ||  ( |_ `  (
n  /  ( 2 ^ m ) ) ) } )
201, 19wceq 1623 1  wff bits  =  ( n  e.  ZZ  |->  { m  e.  NN0  |  -.  2  ||  ( |_
`  ( n  / 
( 2 ^ m
) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  bitsfval  12614  bitsval  12615  bitsf  12618
  Copyright terms: Public domain W3C validator