Metamath Proof Explorer


Theorem blennn0e2

Description: The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020)

Ref Expression
Assertion blennn0e2 N N 2 0 # b N = # b N 2 + 1

Proof

Step Hyp Ref Expression
1 2rp 2 +
2 1ne2 1 2
3 2 necomi 2 1
4 eldifsn 2 + 1 2 + 2 1
5 1 3 4 mpbir2an 2 + 1
6 nnrp N N +
7 6 adantr N N 2 0 N +
8 relogbdivb 2 + 1 N + log 2 N 2 = log 2 N 1
9 5 7 8 sylancr N N 2 0 log 2 N 2 = log 2 N 1
10 9 fveq2d N N 2 0 log 2 N 2 = log 2 N 1
11 10 oveq1d N N 2 0 log 2 N 2 + 1 = log 2 N 1 + 1
12 1 a1i N 2 +
13 3 a1i N 2 1
14 relogbcl 2 + N + 2 1 log 2 N
15 12 6 13 14 syl3anc N log 2 N
16 1zzd N 1
17 15 16 jca N log 2 N 1
18 17 adantr N N 2 0 log 2 N 1
19 flsubz log 2 N 1 log 2 N 1 = log 2 N 1
20 18 19 syl N N 2 0 log 2 N 1 = log 2 N 1
21 20 oveq1d N N 2 0 log 2 N 1 + 1 = log 2 N - 1 + 1
22 15 flcld N log 2 N
23 22 zcnd N log 2 N
24 npcan1 log 2 N log 2 N - 1 + 1 = log 2 N
25 23 24 syl N log 2 N - 1 + 1 = log 2 N
26 25 adantr N N 2 0 log 2 N - 1 + 1 = log 2 N
27 11 21 26 3eqtrd N N 2 0 log 2 N 2 + 1 = log 2 N
28 27 oveq1d N N 2 0 log 2 N 2 + 1 + 1 = log 2 N + 1
29 nn0enne N N 2 0 N 2
30 29 biimpa N N 2 0 N 2
31 blennn N 2 # b N 2 = log 2 N 2 + 1
32 31 oveq1d N 2 # b N 2 + 1 = log 2 N 2 + 1 + 1
33 30 32 syl N N 2 0 # b N 2 + 1 = log 2 N 2 + 1 + 1
34 blennn N # b N = log 2 N + 1
35 34 adantr N N 2 0 # b N = log 2 N + 1
36 28 33 35 3eqtr4rd N N 2 0 # b N = # b N 2 + 1