Metamath Proof Explorer

Definition df-blen

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