Proof of Theorem incexc2
Step | Hyp | Ref
| Expression |
1 | | incexc 14613 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖ {∅})((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠))) |
2 | | hashcl 13185 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(#‘𝐴) ∈
ℕ0) |
3 | 2 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (#‘𝐴) ∈
ℕ0) |
4 | 3 | nn0zd 11518 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (#‘𝐴) ∈
ℤ) |
5 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
6 | | elpwi 4201 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝒫 𝐴 → 𝑘 ⊆ 𝐴) |
7 | | ssdomg 8043 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝑘 ⊆ 𝐴 → 𝑘 ≼ 𝐴)) |
8 | 7 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ≼ 𝐴) |
9 | 5, 6, 8 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ≼ 𝐴) |
10 | | hashdomi 13207 |
. . . . . . . . . . 11
⊢ (𝑘 ≼ 𝐴 → (#‘𝑘) ≤ (#‘𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (#‘𝑘) ≤ (#‘𝐴)) |
12 | | fznn 12446 |
. . . . . . . . . . 11
⊢
((#‘𝐴) ∈
ℤ → ((#‘𝑘)
∈ (1...(#‘𝐴))
↔ ((#‘𝑘) ∈
ℕ ∧ (#‘𝑘)
≤ (#‘𝐴)))) |
13 | 12 | rbaibd 969 |
. . . . . . . . . 10
⊢
(((#‘𝐴) ∈
ℤ ∧ (#‘𝑘)
≤ (#‘𝐴)) →
((#‘𝑘) ∈
(1...(#‘𝐴)) ↔
(#‘𝑘) ∈
ℕ)) |
14 | 4, 11, 13 | syl2anc 694 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((#‘𝑘) ∈ (1...(#‘𝐴)) ↔ (#‘𝑘) ∈
ℕ)) |
15 | | ssfi 8221 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ∈ Fin) |
16 | 5, 6, 15 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ∈ Fin) |
17 | | hashnncl 13195 |
. . . . . . . . . 10
⊢ (𝑘 ∈ Fin →
((#‘𝑘) ∈ ℕ
↔ 𝑘 ≠
∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((#‘𝑘) ∈ ℕ ↔ 𝑘 ≠ ∅)) |
19 | 14, 18 | bitr2d 269 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (𝑘 ≠ ∅ ↔ (#‘𝑘) ∈ (1...(#‘𝐴)))) |
20 | | df-ne 2824 |
. . . . . . . 8
⊢ (𝑘 ≠ ∅ ↔ ¬ 𝑘 = ∅) |
21 | | risset 3091 |
. . . . . . . 8
⊢
((#‘𝑘) ∈
(1...(#‘𝐴)) ↔
∃𝑛 ∈
(1...(#‘𝐴))𝑛 = (#‘𝑘)) |
22 | 19, 20, 21 | 3bitr3g 302 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 = ∅ ↔ ∃𝑛 ∈ (1...(#‘𝐴))𝑛 = (#‘𝑘))) |
23 | | velsn 4226 |
. . . . . . . 8
⊢ (𝑘 ∈ {∅} ↔ 𝑘 = ∅) |
24 | 23 | notbii 309 |
. . . . . . 7
⊢ (¬
𝑘 ∈ {∅} ↔
¬ 𝑘 =
∅) |
25 | | eqcom 2658 |
. . . . . . . 8
⊢
((#‘𝑘) = 𝑛 ↔ 𝑛 = (#‘𝑘)) |
26 | 25 | rexbii 3070 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1...(#‘𝐴))(#‘𝑘) = 𝑛 ↔ ∃𝑛 ∈ (1...(#‘𝐴))𝑛 = (#‘𝑘)) |
27 | 22, 24, 26 | 3bitr4g 303 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 ∈ {∅} ↔
∃𝑛 ∈
(1...(#‘𝐴))(#‘𝑘) = 𝑛)) |
28 | 27 | rabbidva 3219 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → {𝑘 ∈ 𝒫 𝐴 ∣ ¬ 𝑘 ∈ {∅}} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈ (1...(#‘𝐴))(#‘𝑘) = 𝑛}) |
29 | | dfdif2 3616 |
. . . . 5
⊢
(𝒫 𝐴 ∖
{∅}) = {𝑘 ∈
𝒫 𝐴 ∣ ¬
𝑘 ∈
{∅}} |
30 | | iunrab 4599 |
. . . . 5
⊢ ∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈ (1...(#‘𝐴))(#‘𝑘) = 𝑛} |
31 | 28, 29, 30 | 3eqtr4g 2710 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) =
∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) |
32 | 31 | sumeq1d 14475 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
33 | 1, 32 | eqtrd 2685 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑠 ∈ ∪
𝑛 ∈
(1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
34 | | fzfid 12812 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(1...(#‘𝐴)) ∈
Fin) |
35 | | simpll 805 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 𝐴 ∈ Fin) |
36 | | pwfi 8302 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
37 | 35, 36 | sylib 208 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 𝒫 𝐴 ∈ Fin) |
38 | | ssrab2 3720 |
. . . 4
⊢ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ⊆ 𝒫 𝐴 |
39 | | ssfi 8221 |
. . . 4
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑘 ∈
𝒫 𝐴 ∣
(#‘𝑘) = 𝑛} ⊆ 𝒫 𝐴) → {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ∈ Fin) |
40 | 37, 38, 39 | sylancl 695 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ∈ Fin) |
41 | | fveq2 6229 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑠 → (#‘𝑘) = (#‘𝑠)) |
42 | 41 | eqeq1d 2653 |
. . . . . . . . 9
⊢ (𝑘 = 𝑠 → ((#‘𝑘) = 𝑛 ↔ (#‘𝑠) = 𝑛)) |
43 | 42 | elrab 3396 |
. . . . . . . 8
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ↔ (𝑠 ∈ 𝒫 𝐴 ∧ (#‘𝑠) = 𝑛)) |
44 | 43 | simprbi 479 |
. . . . . . 7
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} → (#‘𝑠) = 𝑛) |
45 | 44 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘𝑠) = 𝑛) |
46 | 45 | ralrimiva 2995 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → ∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘𝑠) = 𝑛) |
47 | 46 | ralrimiva 2995 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
∀𝑛 ∈
(1...(#‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘𝑠) = 𝑛) |
48 | | invdisj 4670 |
. . . 4
⊢
(∀𝑛 ∈
(1...(#‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘𝑠) = 𝑛 → Disj 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) |
49 | 47, 48 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj
𝑛 ∈
(1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) |
50 | 45 | oveq1d 6705 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((#‘𝑠) − 1) = (𝑛 − 1)) |
51 | 50 | oveq2d 6706 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (-1↑((#‘𝑠) − 1)) = (-1↑(𝑛 − 1))) |
52 | 51 | oveq1d 6705 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠)) = ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))) |
53 | | 1cnd 10094 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 1 ∈
ℂ) |
54 | 53 | negcld 10417 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → -1 ∈
ℂ) |
55 | | elfznn 12408 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (1...(#‘𝐴)) → 𝑛 ∈ ℕ) |
56 | 55 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → 𝑛 ∈ ℕ) |
57 | | nnm1nn0 11372 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
58 | 56, 57 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → (𝑛 − 1) ∈
ℕ0) |
59 | 54, 58 | expcld 13048 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → (-1↑(𝑛 − 1)) ∈
ℂ) |
60 | 59 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (-1↑(𝑛 − 1)) ∈ ℂ) |
61 | | unifi 8296 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
62 | 61 | ad2antrr 762 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∪ 𝐴 ∈ Fin) |
63 | 56 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑛 ∈ ℕ) |
64 | 45, 63 | eqeltrd 2730 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘𝑠) ∈ ℕ) |
65 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝐴 ∈ Fin) |
66 | | elrabi 3391 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} → 𝑠 ∈ 𝒫 𝐴) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ∈ 𝒫 𝐴) |
68 | | elpwi 4201 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ⊆ 𝐴) |
70 | | ssfi 8221 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ Fin ∧ 𝑠 ⊆ 𝐴) → 𝑠 ∈ Fin) |
71 | 65, 69, 70 | syl2anc 694 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ∈ Fin) |
72 | | hashnncl 13195 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
((#‘𝑠) ∈ ℕ
↔ 𝑠 ≠
∅)) |
73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((#‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅)) |
74 | 64, 73 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → 𝑠 ≠ ∅) |
75 | | intssuni 4531 |
. . . . . . . . . . 11
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝑠) |
77 | 69 | unissd 4494 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∪ 𝑠 ⊆ ∪ 𝐴) |
78 | 76, 77 | sstrd 3646 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝐴) |
79 | | ssfi 8221 |
. . . . . . . . 9
⊢ ((∪ 𝐴
∈ Fin ∧ ∩ 𝑠 ⊆ ∪ 𝐴) → ∩ 𝑠
∈ Fin) |
80 | 62, 78, 79 | syl2anc 694 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ∩ 𝑠 ∈ Fin) |
81 | | hashcl 13185 |
. . . . . . . 8
⊢ (∩ 𝑠
∈ Fin → (#‘∩ 𝑠) ∈
ℕ0) |
82 | 80, 81 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘∩ 𝑠)
∈ ℕ0) |
83 | 82 | nn0cnd 11391 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → (#‘∩ 𝑠)
∈ ℂ) |
84 | 60, 83 | mulcld 10098 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))
∈ ℂ) |
85 | 52, 84 | eqeltrd 2730 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛}) → ((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠)) ∈ ℂ) |
86 | 85 | anasss 680 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ (𝑛 ∈ (1...(#‘𝐴)) ∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛})) → ((-1↑((#‘𝑠) − 1)) ·
(#‘∩ 𝑠)) ∈ ℂ) |
87 | 34, 40, 49, 86 | fsumiun 14597 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(#‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑛 ∈
(1...(#‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))) |
88 | 52 | sumeq2dv 14477 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))) |
89 | 40, 59, 83 | fsummulc2 14560 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → ((-1↑(𝑛 − 1)) ·
Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠)) = Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (#‘∩ 𝑠))) |
90 | 88, 89 | eqtr4d 2688 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈ (1...(#‘𝐴))) → Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= ((-1↑(𝑛 − 1))
· Σ𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠))) |
91 | 90 | sumeq2dv 14477 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑛 ∈
(1...(#‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} ((-1↑((#‘𝑠) − 1)) · (#‘∩ 𝑠))
= Σ𝑛 ∈
(1...(#‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠))) |
92 | 33, 87, 91 | 3eqtrd 2689 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(#‘∪ 𝐴) = Σ𝑛 ∈ (1...(#‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (#‘𝑘) = 𝑛} (#‘∩ 𝑠))) |