Metamath Proof Explorer


Theorem blenre

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

Ref Expression
Assertion blenre ( 𝑁 ∈ ℝ+ → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 rpne0 ( 𝑁 ∈ ℝ+𝑁 ≠ 0 )
2 blenn0 ( ( 𝑁 ∈ ℝ+𝑁 ≠ 0 ) → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) )
3 1 2 mpdan ( 𝑁 ∈ ℝ+ → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) )
4 rpre ( 𝑁 ∈ ℝ+𝑁 ∈ ℝ )
5 rpge0 ( 𝑁 ∈ ℝ+ → 0 ≤ 𝑁 )
6 4 5 absidd ( 𝑁 ∈ ℝ+ → ( abs ‘ 𝑁 ) = 𝑁 )
7 6 oveq2d ( 𝑁 ∈ ℝ+ → ( 2 logb ( abs ‘ 𝑁 ) ) = ( 2 logb 𝑁 ) )
8 7 fveq2d ( 𝑁 ∈ ℝ+ → ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) = ( ⌊ ‘ ( 2 logb 𝑁 ) ) )
9 8 oveq1d ( 𝑁 ∈ ℝ+ → ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
10 3 9 eqtrd ( 𝑁 ∈ ℝ+ → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )