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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cblen
1		vn	$$setvarn$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarn$$
4		cc0	$$class0$$
5	3 4	wceq	$$wffn=0$$
6		c1	$$class1$$
7		cfl	$$class⌊.⌋$$
8		c2	$$class2$$
9		clogb	$$class\mathrm{logb}$$
10		cabs	$$class\mathrm{abs}$$
11	3 10	cfv	$$class\left|n\right|$$
12	8 11 9	co	$$class{\log }_2\left|n\right|$$
13	12 7	cfv	$$class⌊{\log }_2\left|n\right|⌋$$
14		caddc	$$class+$$
15	13 6 14	co	$$class\left(⌊{\log }_2\left|n\right|⌋+1\right)$$
16	5 6 15	cif	$$classif\left(n=0,1,⌊{\log }_2\left|n\right|⌋+1\right)$$
17	1 2 16	cmpt	$$class\left(n\in \mathrm{V}⟼if\left(n=0,1,⌊{\log }_2\left|n\right|⌋+1\right)\right)$$
18	0 17	wceq