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 ⊢ N ∈ ℕ 0 → # b ⁡ N ∈ ℕ

Proof

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