Theorem blenre

Description: The binary length of a positive real number. (Contributed by AV, 20-May-2020)

	Ref	Expression
Assertion	blenre

Proof

Step	Hyp	Ref	Expression
1		rpne0	$$⊢N\in {ℝ}^{+}\to N\ne 0$$
2		blenn0
3	1 2	mpdan
4		rpre	$$⊢N\in {ℝ}^{+}\to N\in ℝ$$
5		rpge0	$$⊢N\in {ℝ}^{+}\to 0\le N$$
6	4 5	absidd	$$⊢N\in {ℝ}^{+}\to \left|N\right|=N$$
7	6	oveq2d	$$⊢N\in {ℝ}^{+}\to {\log }_2\left|N\right|={\log }_{2}N$$
8	7	fveq2d	$$⊢N\in {ℝ}^{+}\to ⌊{\log }_2\left|N\right|⌋=⌊{\log }_{2}N⌋$$
9	8	oveq1d	$$⊢N\in {ℝ}^{+}\to ⌊{\log }_2\left|N\right|⌋+1=⌊{\log }_{2}N⌋+1$$
10	3 9	eqtrd