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 ) ) )