Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-blen Structured version   Visualization version   GIF version

Definition df-blen 42135
Description: Define the binary length of an integer. Definition in section 1.3 of [AhoHopUll] p. 12. Although not restricted to integers, this definition is only meaningful for 𝑛 ∈ ℤ or even for 𝑛 ∈ ℂ. (Contributed by AV, 16-May-2020.)
Assertion
Ref Expression
df-blen #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))

Detailed syntax breakdown of Definition df-blen
StepHypRef Expression
1 cblen 42134 . 2 class #b
2 vn . . 3 setvar 𝑛
3 cvv 3198 . . 3 class V
42cv 1481 . . . . 5 class 𝑛
5 cc0 9933 . . . . 5 class 0
64, 5wceq 1482 . . . 4 wff 𝑛 = 0
7 c1 9934 . . . 4 class 1
8 c2 11067 . . . . . . 7 class 2
9 cabs 13968 . . . . . . . 8 class abs
104, 9cfv 5886 . . . . . . 7 class (abs‘𝑛)
11 clogb 24496 . . . . . . 7 class logb
128, 10, 11co 6647 . . . . . 6 class (2 logb (abs‘𝑛))
13 cfl 12586 . . . . . 6 class
1412, 13cfv 5886 . . . . 5 class (⌊‘(2 logb (abs‘𝑛)))
15 caddc 9936 . . . . 5 class +
1614, 7, 15co 6647 . . . 4 class ((⌊‘(2 logb (abs‘𝑛))) + 1)
176, 7, 16cif 4084 . . 3 class if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1))
182, 3, 17cmpt 4727 . 2 class (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
191, 18wceq 1482 1 wff #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
Colors of variables: wff setvar class
This definition is referenced by:  blenval  42136
  Copyright terms: Public domain W3C validator