Theorem 2ebits

Description: The bits of a power of two. (Contributed by Mario Carneiro, 5-Sep-2016)

	Ref	Expression
Assertion	2ebits	|- ( N e. NN0 -> ( bits ` ( 2 ^ N ) ) = { N } )

Proof

Step	Hyp	Ref	Expression
1		2nn	|- 2 e. NN
2	1	a1i	|- ( N e. NN0 -> 2 e. NN )
3		id	|- ( N e. NN0 -> N e. NN0 )
4	2 3	nnexpcld	|- ( N e. NN0 -> ( 2 ^ N ) e. NN )
5	4	nncnd	|- ( N e. NN0 -> ( 2 ^ N ) e. CC )
6		oveq2	|- ( k = N -> ( 2 ^ k ) = ( 2 ^ N ) )
7	6	sumsn	|- ( ( N e. NN0 /\ ( 2 ^ N ) e. CC ) -> sum_ k e. { N } ( 2 ^ k ) = ( 2 ^ N ) )
8	5 7	mpdan	|- ( N e. NN0 -> sum_ k e. { N } ( 2 ^ k ) = ( 2 ^ N ) )
9	8	fveq2d	|- ( N e. NN0 -> ( bits ` sum_ k e. { N } ( 2 ^ k ) ) = ( bits ` ( 2 ^ N ) ) )
10		snssi	|- ( N e. NN0 -> { N } C_ NN0 )
11		snfi	|- { N } e. Fin
12		elfpw	|- ( { N } e. ( ~P NN0 i^i Fin ) <-> ( { N } C_ NN0 /\ { N } e. Fin ) )
13	10 11 12	sylanblrc	|- ( N e. NN0 -> { N } e. ( ~P NN0 i^i Fin ) )
14		bitsinv2	|- ( { N } e. ( ~P NN0 i^i Fin ) -> ( bits ` sum_ k e. { N } ( 2 ^ k ) ) = { N } )
15	13 14	syl	|- ( N e. NN0 -> ( bits ` sum_ k e. { N } ( 2 ^ k ) ) = { N } )
16	9 15	eqtr3d	|- ( N e. NN0 -> ( bits ` ( 2 ^ N ) ) = { N } )