Theorem blennn

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

	Ref	Expression
Assertion	blennn

Proof

Step	Hyp	Ref	Expression
1		nnne0	$$⊢N\in \mathbb{N}\to N\ne 0$$
2		blenn0
3	1 2	mpdan
4		nnre	$$⊢N\in \mathbb{N}\to N\in ℝ$$
5		nnnn0	$$⊢N\in \mathbb{N}\to N\in {\mathbb{N}}_0$$
6	5	nn0ge0d	$$⊢N\in \mathbb{N}\to 0\le N$$
7	4 6	absidd	$$⊢N\in \mathbb{N}\to \left|N\right|=N$$
8	7	oveq2d	$$⊢N\in \mathbb{N}\to {\log }_2\left|N\right|={\log }_{2}N$$
9	8	fveq2d	$$⊢N\in \mathbb{N}\to ⌊{\log }_2\left|N\right|⌋=⌊{\log }_{2}N⌋$$
10	9	oveq1d	$$⊢N\in \mathbb{N}\to ⌊{\log }_2\left|N\right|⌋+1=⌊{\log }_{2}N⌋+1$$
11	3 10	eqtrd