Proof of Theorem incexc2
| Step | Hyp | Ref
| Expression |
| 1 | | incexc 15873 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑠 ∈ (𝒫 𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))) |
| 2 | | hashcl 14395 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ Fin →
(♯‘𝐴) ∈
ℕ0) |
| 3 | 2 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (♯‘𝐴) ∈
ℕ0) |
| 4 | 3 | nn0zd 12639 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (♯‘𝐴) ∈
ℤ) |
| 5 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → 𝐴 ∈ Fin) |
| 6 | | elpwi 4607 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ 𝒫 𝐴 → 𝑘 ⊆ 𝐴) |
| 7 | | ssdomg 9040 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ Fin → (𝑘 ⊆ 𝐴 → 𝑘 ≼ 𝐴)) |
| 8 | 7 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ≼ 𝐴) |
| 9 | 5, 6, 8 | syl2an 596 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ≼ 𝐴) |
| 10 | | hashdomi 14419 |
. . . . . . . . . . 11
⊢ (𝑘 ≼ 𝐴 → (♯‘𝑘) ≤ (♯‘𝐴)) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (♯‘𝑘) ≤ (♯‘𝐴)) |
| 12 | | fznn 13632 |
. . . . . . . . . . 11
⊢
((♯‘𝐴)
∈ ℤ → ((♯‘𝑘) ∈ (1...(♯‘𝐴)) ↔ ((♯‘𝑘) ∈ ℕ ∧
(♯‘𝑘) ≤
(♯‘𝐴)))) |
| 13 | 12 | rbaibd 540 |
. . . . . . . . . 10
⊢
(((♯‘𝐴)
∈ ℤ ∧ (♯‘𝑘) ≤ (♯‘𝐴)) → ((♯‘𝑘) ∈ (1...(♯‘𝐴)) ↔ (♯‘𝑘) ∈
ℕ)) |
| 14 | 4, 11, 13 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((♯‘𝑘) ∈
(1...(♯‘𝐴))
↔ (♯‘𝑘)
∈ ℕ)) |
| 15 | | ssfi 9213 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ Fin ∧ 𝑘 ⊆ 𝐴) → 𝑘 ∈ Fin) |
| 16 | 5, 6, 15 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → 𝑘 ∈ Fin) |
| 17 | | hashnncl 14405 |
. . . . . . . . . 10
⊢ (𝑘 ∈ Fin →
((♯‘𝑘) ∈
ℕ ↔ 𝑘 ≠
∅)) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → ((♯‘𝑘) ∈ ℕ ↔ 𝑘 ≠ ∅)) |
| 19 | 14, 18 | bitr2d 280 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (𝑘 ≠ ∅ ↔ (♯‘𝑘) ∈
(1...(♯‘𝐴)))) |
| 20 | | df-ne 2941 |
. . . . . . . 8
⊢ (𝑘 ≠ ∅ ↔ ¬ 𝑘 = ∅) |
| 21 | | risset 3233 |
. . . . . . . 8
⊢
((♯‘𝑘)
∈ (1...(♯‘𝐴)) ↔ ∃𝑛 ∈ (1...(♯‘𝐴))𝑛 = (♯‘𝑘)) |
| 22 | 19, 20, 21 | 3bitr3g 313 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 = ∅ ↔ ∃𝑛 ∈
(1...(♯‘𝐴))𝑛 = (♯‘𝑘))) |
| 23 | | velsn 4642 |
. . . . . . . 8
⊢ (𝑘 ∈ {∅} ↔ 𝑘 = ∅) |
| 24 | 23 | notbii 320 |
. . . . . . 7
⊢ (¬
𝑘 ∈ {∅} ↔
¬ 𝑘 =
∅) |
| 25 | | eqcom 2744 |
. . . . . . . 8
⊢
((♯‘𝑘) =
𝑛 ↔ 𝑛 = (♯‘𝑘)) |
| 26 | 25 | rexbii 3094 |
. . . . . . 7
⊢
(∃𝑛 ∈
(1...(♯‘𝐴))(♯‘𝑘) = 𝑛 ↔ ∃𝑛 ∈ (1...(♯‘𝐴))𝑛 = (♯‘𝑘)) |
| 27 | 22, 24, 26 | 3bitr4g 314 |
. . . . . 6
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑘 ∈ 𝒫 𝐴) → (¬ 𝑘 ∈ {∅} ↔
∃𝑛 ∈
(1...(♯‘𝐴))(♯‘𝑘) = 𝑛)) |
| 28 | 27 | rabbidva 3443 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → {𝑘 ∈ 𝒫 𝐴 ∣ ¬ 𝑘 ∈ {∅}} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈
(1...(♯‘𝐴))(♯‘𝑘) = 𝑛}) |
| 29 | | dfdif2 3960 |
. . . . 5
⊢
(𝒫 𝐴 ∖
{∅}) = {𝑘 ∈
𝒫 𝐴 ∣ ¬
𝑘 ∈
{∅}} |
| 30 | | iunrab 5052 |
. . . . 5
⊢ ∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} = {𝑘 ∈ 𝒫 𝐴 ∣ ∃𝑛 ∈ (1...(♯‘𝐴))(♯‘𝑘) = 𝑛} |
| 31 | 28, 29, 30 | 3eqtr4g 2802 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → (𝒫
𝐴 ∖ {∅}) =
∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) |
| 32 | 31 | sumeq1d 15736 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ (𝒫
𝐴 ∖
{∅})((-1↑((♯‘𝑠) − 1)) · (♯‘∩ 𝑠))
= Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
| 33 | 1, 32 | eqtrd 2777 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑠 ∈ ∪
𝑛 ∈
(1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
| 34 | | fzfid 14014 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(1...(♯‘𝐴))
∈ Fin) |
| 35 | | simpll 767 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 𝐴 ∈
Fin) |
| 36 | | pwfi 9357 |
. . . . 5
⊢ (𝐴 ∈ Fin ↔ 𝒫
𝐴 ∈
Fin) |
| 37 | 35, 36 | sylib 218 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 𝒫 𝐴 ∈
Fin) |
| 38 | | ssrab2 4080 |
. . . 4
⊢ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ⊆ 𝒫 𝐴 |
| 39 | | ssfi 9213 |
. . . 4
⊢
((𝒫 𝐴 ∈
Fin ∧ {𝑘 ∈
𝒫 𝐴 ∣
(♯‘𝑘) = 𝑛} ⊆ 𝒫 𝐴) → {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ∈ Fin) |
| 40 | 37, 38, 39 | sylancl 586 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ {𝑘 ∈ 𝒫
𝐴 ∣
(♯‘𝑘) = 𝑛} ∈ Fin) |
| 41 | | fveqeq2 6915 |
. . . . . . . . 9
⊢ (𝑘 = 𝑠 → ((♯‘𝑘) = 𝑛 ↔ (♯‘𝑠) = 𝑛)) |
| 42 | 41 | elrab 3692 |
. . . . . . . 8
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ↔ (𝑠 ∈ 𝒫 𝐴 ∧ (♯‘𝑠) = 𝑛)) |
| 43 | 42 | simprbi 496 |
. . . . . . 7
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} → (♯‘𝑠) = 𝑛) |
| 44 | 43 | adantl 481 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘𝑠) = 𝑛) |
| 45 | 44 | ralrimiva 3146 |
. . . . 5
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ ∀𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘𝑠) = 𝑛) |
| 46 | 45 | ralrimiva 3146 |
. . . 4
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
∀𝑛 ∈
(1...(♯‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘𝑠) = 𝑛) |
| 47 | | invdisj 5129 |
. . . 4
⊢
(∀𝑛 ∈
(1...(♯‘𝐴))∀𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘𝑠) = 𝑛 → Disj 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) |
| 48 | 46, 47 | syl 17 |
. . 3
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → Disj
𝑛 ∈
(1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) |
| 49 | 44 | oveq1d 7446 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((♯‘𝑠) − 1) = (𝑛 − 1)) |
| 50 | 49 | oveq2d 7447 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (-1↑((♯‘𝑠) − 1)) = (-1↑(𝑛 − 1))) |
| 51 | 50 | oveq1d 7446 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))) |
| 52 | | 1cnd 11256 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 1 ∈ ℂ) |
| 53 | 52 | negcld 11607 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ -1 ∈ ℂ) |
| 54 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(♯‘𝐴))
→ 𝑛 ∈
ℕ) |
| 55 | 54 | adantl 481 |
. . . . . . . . 9
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ 𝑛 ∈
ℕ) |
| 56 | | nnm1nn0 12567 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
| 57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ (𝑛 − 1) ∈
ℕ0) |
| 58 | 53, 57 | expcld 14186 |
. . . . . . 7
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ (-1↑(𝑛 −
1)) ∈ ℂ) |
| 59 | 58 | adantr 480 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (-1↑(𝑛 − 1)) ∈ ℂ) |
| 60 | | unifi 9384 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) → ∪ 𝐴
∈ Fin) |
| 61 | 60 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∪ 𝐴 ∈ Fin) |
| 62 | 55 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑛 ∈ ℕ) |
| 63 | 44, 62 | eqeltrd 2841 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘𝑠) ∈ ℕ) |
| 64 | 35 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝐴 ∈ Fin) |
| 65 | | elrabi 3687 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} → 𝑠 ∈ 𝒫 𝐴) |
| 66 | 65 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ∈ 𝒫 𝐴) |
| 67 | | elpwi 4607 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ 𝒫 𝐴 → 𝑠 ⊆ 𝐴) |
| 68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ⊆ 𝐴) |
| 69 | 64, 68 | ssfid 9301 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ∈ Fin) |
| 70 | | hashnncl 14405 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ Fin →
((♯‘𝑠) ∈
ℕ ↔ 𝑠 ≠
∅)) |
| 71 | 69, 70 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((♯‘𝑠) ∈ ℕ ↔ 𝑠 ≠ ∅)) |
| 72 | 63, 71 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → 𝑠 ≠ ∅) |
| 73 | | intssuni 4970 |
. . . . . . . . . . 11
⊢ (𝑠 ≠ ∅ → ∩ 𝑠
⊆ ∪ 𝑠) |
| 74 | 72, 73 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝑠) |
| 75 | 68 | unissd 4917 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∪ 𝑠 ⊆ ∪ 𝐴) |
| 76 | 74, 75 | sstrd 3994 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∩ 𝑠 ⊆ ∪ 𝐴) |
| 77 | 61, 76 | ssfid 9301 |
. . . . . . . 8
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ∩ 𝑠 ∈ Fin) |
| 78 | | hashcl 14395 |
. . . . . . . 8
⊢ (∩ 𝑠
∈ Fin → (♯‘∩ 𝑠) ∈
ℕ0) |
| 79 | 77, 78 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘∩ 𝑠)
∈ ℕ0) |
| 80 | 79 | nn0cnd 12589 |
. . . . . 6
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → (♯‘∩ 𝑠)
∈ ℂ) |
| 81 | 59, 80 | mulcld 11281 |
. . . . 5
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))
∈ ℂ) |
| 82 | 51, 81 | eqeltrd 2841 |
. . . 4
⊢ ((((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛}) → ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) ∈ ℂ) |
| 83 | 82 | anasss 466 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ (𝑛 ∈
(1...(♯‘𝐴))
∧ 𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛})) → ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) ∈ ℂ) |
| 84 | 34, 40, 48, 83 | fsumiun 15857 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑠 ∈ ∪ 𝑛 ∈ (1...(♯‘𝐴)){𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = Σ𝑛 ∈ (1...(♯‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠))) |
| 85 | 51 | sumeq2dv 15738 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ Σ𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))) |
| 86 | 40, 58, 80 | fsummulc2 15820 |
. . . 4
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ ((-1↑(𝑛 −
1)) · Σ𝑠
∈ {𝑘 ∈ 𝒫
𝐴 ∣
(♯‘𝑘) = 𝑛} (♯‘∩ 𝑠))
= Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑(𝑛 − 1)) · (♯‘∩ 𝑠))) |
| 87 | 85, 86 | eqtr4d 2780 |
. . 3
⊢ (((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) ∧ 𝑛 ∈
(1...(♯‘𝐴)))
→ Σ𝑠 ∈
{𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = ((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩
𝑠))) |
| 88 | 87 | sumeq2dv 15738 |
. 2
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
Σ𝑛 ∈
(1...(♯‘𝐴))Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} ((-1↑((♯‘𝑠) − 1)) ·
(♯‘∩ 𝑠)) = Σ𝑛 ∈ (1...(♯‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩
𝑠))) |
| 89 | 33, 84, 88 | 3eqtrd 2781 |
1
⊢ ((𝐴 ∈ Fin ∧ 𝐴 ⊆ Fin) →
(♯‘∪ 𝐴) = Σ𝑛 ∈ (1...(♯‘𝐴))((-1↑(𝑛 − 1)) · Σ𝑠 ∈ {𝑘 ∈ 𝒫 𝐴 ∣ (♯‘𝑘) = 𝑛} (♯‘∩
𝑠))) |