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 e. NN0 -> ( #b ` N ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		elnn0	|- ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2		blennnelnn	|- ( N e. NN -> ( #b ` N ) e. NN )
3		fveq2	|- ( N = 0 -> ( #b ` N ) = ( #b ` 0 ) )
4		blen0	|- ( #b ` 0 ) = 1
5		1nn	|- 1 e. NN
6	4 5	eqeltri	|- ( #b ` 0 ) e. NN
7	3 6	eqeltrdi	|- ( N = 0 -> ( #b ` N ) e. NN )
8	2 7	jaoi	|- ( ( N e. NN \/ N = 0 ) -> ( #b ` N ) e. NN )
9	1 8	sylbi	|- ( N e. NN0 -> ( #b ` N ) e. NN )