Step | Hyp | Ref
| Expression |
1 | | fzonel 13256 |
. . . . . . 7
⊢ ¬
𝑁 ∈ (0..^𝑁) |
2 | 1 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ¬ 𝑁 ∈ (0..^𝑁)) |
3 | | disjsn 4627 |
. . . . . 6
⊢
(((0..^𝑁) ∩
{𝑁}) = ∅ ↔ ¬
𝑁 ∈ (0..^𝑁)) |
4 | 2, 3 | sylibr 237 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ((0..^𝑁) ∩ {𝑁}) = ∅) |
5 | 4 | ineq2d 4127 |
. . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ ((0..^𝑁) ∩ {𝑁})) = (𝐴 ∩ ∅)) |
6 | | inindi 4141 |
. . . 4
⊢ (𝐴 ∩ ((0..^𝑁) ∩ {𝑁})) = ((𝐴 ∩ (0..^𝑁)) ∩ (𝐴 ∩ {𝑁})) |
7 | | in0 4306 |
. . . 4
⊢ (𝐴 ∩ ∅) =
∅ |
8 | 5, 6, 7 | 3eqtr3g 2801 |
. . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝐴 ∩ (0..^𝑁)) ∩ (𝐴 ∩ {𝑁})) = ∅) |
9 | | simpr 488 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
ℕ0) |
10 | | nn0uz 12476 |
. . . . . . 7
⊢
ℕ0 = (ℤ≥‘0) |
11 | 9, 10 | eleqtrdi 2848 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝑁 ∈
(ℤ≥‘0)) |
12 | | fzosplitsn 13350 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^(𝑁 + 1)) = ((0..^𝑁) ∪ {𝑁})) |
14 | 13 | ineq2d 4127 |
. . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) = (𝐴 ∩ ((0..^𝑁) ∪ {𝑁}))) |
15 | | indi 4188 |
. . . 4
⊢ (𝐴 ∩ ((0..^𝑁) ∪ {𝑁})) = ((𝐴 ∩ (0..^𝑁)) ∪ (𝐴 ∩ {𝑁})) |
16 | 14, 15 | eqtrdi 2794 |
. . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) = ((𝐴 ∩ (0..^𝑁)) ∪ (𝐴 ∩ {𝑁}))) |
17 | | fzofi 13547 |
. . . . 5
⊢
(0..^(𝑁 + 1)) ∈
Fin |
18 | 17 | a1i 11 |
. . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^(𝑁 + 1)) ∈ Fin) |
19 | | inss2 4144 |
. . . 4
⊢ (𝐴 ∩ (0..^(𝑁 + 1))) ⊆ (0..^(𝑁 + 1)) |
20 | | ssfi 8851 |
. . . 4
⊢
(((0..^(𝑁 + 1))
∈ Fin ∧ (𝐴 ∩
(0..^(𝑁 + 1))) ⊆
(0..^(𝑁 + 1))) →
(𝐴 ∩ (0..^(𝑁 + 1))) ∈
Fin) |
21 | 18, 19, 20 | sylancl 589 |
. . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) ∈ Fin) |
22 | | 2nn 11903 |
. . . . . 6
⊢ 2 ∈
ℕ |
23 | 22 | a1i 11 |
. . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → 2 ∈
ℕ) |
24 | | inss1 4143 |
. . . . . . 7
⊢ (𝐴 ∩ (0..^(𝑁 + 1))) ⊆ 𝐴 |
25 | | simpl 486 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → 𝐴 ⊆
ℕ0) |
26 | 24, 25 | sstrid 3912 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) ⊆
ℕ0) |
27 | 26 | sselda 3901 |
. . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → 𝑘 ∈ ℕ0) |
28 | 23, 27 | nnexpcld 13812 |
. . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → (2↑𝑘) ∈ ℕ) |
29 | 28 | nncnd 11846 |
. . 3
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))) → (2↑𝑘) ∈ ℂ) |
30 | 8, 16, 21, 29 | fsumsplit 15305 |
. 2
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → Σ𝑘 ∈ (𝐴 ∩ (0..^(𝑁 + 1)))(2↑𝑘) = (Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘) + Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘))) |
31 | | elfpw 8978 |
. . . 4
⊢ ((𝐴 ∩ (0..^(𝑁 + 1))) ∈ (𝒫
ℕ0 ∩ Fin) ↔ ((𝐴 ∩ (0..^(𝑁 + 1))) ⊆ ℕ0 ∧
(𝐴 ∩ (0..^(𝑁 + 1))) ∈
Fin)) |
32 | 26, 21, 31 | sylanbrc 586 |
. . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^(𝑁 + 1))) ∈ (𝒫
ℕ0 ∩ Fin)) |
33 | | bitsinv.k |
. . . 4
⊢ 𝐾 = ◡(bits ↾
ℕ0) |
34 | 33 | bitsinv 16007 |
. . 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 4143 |
. . . . . 6
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ 𝐴 |
37 | 36, 25 | sstrid 3912 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^𝑁)) ⊆
ℕ0) |
38 | | fzofi 13547 |
. . . . . . 7
⊢
(0..^𝑁) ∈
Fin |
39 | 38 | a1i 11 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (0..^𝑁) ∈ Fin) |
40 | | inss2 4144 |
. . . . . 6
⊢ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁) |
41 | | ssfi 8851 |
. . . . . 6
⊢
(((0..^𝑁) ∈ Fin
∧ (𝐴 ∩ (0..^𝑁)) ⊆ (0..^𝑁)) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) |
42 | 39, 40, 41 | sylancl 589 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^𝑁)) ∈ Fin) |
43 | | elfpw 8978 |
. . . . 5
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) ↔ ((𝐴 ∩
(0..^𝑁)) ⊆
ℕ0 ∧ (𝐴 ∩ (0..^𝑁)) ∈ Fin)) |
44 | 37, 42, 43 | sylanbrc 586 |
. . . 4
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin)) |
45 | 33 | bitsinv 16007 |
. . . 4
⊢ ((𝐴 ∩ (0..^𝑁)) ∈ (𝒫 ℕ0
∩ Fin) → (𝐾‘(𝐴 ∩ (0..^𝑁))) = Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘)) |
46 | 44, 45 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^𝑁))) = Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘)) |
47 | | snssi 4721 |
. . . . . . . 8
⊢ (𝑁 ∈ 𝐴 → {𝑁} ⊆ 𝐴) |
48 | 47 | adantl 485 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → {𝑁} ⊆ 𝐴) |
49 | | sseqin2 4130 |
. . . . . . 7
⊢ ({𝑁} ⊆ 𝐴 ↔ (𝐴 ∩ {𝑁}) = {𝑁}) |
50 | 48, 49 | sylib 221 |
. . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (𝐴 ∩ {𝑁}) = {𝑁}) |
51 | 50 | sumeq1d 15265 |
. . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘) = Σ𝑘 ∈ {𝑁} (2↑𝑘)) |
52 | | simpr 488 |
. . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈ 𝐴) |
53 | 22 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → 2 ∈ ℕ) |
54 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → 𝑁 ∈
ℕ0) |
55 | 53, 54 | nnexpcld 13812 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈ ℕ) |
56 | 55 | nncnd 11846 |
. . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) ∈ ℂ) |
57 | | oveq2 7221 |
. . . . . . 7
⊢ (𝑘 = 𝑁 → (2↑𝑘) = (2↑𝑁)) |
58 | 57 | sumsn 15310 |
. . . . . 6
⊢ ((𝑁 ∈ 𝐴 ∧ (2↑𝑁) ∈ ℂ) → Σ𝑘 ∈ {𝑁} (2↑𝑘) = (2↑𝑁)) |
59 | 52, 56, 58 | syl2anc 587 |
. . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → Σ𝑘 ∈ {𝑁} (2↑𝑘) = (2↑𝑁)) |
60 | 51, 59 | eqtr2d 2778 |
. . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ 𝑁 ∈ 𝐴) → (2↑𝑁) = Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘)) |
61 | | simpr 488 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → ¬ 𝑁 ∈ 𝐴) |
62 | | disjsn 4627 |
. . . . . . 7
⊢ ((𝐴 ∩ {𝑁}) = ∅ ↔ ¬ 𝑁 ∈ 𝐴) |
63 | 61, 62 | sylibr 237 |
. . . . . 6
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → (𝐴 ∩ {𝑁}) = ∅) |
64 | 63 | sumeq1d 15265 |
. . . . 5
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘) = Σ𝑘 ∈ ∅ (2↑𝑘)) |
65 | | sum0 15285 |
. . . . 5
⊢
Σ𝑘 ∈
∅ (2↑𝑘) =
0 |
66 | 64, 65 | eqtr2di 2795 |
. . . 4
⊢ (((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) ∧ ¬ 𝑁 ∈ 𝐴) → 0 = Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘)) |
67 | 60, 66 | ifeqda 4475 |
. . 3
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → if(𝑁 ∈ 𝐴, (2↑𝑁), 0) = Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘)) |
68 | 46, 67 | oveq12d 7231 |
. 2
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0)) = (Σ𝑘 ∈ (𝐴 ∩ (0..^𝑁))(2↑𝑘) + Σ𝑘 ∈ (𝐴 ∩ {𝑁})(2↑𝑘))) |
69 | 30, 35, 68 | 3eqtr4d 2787 |
1
⊢ ((𝐴 ⊆ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + if(𝑁 ∈ 𝐴, (2↑𝑁), 0))) |