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 44915
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 44914 . 2 class #b
2 vn . . 3 setvar 𝑛
3 cvv 3480 . . 3 class V
42cv 1537 . . . . 5 class 𝑛
5 cc0 10535 . . . . 5 class 0
64, 5wceq 1538 . . . 4 wff 𝑛 = 0
7 c1 10536 . . . 4 class 1
8 c2 11689 . . . . . . 7 class 2
9 cabs 14593 . . . . . . . 8 class abs
104, 9cfv 6343 . . . . . . 7 class (abs‘𝑛)
11 clogb 25357 . . . . . . 7 class logb
128, 10, 11co 7149 . . . . . 6 class (2 logb (abs‘𝑛))
13 cfl 13164 . . . . . 6 class
1412, 13cfv 6343 . . . . 5 class (⌊‘(2 logb (abs‘𝑛)))
15 caddc 10538 . . . . 5 class +
1614, 7, 15co 7149 . . . 4 class ((⌊‘(2 logb (abs‘𝑛))) + 1)
176, 7, 16cif 4450 . . 3 class if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1))
182, 3, 17cmpt 5132 . 2 class (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
191, 18wceq 1538 1 wff #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
Colors of variables: wff setvar class
This definition is referenced by:  blenval  44916
  Copyright terms: Public domain W3C validator