Metamath Proof Explorer


Theorem blengt1fldiv2p1

Description: The binary length of an integer greater than 1 is the binary length of the integer divided by 2, increased by one. (Contributed by AV, 3-Jun-2020)

Ref Expression
Assertion blengt1fldiv2p1 N 2 # b N = # b N 2 + 1

Proof

Step Hyp Ref Expression
1 eluz2nn N 2 N
2 nneop N N 2 N + 1 2
3 1 2 syl N 2 N 2 N + 1 2
4 nnnn0 N 2 N 2 0
5 blennn0em1 N N 2 0 # b N 2 = # b N 1
6 4 5 sylan2 N N 2 # b N 2 = # b N 1
7 6 ancoms N 2 N # b N 2 = # b N 1
8 7 oveq1d N 2 N # b N 2 + 1 = # b N - 1 + 1
9 nnz N 2 N 2
10 flid N 2 N 2 = N 2
11 9 10 syl N 2 N 2 = N 2
12 11 eqcomd N 2 N 2 = N 2
13 12 fveq2d N 2 # b N 2 = # b N 2
14 13 oveq1d N 2 # b N 2 + 1 = # b N 2 + 1
15 14 adantr N 2 N # b N 2 + 1 = # b N 2 + 1
16 blennnelnn N # b N
17 16 nncnd N # b N
18 npcan1 # b N # b N - 1 + 1 = # b N
19 17 18 syl N # b N - 1 + 1 = # b N
20 19 adantl N 2 N # b N - 1 + 1 = # b N
21 8 15 20 3eqtr3rd N 2 N # b N = # b N 2 + 1
22 21 expcom N N 2 # b N = # b N 2 + 1
23 22 1 syl11 N 2 N 2 # b N = # b N 2 + 1
24 nnnn0 N + 1 2 N + 1 2 0
25 blennngt2o2 N 2 N + 1 2 0 # b N = # b N 1 2 + 1
26 24 25 sylan2 N 2 N + 1 2 # b N = # b N 1 2 + 1
27 26 ancoms N + 1 2 N 2 # b N = # b N 1 2 + 1
28 eluzge2nn0 N 2 N 0
29 nn0ofldiv2 N 0 N + 1 2 0 N 2 = N 1 2
30 28 24 29 syl2anr N + 1 2 N 2 N 2 = N 1 2
31 30 eqcomd N + 1 2 N 2 N 1 2 = N 2
32 31 fveq2d N + 1 2 N 2 # b N 1 2 = # b N 2
33 32 oveq1d N + 1 2 N 2 # b N 1 2 + 1 = # b N 2 + 1
34 27 33 eqtrd N + 1 2 N 2 # b N = # b N 2 + 1
35 34 ex N + 1 2 N 2 # b N = # b N 2 + 1
36 23 35 jaoi N 2 N + 1 2 N 2 # b N = # b N 2 + 1
37 3 36 mpcom N 2 # b N = # b N 2 + 1