Metamath Proof Explorer


Theorem blennn0elnn

Description: The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020)

Ref Expression
Assertion blennn0elnn ( 𝑁 ∈ ℕ0 → ( #b𝑁 ) ∈ ℕ )

Proof

Step Hyp Ref Expression
1 elnn0 ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2 blennnelnn ( 𝑁 ∈ ℕ → ( #b𝑁 ) ∈ ℕ )
3 fveq2 ( 𝑁 = 0 → ( #b𝑁 ) = ( #b ‘ 0 ) )
4 blen0 ( #b ‘ 0 ) = 1
5 1nn 1 ∈ ℕ
6 4 5 eqeltri ( #b ‘ 0 ) ∈ ℕ
7 3 6 eqeltrdi ( 𝑁 = 0 → ( #b𝑁 ) ∈ ℕ )
8 2 7 jaoi ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( #b𝑁 ) ∈ ℕ )
9 1 8 sylbi ( 𝑁 ∈ ℕ0 → ( #b𝑁 ) ∈ ℕ )