Proof of Theorem incexc2
Step | Hyp | Ref
| Expression |
1 | | incexc 15278 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) |
2 | | hashcl 13802 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
3 | 2 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (♯‘𝐴) ∈
ℕ0) |
4 | 3 | nn0zd 12159 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (♯‘𝐴) ∈
ℤ) |
5 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
6 | | elpwi 4494 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝒫 𝐴 → 𝑘 ⊆ 𝐴) |
7 | | ssdomg 8594 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝑘 ⊆ 𝐴 → 𝑘 ≼ 𝐴)) |
8 | 7 | imp 410 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ≼ 𝐴) |
9 | 5, 6, 8 | syl2an 599 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ≼ 𝐴) |
10 | | hashdomi 13826 |
. . . . . . . . . . 11
⊢ (𝑘 ≼ 𝐴 → (♯‘𝑘) ≤ (♯‘𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (♯‘𝑘) ≤ (♯‘𝐴)) |
12 | | fznn 13059 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → ((♯‘𝑘) ∈ (1...(♯‘𝐴)) ↔ ((♯‘𝑘) ∈ ℕ ∧
(♯‘𝑘) ≤
(♯‘𝐴)))) |
13 | 12 | rbaibd 544 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝑘) ≤ (♯‘𝐴)) → ((♯‘𝑘) ∈ (1...(♯‘𝐴)) ↔ (♯‘𝑘) ∈
ℕ)) |
14 | 4, 11, 13 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((♯‘𝑘) ∈
(1...(♯‘𝐴))
↔ (♯‘𝑘)
∈ ℕ)) |
15 | | ssfi 8765 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ∈ Fin) |
16 | 5, 6, 15 | syl2an 599 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ∈ Fin) |
17 | | hashnncl 13812 |
. . . . . . . . . 10
⊢ (𝑘 ∈ Fin →
((♯‘𝑘) ∈
ℕ ↔ 𝑘 ≠
∅)) |
18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((♯‘𝑘) ∈ ℕ ↔ 𝑘 ≠ ∅)) |
19 | 14, 18 | bitr2d 283 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (𝑘 ≠ ∅ ↔ (♯‘𝑘) ∈
(1...(♯‘𝐴)))) |
20 | | df-ne 2935 |
. . . . . . . 8
⊢ (𝑘 ≠ ∅ ↔ ¬ 𝑘 = ∅) |
21 | | risset 3176 |
. . . . . . . 8
⊢
((♯‘𝑘)
∈ (1...(♯‘𝐴)) ↔ ∃𝑛 ∈ (1...(♯‘𝐴))𝑛 = (♯‘𝑘)) |
22 | 19, 20, 21 | 3bitr3g 316 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 = ∅ ↔ ∃𝑛 ∈
(1...(♯‘𝐴))𝑛 = (♯‘𝑘))) |
23 | | velsn 4529 |
. . . . . . . 8
⊢ (𝑘 ∈ {∅} ↔ 𝑘 = ∅) |
24 | 23 | notbii 323 |
. . . . . . 7
⊢ (¬
𝑘 ∈ {∅} ↔
¬ 𝑘 =
∅) |
25 | | eqcom 2745 |
. . . . . . . 8
⊢
((♯‘𝑘) =
𝑛 ↔ 𝑛 = (♯‘𝑘)) |
26 | 25 | rexbii 3160 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1...(♯‘𝐴))(♯‘𝑘) = 𝑛 ↔ ∃𝑛 ∈ (1...(♯‘𝐴))𝑛 = (♯‘𝑘)) |
27 | 22, 24, 26 | 3bitr4g 317 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 ∈ {∅} ↔
∃𝑛 ∈
(1...(♯‘𝐴))(♯‘𝑘) = 𝑛)) |
28 | 27 | rabbidva 3378 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → {𝑘 ∈ 𝒫 𝐴 ∣ ¬ 𝑘 ∈ {∅}} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈
(1...(♯‘𝐴))(♯‘𝑘) = 𝑛}) |
29 | | dfdif2 3850 |
. . . . 5
⊢
(𝒫 𝐴 ∖
{∅}) = {𝑘 ∈
𝒫 𝐴 ∣ ¬
𝑘 ∈
{∅}} |
30 | | iunrab 4935 |
. . . . 5
⊢ ∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈ (1...(♯‘𝐴))(♯‘𝑘) = 𝑛} |
31 | 28, 29, 30 | 3eqtr4g 2798 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) =
∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) |
32 | 31 | sumeq1d 15144 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
33 | 1, 32 | eqtrd 2773 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑠 ∈ ∪
𝑛 ∈
(1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
34 | | fzfid 13425 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(1...(♯‘𝐴))
∈ Fin) |
35 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 𝐴 ∈
Fin) |
36 | | pwfi 8769 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
37 | 35, 36 | sylib 221 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 𝒫 𝐴 ∈
Fin) |
38 | | ssrab2 3967 |
. . . 4
⊢ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ⊆ 𝒫 𝐴 |
39 | | ssfi 8765 |
. . . 4
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑘 ∈
𝒫 𝐴 ∣
(♯‘𝑘) = 𝑛} ⊆ 𝒫 𝐴) → {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ∈ Fin) |
40 | 37, 38, 39 | sylancl 589 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ {𝑘 ∈ 𝒫
𝐴 ∣
(♯‘𝑘) = 𝑛} ∈ Fin) |
41 | | fveqeq2 6677 |
. . . . . . . . 9
⊢ (𝑘 = 𝑠 → ((♯‘𝑘) = 𝑛 ↔ (♯‘𝑠) = 𝑛)) |
42 | 41 | elrab 3585 |
. . . . . . . 8
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ↔ (𝑠 ∈ 𝒫 𝐴 ∧ (♯‘𝑠) = 𝑛)) |
43 | 42 | simprbi 500 |
. . . . . . 7
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} → (♯‘𝑠) = 𝑛) |
44 | 43 | adantl 485 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘𝑠) = 𝑛) |
45 | 44 | ralrimiva 3096 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ ∀𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘𝑠) = 𝑛) |
46 | 45 | ralrimiva 3096 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
∀𝑛 ∈
(1...(♯‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘𝑠) = 𝑛) |
47 | | invdisj 5011 |
. . . 4
⊢
(∀𝑛 ∈
(1...(♯‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘𝑠) = 𝑛 → Disj 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) |
48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj
𝑛 ∈
(1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) |
49 | 44 | oveq1d 7179 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((♯‘𝑠) − 1) = (𝑛 − 1)) |
50 | 49 | oveq2d 7180 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (-1↑((♯‘𝑠) − 1)) = (-1↑(𝑛 − 1))) |
51 | 50 | oveq1d 7179 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))) |
52 | | 1cnd 10707 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 1 ∈ ℂ) |
53 | 52 | negcld 11055 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ -1 ∈ ℂ) |
54 | | elfznn 13020 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(♯‘𝐴))
→ 𝑛 ∈
ℕ) |
55 | 54 | adantl 485 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 𝑛 ∈
ℕ) |
56 | | nnm1nn0 12010 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ (𝑛 − 1) ∈
ℕ0) |
58 | 53, 57 | expcld 13595 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ (-1↑(𝑛 −
1)) ∈ ℂ) |
59 | 58 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (-1↑(𝑛 − 1)) ∈ ℂ) |
60 | | unifi 8879 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
61 | 60 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∪ 𝐴 ∈ Fin) |
62 | 55 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑛 ∈ ℕ) |
63 | 44, 62 | eqeltrd 2833 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘𝑠) ∈ ℕ) |
64 | 35 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝐴 ∈ Fin) |
65 | | elrabi 3579 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} → 𝑠 ∈ 𝒫 𝐴) |
66 | 65 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ∈ 𝒫 𝐴) |
67 | | elpwi 4494 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ⊆ 𝐴) |
69 | 64, 68 | ssfid 8812 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ∈ Fin) |
70 | | hashnncl 13812 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
((♯‘𝑠) ∈
ℕ ↔ 𝑠 ≠
∅)) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅)) |
72 | 63, 71 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ≠ ∅) |
73 | | intssuni 4855 |
. . . . . . . . . . 11
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
74 | 72, 73 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝑠) |
75 | 68 | unissd 4803 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∪ 𝑠 ⊆ ∪ 𝐴) |
76 | 74, 75 | sstrd 3885 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝐴) |
77 | 61, 76 | ssfid 8812 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∩ 𝑠 ∈ Fin) |
78 | | hashcl 13802 |
. . . . . . . 8
⊢ (∩ 𝑠
∈ Fin → (♯‘∩ 𝑠) ∈
ℕ0) |
79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘∩ 𝑠)
∈ ℕ0) |
80 | 79 | nn0cnd 12031 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘∩ 𝑠)
∈ ℂ) |
81 | 59, 80 | mulcld 10732 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))
∈ ℂ) |
82 | 51, 81 | eqeltrd 2833 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) ∈ ℂ) |
83 | 82 | anasss 470 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ (𝑛 ∈
(1...(♯‘𝐴))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛})) → ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) ∈ ℂ) |
84 | 34, 40, 48, 83 | fsumiun 15262 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = Σ𝑛 ∈ (1...(♯‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
85 | 51 | sumeq2dv 15146 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ Σ𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))) |
86 | 40, 58, 80 | fsummulc2 15225 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ ((-1↑(𝑛 −
1)) · Σ𝑠
∈ {𝑘 ∈ 𝒫
𝐴 ∣
(♯‘𝑘) = 𝑛} (♯‘∩ 𝑠))
= Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))) |
87 | 85, 86 | eqtr4d 2776 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ Σ𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = ((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩
𝑠))) |
88 | 87 | sumeq2dv 15146 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑛 ∈
(1...(♯‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = Σ𝑛 ∈ (1...(♯‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩
𝑠))) |
89 | 33, 84, 88 | 3eqtrd 2777 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑛 ∈ (1...(♯‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩
𝑠))) |