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