| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fzonel 13714 | . . . . . . 7
⊢  ¬
𝑁 ∈ (0..^𝑁) | 
| 2 | 1 | a1i 11 | . . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ¬ 𝑁 ∈ (0..^𝑁)) | 
| 3 |  | disjsn 4710 | . . . . . 6
⊢
(((0..^𝑁) ∩
{𝑁}) = ∅ ↔ ¬
𝑁 ∈ (0..^𝑁)) | 
| 4 | 2, 3 | sylibr 234 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ((0..^𝑁) ∩ {𝑁}) = ∅) | 
| 5 | 4 | ineq2d 4219 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ ((0..^𝑁) ∩ {𝑁})) = (𝐴 ∩ ∅)) | 
| 6 |  | inindi 4234 | . . . 4
⊢ (𝐴 ∩ ((0..^𝑁) ∩ {𝑁})) = ((𝐴 ∩ (0..^𝑁)) ∩ (𝐴 ∩ {𝑁})) | 
| 7 |  | in0 4394 | . . . 4
⊢ (𝐴 ∩ ∅) =
∅ | 
| 8 | 5, 6, 7 | 3eqtr3g 2799 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝐴 ∩ (0..^𝑁)) ∩ (𝐴 ∩ {𝑁})) = ∅) | 
| 9 |  | simpr 484 | . . . . . . 7
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) | 
| 10 |  | nn0uz 12921 | . . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) | 
| 11 | 9, 10 | eleqtrdi 2850 | . . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
(ℤ≥‘0)) | 
| 12 |  | fzosplitsn 13815 | . . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) | 
| 13 | 11, 12 | syl 17 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) | 
| 14 | 13 | ineq2d 4219 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) = (𝐴 ∩ ((0..^𝑁) ∪ {𝑁}))) | 
| 15 |  | indi 4283 | . . . 4
⊢ (𝐴 ∩ ((0..^𝑁) ∪ {𝑁})) = ((𝐴 ∩ (0..^𝑁)) ∪ (𝐴 ∩ {𝑁})) | 
| 16 | 14, 15 | eqtrdi 2792 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) = ((𝐴 ∩ (0..^𝑁)) ∪ (𝐴 ∩ {𝑁}))) | 
| 17 |  | fzofi 14016 | . . . . 5
⊢
(0..^(𝑁 + 1)) ∈
Fin | 
| 18 | 17 | a1i 11 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^(𝑁 + 1)) ∈ Fin) | 
| 19 |  | inss2 4237 | . . . 4
⊢ (𝐴 ∩ (0..^(𝑁 + 1))) ⊆ (0..^(𝑁 + 1)) | 
| 20 |  | ssfi 9214 | . . . 4
⊢
(((0..^(𝑁 + 1))
∈ Fin ∧ (𝐴 ∩
(0..^(𝑁 + 1))) ⊆
(0..^(𝑁 + 1))) →
(𝐴 ∩ (0..^(𝑁 + 1))) ∈
Fin) | 
| 21 | 18, 19, 20 | sylancl 586 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) ∈ Fin) | 
| 22 |  | 2nn 12340 | . . . . . 6
⊢ 2 ∈
ℕ | 
| 23 | 22 | a1i 11 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → 2 ∈
ℕ) | 
| 24 |  | inss1 4236 | . . . . . . 7
⊢ (𝐴 ∩ (0..^(𝑁 + 1))) ⊆ 𝐴 | 
| 25 |  | simpl 482 | . . . . . . 7
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝐴 ⊆
ℕ0) | 
| 26 | 24, 25 | sstrid 3994 | . . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) ⊆
ℕ0) | 
| 27 | 26 | sselda 3982 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → 𝑘 ∈ ℕ0) | 
| 28 | 23, 27 | nnexpcld 14285 | . . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → (2↑𝑘) ∈ ℕ) | 
| 29 | 28 | nncnd 12283 | . . 3
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → (2↑𝑘) ∈ ℂ) | 
| 30 | 8, 16, 21, 29 | fsumsplit 15778 | . 2
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → Σ𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))(2↑𝑘) = (Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘) + Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘))) | 
| 31 |  | elfpw 9395 | . . . 4
⊢ ((𝐴 ∩ (0..^(𝑁 + 1))) ∈ (𝒫
ℕ0 ∩ Fin) ↔ ((𝐴 ∩ (0..^(𝑁 + 1))) ⊆ ℕ0 ∧
(𝐴 ∩ (0..^(𝑁 + 1))) ∈
Fin)) | 
| 32 | 26, 21, 31 | sylanbrc 583 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) ∈ (𝒫
ℕ0 ∩ Fin)) | 
| 33 |  | bitsinv.k | . . . 4
⊢ 𝐾 = ◡(bits ↾
ℕ0) | 
| 34 | 33 | bitsinv 16486 | . . 3
⊢ ((𝐴 ∩ (0..^(𝑁 + 1))) ∈ (𝒫
ℕ0 ∩ Fin) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = Σ𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))(2↑𝑘)) | 
| 35 | 32, 34 | syl 17 | . 2
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = Σ𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))(2↑𝑘)) | 
| 36 |  | inss1 4236 | . . . . . 6
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴 | 
| 37 | 36, 25 | sstrid 3994 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^𝑁)) ⊆
ℕ0) | 
| 38 |  | fzofi 14016 | . . . . . . 7
⊢
(0..^𝑁) ∈
Fin | 
| 39 | 38 | a1i 11 | . . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^𝑁) ∈ Fin) | 
| 40 |  | inss2 4237 | . . . . . 6
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁) | 
| 41 |  | ssfi 9214 | . . . . . 6
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) | 
| 42 | 39, 40, 41 | sylancl 586 | . . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) | 
| 43 |  | elfpw 9395 | . . . . 5
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐴 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin)) | 
| 44 | 37, 42, 43 | sylanbrc 583 | . . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) | 
| 45 | 33 | bitsinv 16486 | . . . 4
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) = Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘)) | 
| 46 | 44, 45 | syl 17 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^𝑁))) = Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘)) | 
| 47 |  | snssi 4807 | . . . . . . . 8
⊢ (𝑁 ∈ 𝐴 → {𝑁} ⊆ 𝐴) | 
| 48 | 47 | adantl 481 | . . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → {𝑁} ⊆ 𝐴) | 
| 49 |  | sseqin2 4222 | . . . . . . 7
⊢ ({𝑁} ⊆ 𝐴 ↔ (𝐴 ∩ {𝑁}) = {𝑁}) | 
| 50 | 48, 49 | sylib 218 | . . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (𝐴 ∩ {𝑁}) = {𝑁}) | 
| 51 | 50 | sumeq1d 15737 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘) = Σ𝑘 ∈ {𝑁} (2↑𝑘)) | 
| 52 |  | simpr 484 | . . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈ 𝐴) | 
| 53 | 22 | a1i 11 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → 2 ∈ ℕ) | 
| 54 |  | simplr 768 | . . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈
ℕ0) | 
| 55 | 53, 54 | nnexpcld 14285 | . . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈ ℕ) | 
| 56 | 55 | nncnd 12283 | . . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈ ℂ) | 
| 57 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑘 = 𝑁 → (2↑𝑘) = (2↑𝑁)) | 
| 58 | 57 | sumsn 15783 | . . . . . 6
⊢ ((𝑁 ∈ 𝐴 ∧ (2↑𝑁) ∈ ℂ) → Σ𝑘 ∈ {𝑁} (2↑𝑘) = (2↑𝑁)) | 
| 59 | 52, 56, 58 | syl2anc 584 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → Σ𝑘 ∈ {𝑁} (2↑𝑘) = (2↑𝑁)) | 
| 60 | 51, 59 | eqtr2d 2777 | . . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) = Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘)) | 
| 61 |  | simpr 484 | . . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → ¬ 𝑁 ∈ 𝐴) | 
| 62 |  | disjsn 4710 | . . . . . . 7
⊢ ((𝐴 ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ 𝐴) | 
| 63 | 61, 62 | sylibr 234 | . . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → (𝐴 ∩ {𝑁}) = ∅) | 
| 64 | 63 | sumeq1d 15737 | . . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘) = Σ𝑘 ∈ ∅ (2↑𝑘)) | 
| 65 |  | sum0 15758 | . . . . 5
⊢
Σ𝑘 ∈
∅ (2↑𝑘) =
0 | 
| 66 | 64, 65 | eqtr2di 2793 | . . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → 0 = Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘)) | 
| 67 | 60, 66 | ifeqda 4561 | . . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘)) | 
| 68 | 46, 67 | oveq12d 7450 | . 2
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) = (Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘) + Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘))) | 
| 69 | 30, 35, 68 | 3eqtr4d 2786 | 1
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) |