Description: The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | blennn0elnn | ⊢ ( 𝑁 ∈ ℕ0 → ( #b ‘ 𝑁 ) ∈ ℕ ) |
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 ‘ 𝑁 ) ∈ ℕ ) |