Metamath Proof Explorer


Theorem blenn0

Description: The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020)

Ref Expression
Assertion blenn0 ( ( 𝑁𝑉𝑁 ≠ 0 ) → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) )

Proof

Step Hyp Ref Expression
1 blenval ( 𝑁𝑉 → ( #b𝑁 ) = if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) )
2 ifnefalse ( 𝑁 ≠ 0 → if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) = ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) )
3 1 2 sylan9eq ( ( 𝑁𝑉𝑁 ≠ 0 ) → ( #b𝑁 ) = ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) )