Metamath Proof Explorer


Theorem blen0

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

Ref Expression
Assertion blen0 ( #b ‘ 0 ) = 1

Proof

Step Hyp Ref Expression
1 c0ex 0 ∈ V
2 blenval ( 0 ∈ V → ( #b ‘ 0 ) = if ( 0 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 0 ) ) ) + 1 ) ) )
3 1 2 ax-mp ( #b ‘ 0 ) = if ( 0 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 0 ) ) ) + 1 ) )
4 eqid 0 = 0
5 4 iftruei if ( 0 = 0 , 1 , ( ( ⌊ ‘ ( 2 logb ( abs ‘ 0 ) ) ) + 1 ) ) = 1
6 3 5 eqtri ( #b ‘ 0 ) = 1