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 ⊢ N ∈ V ∧ N ≠ 0 → # b ⁡ N = log 2 N + 1

Proof

Step Hyp Ref Expression
1 blenval ⊢ N ∈ V → # b ⁡ N = if N = 0 1 log 2 N + 1
2 ifnefalse ⊢ N ≠ 0 → if N = 0 1 log 2 N + 1 = log 2 N + 1
3 1 2 sylan9eq ⊢ N ∈ V ∧ N ≠ 0 → # b ⁡ N = log 2 N + 1