Theorem 2ebits

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

	Ref	Expression
Assertion	2ebits	⊢ ( 𝑁 ∈ ℕ0 → ( bits ‘ ( 2 ↑ 𝑁 ) ) = { 𝑁 } )

Proof

Step	Hyp	Ref	Expression
1		2nn	⊢ 2 ∈ ℕ
2	1	a1i	⊢ ( 𝑁 ∈ ℕ0 → 2 ∈ ℕ )
3		id	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℕ0 )
4	2 3	nnexpcld	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℕ )
5	4	nncnd	⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) ∈ ℂ )
6		oveq2	⊢ ( 𝑘 = 𝑁 → ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑁 ) )
7	6	sumsn	⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 2 ↑ 𝑁 ) ∈ ℂ ) → Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑁 ) )
8	5 7	mpdan	⊢ ( 𝑁 ∈ ℕ0 → Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) = ( 2 ↑ 𝑁 ) )
9	8	fveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( bits ‘ Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) ) = ( bits ‘ ( 2 ↑ 𝑁 ) ) )
10		snssi	⊢ ( 𝑁 ∈ ℕ0 → { 𝑁 } ⊆ ℕ0 )
11		snfi	⊢ { 𝑁 } ∈ Fin
12		elfpw	⊢ ( { 𝑁 } ∈ ( 𝒫 ℕ0 ∩ Fin ) ↔ ( { 𝑁 } ⊆ ℕ0 ∧ { 𝑁 } ∈ Fin ) )
13	10 11 12	sylanblrc	⊢ ( 𝑁 ∈ ℕ0 → { 𝑁 } ∈ ( 𝒫 ℕ0 ∩ Fin ) )
14		bitsinv2	⊢ ( { 𝑁 } ∈ ( 𝒫 ℕ0 ∩ Fin ) → ( bits ‘ Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) ) = { 𝑁 } )
15	13 14	syl	⊢ ( 𝑁 ∈ ℕ0 → ( bits ‘ Σ 𝑘 ∈ { 𝑁 } ( 2 ↑ 𝑘 ) ) = { 𝑁 } )
16	9 15	eqtr3d	⊢ ( 𝑁 ∈ ℕ0 → ( bits ‘ ( 2 ↑ 𝑁 ) ) = { 𝑁 } )