Theorem blenpw2

Description: The binary length of a power of 2 is the exponent plus 1. (Contributed by AV, 30-May-2020)

	Ref	Expression
Assertion	blenpw2	|- ( I e. NN0 -> ( #b ` ( 2 ^ I ) ) = ( I + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn	|- 2 e. NN
2		nnexpcl	|- ( ( 2 e. NN /\ I e. NN0 ) -> ( 2 ^ I ) e. NN )
3	1 2	mpan	|- ( I e. NN0 -> ( 2 ^ I ) e. NN )
4		blennn	|- ( ( 2 ^ I ) e. NN -> ( #b ` ( 2 ^ I ) ) = ( ( |_ ` ( 2 logb ( 2 ^ I ) ) ) + 1 ) )
5	3 4	syl	|- ( I e. NN0 -> ( #b ` ( 2 ^ I ) ) = ( ( |_ ` ( 2 logb ( 2 ^ I ) ) ) + 1 ) )
6		2z	|- 2 e. ZZ
7		uzid	|- ( 2 e. ZZ -> 2 e. ( ZZ>= ` 2 ) )
8	6 7	mp1i	|- ( I e. NN0 -> 2 e. ( ZZ>= ` 2 ) )
9		nn0z	|- ( I e. NN0 -> I e. ZZ )
10		nnlogbexp	|- ( ( 2 e. ( ZZ>= ` 2 ) /\ I e. ZZ ) -> ( 2 logb ( 2 ^ I ) ) = I )
11	8 9 10	syl2anc	|- ( I e. NN0 -> ( 2 logb ( 2 ^ I ) ) = I )
12	11	fveq2d	|- ( I e. NN0 -> ( |_ ` ( 2 logb ( 2 ^ I ) ) ) = ( |_ ` I ) )
13		flid	|- ( I e. ZZ -> ( |_ ` I ) = I )
14	9 13	syl	|- ( I e. NN0 -> ( |_ ` I ) = I )
15	12 14	eqtrd	|- ( I e. NN0 -> ( |_ ` ( 2 logb ( 2 ^ I ) ) ) = I )
16	15	oveq1d	|- ( I e. NN0 -> ( ( |_ ` ( 2 logb ( 2 ^ I ) ) ) + 1 ) = ( I + 1 ) )
17	5 16	eqtrd	|- ( I e. NN0 -> ( #b ` ( 2 ^ I ) ) = ( I + 1 ) )