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 log 2 0 + 1
3 1 2 ax-mp ⊢ # b ⁡ 0 = if 0 = 0 1 log 2 0 + 1
4 eqid ⊢ 0 = 0
5 4 iftruei ⊢ if 0 = 0 1 log 2 0 + 1 = 1
6 3 5 eqtri ⊢ # b ⁡ 0 = 1