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 = ( 𝑛 ∈ V ↦ if ( 𝑛 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cblen #b
1 vn 𝑛
2 cvv V
3 1 cv 𝑛
4 cc0 0
5 3 4 wceq 𝑛 = 0
6 c1 1
7 cfl
8 c2 2
9 clogb logb
10 cabs abs
11 3 10 cfv ( abs ‘ 𝑛 )
12 8 11 9 co ( 2 logb ( abs ‘ 𝑛 ) )
13 12 7 cfv ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) )
14 caddc +
15 13 6 14 co ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 )
16 5 6 15 cif if ( 𝑛 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) )
17 1 2 16 cmpt ( 𝑛 ∈ V ↦ if ( 𝑛 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) ) )
18 0 17 wceq #b = ( 𝑛 ∈ V ↦ if ( 𝑛 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) ) )