Theorem blennnelnn

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

	Ref	Expression
Assertion	blennnelnn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		blennn	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) = ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) )
2		2rp	⊢ 2 ∈ ℝ+
3	2	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ℝ+ )
4		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
5		1ne2	⊢ 1 ≠ 2
6	5	necomi	⊢ 2 ≠ 1
7	6	a1i	⊢ ( 𝑁 ∈ ℕ → 2 ≠ 1 )
8		relogbcl	⊢ ( ( 2 ∈ ℝ+ ∧ 𝑁 ∈ ℝ+ ∧ 2 ≠ 1 ) → ( 2 logb 𝑁 ) ∈ ℝ )
9	3 4 7 8	syl3anc	⊢ ( 𝑁 ∈ ℕ → ( 2 logb 𝑁 ) ∈ ℝ )
10		2z	⊢ 2 ∈ ℤ
11		uzid	⊢ ( 2 ∈ ℤ → 2 ∈ ( ℤ≥ ‘ 2 ) )
12	10 11	mp1i	⊢ ( 𝑁 ∈ ℕ → 2 ∈ ( ℤ≥ ‘ 2 ) )
13		nnre	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ )
14		nnge1	⊢ ( 𝑁 ∈ ℕ → 1 ≤ 𝑁 )
15		1re	⊢ 1 ∈ ℝ
16		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑁 ∈ ( 1 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 1 ≤ 𝑁 ) ) )
17	15 16	ax-mp	⊢ ( 𝑁 ∈ ( 1 [,) +∞ ) ↔ ( 𝑁 ∈ ℝ ∧ 1 ≤ 𝑁 ) )
18	13 14 17	sylanbrc	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( 1 [,) +∞ ) )
19		rege1logbzge0	⊢ ( ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑁 ∈ ( 1 [,) +∞ ) ) → 0 ≤ ( 2 logb 𝑁 ) )
20	12 18 19	syl2anc	⊢ ( 𝑁 ∈ ℕ → 0 ≤ ( 2 logb 𝑁 ) )
21		flge0nn0	⊢ ( ( ( 2 logb 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 2 logb 𝑁 ) ) → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℕ0 )
22	9 20 21	syl2anc	⊢ ( 𝑁 ∈ ℕ → ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℕ0 )
23		nn0p1nn	⊢ ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ∈ ℕ )
24	22 23	syl	⊢ ( 𝑁 ∈ ℕ → ( ( ⌊ ‘ ( 2 logb 𝑁 ) ) + 1 ) ∈ ℕ )
25	1 24	eqeltrd	⊢ ( 𝑁 ∈ ℕ → ( #b ‘ 𝑁 ) ∈ ℕ )