Metamath Proof Explorer

Theorem blenval

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

Ref Expression
Assertion blenval ⊢ N ∈ V → # b ⁡ N = if N = 0 1 log 2 N + 1

Proof

Step Hyp Ref Expression
1 df-blen ⊢ # b = n ∈ V ⟼ if n = 0 1 log 2 n + 1
2 eqeq1 ⊢ n = N → n = 0 ↔ N = 0
3 fveq2 ⊢ n = N → n = N
4 3 oveq2d ⊢ n = N → log 2 n = log 2 N
5 4 fveq2d ⊢ n = N → log 2 n = log 2 N
6 5 oveq1d ⊢ n = N → log 2 n + 1 = log 2 N + 1
7 2 6 ifbieq2d ⊢ n = N → if n = 0 1 log 2 n + 1 = if N = 0 1 log 2 N + 1
8 elex ⊢ N ∈ V → N ∈ V
9 1ex ⊢ 1 ∈ V
10 ovex ⊢ log 2 N + 1 ∈ V
11 9 10 ifex ⊢ if N = 0 1 log 2 N + 1 ∈ V
12 11 a1i ⊢ N ∈ V → if N = 0 1 log 2 N + 1 ∈ V
13 1 7 8 12 fvmptd3 ⊢ N ∈ V → # b ⁡ N = if N = 0 1 log 2 N + 1