Metamath Proof Explorer


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 ↑ 𝑁 ) ) = { 𝑁 } )