Definition df-blen 42364

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

Assertion

Ref	Expression
df-blen	|- #b = ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )

Detailed syntax breakdown of Definition df-blen

Step	Hyp	Ref	Expression
1		cblen 42363	. 2 class #b
2		vn	. . 3 setvar n
3		cvv 3200	. . 3 class _V
4	2	cv 1482	. . . . 5 class n
5		cc0 9936	. . . . 5 class 0
6	4, 5	wceq 1483	. . . 4 wff n = 0
7		c1 9937	. . . 4 class 1
8		c2 11070	. . . . . . 7 class 2
9		cabs 13974	. . . . . . . 8 class abs
10	4, 9	cfv 5888	. . . . . . 7 class ( abs ` n )
11		clogb 24502	. . . . . . 7 class logb
12	8, 10, 11	co 6650	. . . . . 6 class ( 2 logb ( abs ` n ) )
13		cfl 12591	. . . . . 6 class |_
14	12, 13	cfv 5888	. . . . 5 class ( |_ ` ( 2 logb ( abs ` n ) ) )
15		caddc 9939	. . . . 5 class +
16	14, 7, 15	co 6650	. . . 4 class ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 )
17	6, 7, 16	cif 4086	. . 3 class if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) )
18	2, 3, 17	cmpt 4729	. 2 class ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )
19	1, 18	wceq 1483	1 wff #b = ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )

This definition is referenced by:  blenval  42365