blennnelnn

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

		Ref	Expression
	Assertion	blennnelnn	$⊢ N \in ℕ \to #_{b(N)\inℕ}$

Step	Hyp	Ref	Expression
1		blennn	$⊢ N \in ℕ \to #_{b(N)=⌊\log_{2} N⌋ + 1}$
2		2rp	$⊢ 2 \in ℝ^{+}$
3	2	a1i	$⊢ N \in ℕ \to 2 \in ℝ^{+}$
4		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
5		1ne2	$⊢ 1 \neq 2$
6	5	necomi	$⊢ 2 \neq 1$
7	6	a1i	$⊢ N \in ℕ \to 2 \neq 1$
8		relogbcl	$⊢ (2 \in ℝ^{+} \land N \in ℝ^{+} \land 2 \neq 1) \to \log_{2} N \in ℝ$
9	3 4 7 8	syl3anc	$⊢ N \in ℕ \to \log_{2} N \in ℝ$
10		2z	$⊢ 2 \in ℤ$
11		uzid	$⊢ 2 \in ℤ \to 2 \in ℤ_{\geq 2}$
12	10 11	mp1i	$⊢ N \in ℕ \to 2 \in ℤ_{\geq 2}$
13		nnre	$⊢ N \in ℕ \to N \in ℝ$
14		nnge1	$⊢ N \in ℕ \to 1 \leq N$
15		1re	$⊢ 1 \in ℝ$
16		elicopnf	$⊢ 1 \in ℝ \to (N \in [1, +∞) \leftrightarrow (N \in ℝ \land 1 \leq N))$
17	15 16	ax-mp	$⊢ N \in [1, +∞) \leftrightarrow (N \in ℝ \land 1 \leq N)$
18	13 14 17	sylanbrc	$⊢ N \in ℕ \to N \in [1, +∞)$
19		rege1logbzge0	$⊢ (2 \in ℤ_{\geq 2} \land N \in [1, +∞)) \to 0 \leq \log_{2} N$
20	12 18 19	syl2anc	$⊢ N \in ℕ \to 0 \leq \log_{2} N$
21		flge0nn0	$⊢ (\log_{2} N \in ℝ \land 0 \leq \log_{2} N) \to ⌊\log_{2} N⌋ \in ℕ_{0}$
22	9 20 21	syl2anc	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ \in ℕ_{0}$
23		nn0p1nn	$⊢ ⌊\log_{2} N⌋ \in ℕ_{0} \to ⌊\log_{2} N⌋ + 1 \in ℕ$
24	22 23	syl	$⊢ N \in ℕ \to ⌊\log_{2} N⌋ + 1 \in ℕ$
25	1 24	eqeltrd	$⊢ N \in ℕ \to #_{b(N)\inℕ}$

Metamath Proof Explorer