Metamath Proof Explorer

Theorem blenval

Description: The binary length of an integer. (Contributed by AV, 20-May-2020)

Ref Expression
Assertion blenval ( 𝑁 ∈ 𝑉 → ( #b ‘ 𝑁 ) = if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) )

Proof

Step Hyp Ref Expression
1 df-blen ⊢ #b = ( 𝑛 ∈ V ↦ if ( 𝑛 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) ) )
2 eqeq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 = 0 ↔ 𝑁 = 0 ) )
3 fveq2 ⊢ ( 𝑛 = 𝑁 → ( abs ‘ 𝑛 ) = ( abs ‘ 𝑁 ) )
4 3 oveq2d ⊢ ( 𝑛 = 𝑁 → ( 2 logb ( abs ‘ 𝑛 ) ) = ( 2 logb ( abs ‘ 𝑁 ) ) )
5 4 fveq2d ⊢ ( 𝑛 = 𝑁 → ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) = ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) )
6 5 oveq1d ⊢ ( 𝑛 = 𝑁 → ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) = ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) )
7 2 6 ifbieq2d ⊢ ( 𝑛 = 𝑁 → if ( 𝑛 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑛 ) ) ) + 1 ) ) = if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) )
8 elex ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ V )
9 1ex ⊢ 1 ∈ V
10 ovex ⊢ ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ∈ V
11 9 10 ifex ⊢ if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) ∈ V
12 11 a1i ⊢ ( 𝑁 ∈ 𝑉 → if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) ∈ V )
13 1 7 8 12 fvmptd3 ⊢ ( 𝑁 ∈ 𝑉 → ( #b ‘ 𝑁 ) = if ( 𝑁 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 𝑁 ) ) ) + 1 ) ) )