Proof of Theorem incexc2
Step | Hyp | Ref
| Expression |
1 | | incexc 14408 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) |
2 | | hashcl 13009 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
3 | 2 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (#‘𝐴) ∈
ℕ0) |
4 | 3 | nn0zd 11356 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (#‘𝐴) ∈
ℤ) |
5 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
6 | | elpwi 4117 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝒫 𝐴 → 𝑘 ⊆ 𝐴) |
7 | | ssdomg 7887 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝑘 ⊆ 𝐴 → 𝑘 ≼ 𝐴)) |
8 | 7 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ≼ 𝐴) |
9 | 5, 6, 8 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ≼ 𝐴) |
10 | | hashdomi 13030 |
. . . . . . . . . . 11
⊢ (𝑘 ≼ 𝐴 → (#‘𝑘) ≤ (#‘𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (#‘𝑘) ≤ (#‘𝐴)) |
12 | | fznn 12278 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝑘)
∈ (1...(#‘𝐴))
↔ ((#‘𝑘) ∈
ℕ ∧ (#‘𝑘)
≤ (#‘𝐴)))) |
13 | 12 | rbaibd 947 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝑘)
≤ (#‘𝐴)) →
((#‘𝑘) ∈
(1...(#‘𝐴)) ↔
(#‘𝑘) ∈
ℕ)) |
14 | 4, 11, 13 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((#‘𝑘) ∈ (1...(#‘𝐴)) ↔ (#‘𝑘) ∈
ℕ)) |
15 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ∈ Fin) |
16 | 5, 6, 15 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ∈ Fin) |
17 | | hashnncl 13018 |
. . . . . . . . . 10
⊢ (𝑘 ∈ Fin →
((#‘𝑘) ∈ ℕ
↔ 𝑘 ≠
∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((#‘𝑘) ∈ ℕ ↔ 𝑘 ≠ ∅)) |
19 | 14, 18 | bitr2d 268 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (𝑘 ≠ ∅ ↔ (#‘𝑘) ∈ (1...(#‘𝐴)))) |
20 | | df-ne 2782 |
. . . . . . . 8
⊢ (𝑘 ≠ ∅ ↔ ¬ 𝑘 = ∅) |
21 | | risset 3044 |
. . . . . . . 8
⊢
((#‘𝑘) ∈
(1...(#‘𝐴)) ↔
∃𝑛 ∈
(1...(#‘𝐴))𝑛 = (#‘𝑘)) |
22 | 19, 20, 21 | 3bitr3g 301 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 = ∅ ↔ ∃𝑛 ∈ (1...(#‘𝐴))𝑛 = (#‘𝑘))) |
23 | | velsn 4141 |
. . . . . . . 8
⊢ (𝑘 ∈ {∅} ↔ 𝑘 = ∅) |
24 | 23 | notbii 309 |
. . . . . . 7
⊢ (¬
𝑘 ∈ {∅} ↔
¬ 𝑘 =
∅) |
25 | | eqcom 2617 |
. . . . . . . 8
⊢
((#‘𝑘) = 𝑛 ↔ 𝑛 = (#‘𝑘)) |
26 | 25 | rexbii 3023 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1...(#‘𝐴))(#‘𝑘) = 𝑛 ↔ ∃𝑛 ∈ (1...(#‘𝐴))𝑛 = (#‘𝑘)) |
27 | 22, 24, 26 | 3bitr4g 302 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 ∈ {∅} ↔
∃𝑛 ∈
(1...(#‘𝐴))(#‘𝑘) = 𝑛)) |
28 | 27 | rabbidva 3163 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → {𝑘 ∈ 𝒫 𝐴 ∣ ¬ 𝑘 ∈ {∅}} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈ (1...(#‘𝐴))(#‘𝑘) = 𝑛}) |
29 | | dfdif2 3549 |
. . . . 5
⊢
(𝒫 𝐴 ∖
{∅}) = {𝑘 ∈
𝒫 𝐴 ∣ ¬
𝑘 ∈
{∅}} |
30 | | iunrab 4503 |
. . . . 5
⊢ ∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈ (1...(#‘𝐴))(#‘𝑘) = 𝑛} |
31 | 28, 29, 30 | 3eqtr4g 2669 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) =
∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) |
32 | 31 | sumeq1d 14279 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
33 | 1, 32 | eqtrd 2644 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ ∪
𝑛 ∈
(1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
34 | | fzfid 12634 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(1...(#‘𝐴)) ∈
Fin) |
35 | | simpll 786 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 𝐴 ∈ Fin) |
36 | | pwfi 8144 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
37 | 35, 36 | sylib 207 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 𝒫 𝐴 ∈ Fin) |
38 | | ssrab2 3650 |
. . . 4
⊢ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ⊆ 𝒫 𝐴 |
39 | | ssfi 8065 |
. . . 4
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑘 ∈
𝒫 𝐴 ∣
(#‘𝑘) = 𝑛} ⊆ 𝒫 𝐴) → {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ∈ Fin) |
40 | 37, 38, 39 | sylancl 693 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ∈ Fin) |
41 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑠 → (#‘𝑘) = (#‘𝑠)) |
42 | 41 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑘 = 𝑠 → ((#‘𝑘) = 𝑛 ↔ (#‘𝑠) = 𝑛)) |
43 | 42 | elrab 3331 |
. . . . . . . 8
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ↔ (𝑠 ∈ 𝒫 𝐴 ∧ (#‘𝑠) = 𝑛)) |
44 | 43 | simprbi 479 |
. . . . . . 7
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} → (#‘𝑠) = 𝑛) |
45 | 44 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘𝑠) = 𝑛) |
46 | 45 | ralrimiva 2949 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → ∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘𝑠) = 𝑛) |
47 | 46 | ralrimiva 2949 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
∀𝑛 ∈
(1...(#‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘𝑠) = 𝑛) |
48 | | invdisj 4571 |
. . . 4
⊢
(∀𝑛 ∈
(1...(#‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘𝑠) = 𝑛 → Disj 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) |
49 | 47, 48 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj
𝑛 ∈
(1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) |
50 | 45 | oveq1d 6564 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((#‘𝑠) − 1) = (𝑛 − 1)) |
51 | 50 | oveq2d 6565 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (-1↑((#‘𝑠) − 1)) = (-1↑(𝑛 − 1))) |
52 | 51 | oveq1d 6564 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠)) = ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))) |
53 | | 1cnd 9935 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 1 ∈
ℂ) |
54 | 53 | negcld 10258 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → -1 ∈
ℂ) |
55 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(#‘𝐴)) → 𝑛 ∈ ℕ) |
56 | 55 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 𝑛 ∈ ℕ) |
57 | | nnm1nn0 11211 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
58 | 56, 57 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → (𝑛 − 1) ∈
ℕ0) |
59 | 54, 58 | expcld 12870 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → (-1↑(𝑛 − 1)) ∈
ℂ) |
60 | 59 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (-1↑(𝑛 − 1)) ∈ ℂ) |
61 | | unifi 8138 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
62 | 61 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∪ 𝐴 ∈ Fin) |
63 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑛 ∈ ℕ) |
64 | 45, 63 | eqeltrd 2688 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘𝑠) ∈ ℕ) |
65 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝐴 ∈ Fin) |
66 | | elrabi 3328 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} → 𝑠 ∈ 𝒫 𝐴) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ∈ 𝒫 𝐴) |
68 | | elpwi 4117 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ⊆ 𝐴) |
70 | | ssfi 8065 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin) |
71 | 65, 69, 70 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ∈ Fin) |
72 | | hashnncl 13018 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((#‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅)) |
74 | 64, 73 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ≠ ∅) |
75 | | intssuni 4434 |
. . . . . . . . . . 11
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝑠) |
77 | 69 | unissd 4398 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∪ 𝑠 ⊆ ∪ 𝐴) |
78 | 76, 77 | sstrd 3578 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝐴) |
79 | | ssfi 8065 |
. . . . . . . . 9
⊢ ((∪ 𝐴
∈ Fin ∧ ∩ 𝑠 ⊆ ∪ 𝐴) → ∩ 𝑠
∈ Fin) |
80 | 62, 78, 79 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∩ 𝑠 ∈ Fin) |
81 | | hashcl 13009 |
. . . . . . . 8
⊢ (∩ 𝑠
∈ Fin → (#‘∩ 𝑠) ∈
ℕ0) |
82 | 80, 81 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘∩ 𝑠)
∈ ℕ0) |
83 | 82 | nn0cnd 11230 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘∩ 𝑠)
∈ ℂ) |
84 | 60, 83 | mulcld 9939 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))
∈ ℂ) |
85 | 52, 84 | eqeltrd 2688 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠)) ∈ ℂ) |
86 | 85 | anasss 677 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ (𝑛 ∈ (1...(#‘𝐴)) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛})) → ((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠)) ∈ ℂ) |
87 | 34, 40, 49, 86 | fsumiun 14394 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑛 ∈
(1...(#‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
88 | 52 | sumeq2dv 14281 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))) |
89 | 40, 59, 83 | fsummulc2 14358 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → ((-1↑(𝑛 − 1)) ·
Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠)) = Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))) |
90 | 88, 89 | eqtr4d 2647 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= ((-1↑(𝑛 − 1))
· Σ𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠))) |
91 | 90 | sumeq2dv 14281 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑛 ∈
(1...(#‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑛 ∈
(1...(#‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠))) |
92 | 33, 87, 91 | 3eqtrd 2648 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑛 ∈ (1...(#‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠))) |