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