Theorem blenpw2m1

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

	Ref	Expression
Assertion	blenpw2m1	|- ( I e. NN -> ( #b ` ( ( 2 ^ I ) - 1 ) ) = I )

Proof

Step	Hyp	Ref	Expression
1		2nn0	|- 2 e. NN0
2	1	a1i	|- ( I e. NN -> 2 e. NN0 )
3		nnnn0	|- ( I e. NN -> I e. NN0 )
4	2 3	nn0expcld	|- ( I e. NN -> ( 2 ^ I ) e. NN0 )
5		nnge1	|- ( I e. NN -> 1 <_ I )
6		2cnd	|- ( I e. NN -> 2 e. CC )
7	6	exp1d	|- ( I e. NN -> ( 2 ^ 1 ) = 2 )
8	7	eqcomd	|- ( I e. NN -> 2 = ( 2 ^ 1 ) )
9	8	breq1d	|- ( I e. NN -> ( 2 <_ ( 2 ^ I ) <-> ( 2 ^ 1 ) <_ ( 2 ^ I ) ) )
10		2re	|- 2 e. RR
11	10	a1i	|- ( I e. NN -> 2 e. RR )
12		1zzd	|- ( I e. NN -> 1 e. ZZ )
13		nnz	|- ( I e. NN -> I e. ZZ )
14		1lt2	|- 1 < 2
15	14	a1i	|- ( I e. NN -> 1 < 2 )
16	11 12 13 15	leexp2d	|- ( I e. NN -> ( 1 <_ I <-> ( 2 ^ 1 ) <_ ( 2 ^ I ) ) )
17	9 16	bitr4d	|- ( I e. NN -> ( 2 <_ ( 2 ^ I ) <-> 1 <_ I ) )
18	5 17	mpbird	|- ( I e. NN -> 2 <_ ( 2 ^ I ) )
19		nn0ge2m1nn	|- ( ( ( 2 ^ I ) e. NN0 /\ 2 <_ ( 2 ^ I ) ) -> ( ( 2 ^ I ) - 1 ) e. NN )
20	4 18 19	syl2anc	|- ( I e. NN -> ( ( 2 ^ I ) - 1 ) e. NN )
21		blennn	|- ( ( ( 2 ^ I ) - 1 ) e. NN -> ( #b ` ( ( 2 ^ I ) - 1 ) ) = ( ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) + 1 ) )
22	20 21	syl	|- ( I e. NN -> ( #b ` ( ( 2 ^ I ) - 1 ) ) = ( ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) + 1 ) )
23		logbpw2m1	|- ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) = ( I - 1 ) )
24	23	oveq1d	|- ( I e. NN -> ( ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) + 1 ) = ( ( I - 1 ) + 1 ) )
25		nncn	|- ( I e. NN -> I e. CC )
26		npcan1	|- ( I e. CC -> ( ( I - 1 ) + 1 ) = I )
27	25 26	syl	|- ( I e. NN -> ( ( I - 1 ) + 1 ) = I )
28	22 24 27	3eqtrd	|- ( I e. NN -> ( #b ` ( ( 2 ^ I ) - 1 ) ) = I )