blennn0elnn

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

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

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		blennnelnn	$⊢ N \in ℕ \to #_{b(N)\inℕ}$
3		fveq2	$⊢ N = 0 \to #_{b(N)=#_{b} (0)}$
4		blen0	$⊢ #_{b(0)=1}$
5		1nn	$⊢ 1 \in ℕ$
6	4 5	eqeltri	$⊢ #_{b(0)\inℕ}$
7	3 6	eqeltrdi	$⊢ N = 0 \to #_{b(N)\inℕ}$
8	2 7	jaoi	$⊢ (N \in ℕ \lor N = 0) \to #_{b(N)\inℕ}$
9	1 8	sylbi	$⊢ N \in ℕ_{0} \to #_{b(N)\inℕ}$

Metamath Proof Explorer