Metamath Proof Explorer


Theorem blennn

Description: The binary length of a positive integer. (Contributed by AV, 21-May-2020)

Ref Expression
Assertion blennn N # b N = log 2 N + 1

Proof

Step Hyp Ref Expression
1 nnne0 N N 0
2 blenn0 N N 0 # b N = log 2 N + 1
3 1 2 mpdan N # b N = log 2 N + 1
4 nnre N N
5 nnnn0 N N 0
6 5 nn0ge0d N 0 N
7 4 6 absidd N N = N
8 7 oveq2d N log 2 N = log 2 N
9 8 fveq2d N log 2 N = log 2 N
10 9 oveq1d N log 2 N + 1 = log 2 N + 1
11 3 10 eqtrd N # b N = log 2 N + 1