Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Complexity theory
Binary length
blennn
Next ⟩
blennnelnn
Metamath Proof Explorer
Ascii
Unicode
Theorem
blennn
Description:
The binary length of a positive integer.
(Contributed by
AV
, 21-May-2020)
Ref
Expression
Assertion
blennn
⊢
N
∈
ℕ
→
#
b
⁡
N
=
log
2
N
+
1
Proof
Step
Hyp
Ref
Expression
1
nnne0
⊢
N
∈
ℕ
→
N
≠
0
2
blenn0
⊢
N
∈
ℕ
∧
N
≠
0
→
#
b
⁡
N
=
log
2
N
+
1
3
1
2
mpdan
⊢
N
∈
ℕ
→
#
b
⁡
N
=
log
2
N
+
1
4
nnre
⊢
N
∈
ℕ
→
N
∈
ℝ
5
nnnn0
⊢
N
∈
ℕ
→
N
∈
ℕ
0
6
5
nn0ge0d
⊢
N
∈
ℕ
→
0
≤
N
7
4
6
absidd
⊢
N
∈
ℕ
→
N
=
N
8
7
oveq2d
⊢
N
∈
ℕ
→
log
2
N
=
log
2
N
9
8
fveq2d
⊢
N
∈
ℕ
→
log
2
N
=
log
2
N
10
9
oveq1d
⊢
N
∈
ℕ
→
log
2
N
+
1
=
log
2
N
+
1
11
3
10
eqtrd
⊢
N
∈
ℕ
→
#
b
⁡
N
=
log
2
N
+
1