Definition df-blen 44623

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 𝑛 ∈ ℤ or even for 𝑛 ∈ ℂ. (Contributed by AV, 16-May-2020.)

Assertion

Ref	Expression
df-blen	⊢ #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))

Detailed syntax breakdown of Definition df-blen

Step	Hyp	Ref	Expression
1		cblen 44622	. 2 class #b
2		vn	. . 3 setvar 𝑛
3		cvv 3495	. . 3 class V
4	2	cv 1532	. . . . 5 class 𝑛
5		cc0 10531	. . . . 5 class 0
6	4, 5	wceq 1533	. . . 4 wff 𝑛 = 0
7		c1 10532	. . . 4 class 1
8		c2 11686	. . . . . . 7 class 2
9		cabs 14587	. . . . . . . 8 class abs
10	4, 9	cfv 6350	. . . . . . 7 class (abs‘𝑛)
11		clogb 25336	. . . . . . 7 class logb
12	8, 10, 11	co 7150	. . . . . 6 class (2 logb (abs‘𝑛))
13		cfl 13154	. . . . . 6 class ⌊
14	12, 13	cfv 6350	. . . . 5 class (⌊‘(2 logb (abs‘𝑛)))
15		caddc 10534	. . . . 5 class +
16	14, 7, 15	co 7150	. . . 4 class ((⌊‘(2 logb (abs‘𝑛))) + 1)
17	6, 7, 16	cif 4467	. . 3 class if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1))
18	2, 3, 17	cmpt 5139	. 2 class (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))
19	1, 18	wceq 1533	1 wff #b = (𝑛 ∈ V ↦ if(𝑛 = 0, 1, ((⌊‘(2 logb (abs‘𝑛))) + 1)))

This definition is referenced by:  blenval  44624