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 e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cblen	|- #b
1		vn	|- n
2		cvv	|- _V
3	1	cv	|- n
4		cc0	|- 0
5	3 4	wceq	|- n = 0
6		c1	|- 1
7		cfl	|- |_
8		c2	|- 2
9		clogb	|- logb
10		cabs	|- abs
11	3 10	cfv	|- ( abs ` n )
12	8 11 9	co	|- ( 2 logb ( abs ` n ) )
13	12 7	cfv	|- ( |_ ` ( 2 logb ( abs ` n ) ) )
14		caddc	|- +
15	13 6 14	co	|- ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 )
16	5 6 15	cif	|- if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) )
17	1 2 16	cmpt	|- ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )
18	0 17	wceq	|- #b = ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )