Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Binary length
df-blen
Metamath Proof Explorer
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 n e. ZZ or even for n e. CC . (Contributed by AV , 16-May-2020)
Ref
Expression
Assertion
df-blen
⊢ # b = n ∈ V ⟼ if n = 0 1 log 2 n + 1
Detailed syntax breakdown
Step
Hyp
Ref
Expression
0
cblen
class # b
1
vn
setvar n
2
cvv
class V
3
1
cv
setvar n
4
cc0
class 0
5
3 4
wceq
wff n = 0
6
c1
class 1
7
cfl
class .
8
c2
class 2
9
clogb
class logb
10
cabs
class abs
11
3 10
cfv
class n
12
8 11 9
co
class log 2 n
13
12 7
cfv
class log 2 n
14
caddc
class +
15
13 6 14
co
class log 2 n + 1
16
5 6 15
cif
class if n = 0 1 log 2 n + 1
17
1 2 16
cmpt
class n ∈ V ⟼ if n = 0 1 log 2 n + 1
18
0 17
wceq
wff # b = n ∈ V ⟼ if n = 0 1 log 2 n + 1