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

Definition df-bits 12939
 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-bits
StepHypRef Expression
1 cbits 12936 . 2 bits
2 vn . . 3
3 cz 10287 . . 3
4 c2 10054 . . . . . 6
52cv 1652 . . . . . . . 8
6 vm . . . . . . . . . 10
76cv 1652 . . . . . . . . 9
8 cexp 11387 . . . . . . . . 9
94, 7, 8co 6084 . . . . . . . 8
10 cdiv 9682 . . . . . . . 8
115, 9, 10co 6084 . . . . . . 7
12 cfl 11206 . . . . . . 7
1311, 12cfv 5457 . . . . . 6
14 cdivides 12857 . . . . . 6
154, 13, 14wbr 4215 . . . . 5
1615wn 3 . . . 4
17 cn0 10226 . . . 4
1816, 6, 17crab 2711 . . 3
192, 3, 18cmpt 4269 . 2
201, 19wceq 1653 1 bits
 Colors of variables: wff set class This definition is referenced by:  bitsfval  12940  bitsval  12941  bitsf  12944
 Copyright terms: Public domain W3C validator