Step | Hyp | Ref
| Expression |
1 | | musumsum.3 |
. . . . . . 7
β’ (π β π΄ β β) |
2 | 1 | sselda 3948 |
. . . . . 6
β’ ((π β§ π β π΄) β π β β) |
3 | | musum 26563 |
. . . . . 6
β’ (π β β β
Ξ£π β {π β β β£ π β₯ π} (ΞΌβπ) = if(π = 1, 1, 0)) |
4 | 2, 3 | syl 17 |
. . . . 5
β’ ((π β§ π β π΄) β Ξ£π β {π β β β£ π β₯ π} (ΞΌβπ) = if(π = 1, 1, 0)) |
5 | 4 | oveq1d 7376 |
. . . 4
β’ ((π β§ π β π΄) β (Ξ£π β {π β β β£ π β₯ π} (ΞΌβπ) Β· π΅) = (if(π = 1, 1, 0) Β· π΅)) |
6 | | fzfid 13887 |
. . . . . 6
β’ ((π β§ π β π΄) β (1...π) β Fin) |
7 | | dvdsssfz1 16208 |
. . . . . . 7
β’ (π β β β {π β β β£ π β₯ π} β (1...π)) |
8 | 2, 7 | syl 17 |
. . . . . 6
β’ ((π β§ π β π΄) β {π β β β£ π β₯ π} β (1...π)) |
9 | 6, 8 | ssfid 9217 |
. . . . 5
β’ ((π β§ π β π΄) β {π β β β£ π β₯ π} β Fin) |
10 | | musumsum.5 |
. . . . 5
β’ ((π β§ π β π΄) β π΅ β β) |
11 | | elrabi 3643 |
. . . . . . . 8
β’ (π β {π β β β£ π β₯ π} β π β β) |
12 | | mucl 26513 |
. . . . . . . 8
β’ (π β β β
(ΞΌβπ) β
β€) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (π β {π β β β£ π β₯ π} β (ΞΌβπ) β β€) |
14 | 13 | zcnd 12616 |
. . . . . 6
β’ (π β {π β β β£ π β₯ π} β (ΞΌβπ) β β) |
15 | 14 | adantl 483 |
. . . . 5
β’ (((π β§ π β π΄) β§ π β {π β β β£ π β₯ π}) β (ΞΌβπ) β β) |
16 | 9, 10, 15 | fsummulc1 15678 |
. . . 4
β’ ((π β§ π β π΄) β (Ξ£π β {π β β β£ π β₯ π} (ΞΌβπ) Β· π΅) = Ξ£π β {π β β β£ π β₯ π} ((ΞΌβπ) Β· π΅)) |
17 | | ovif 7458 |
. . . . 5
β’ (if(π = 1, 1, 0) Β· π΅) = if(π = 1, (1 Β· π΅), (0 Β· π΅)) |
18 | | velsn 4606 |
. . . . . . . . 9
β’ (π β {1} β π = 1) |
19 | 18 | bicomi 223 |
. . . . . . . 8
β’ (π = 1 β π β {1}) |
20 | 19 | a1i 11 |
. . . . . . 7
β’ (π΅ β β β (π = 1 β π β {1})) |
21 | | mulid2 11162 |
. . . . . . 7
β’ (π΅ β β β (1
Β· π΅) = π΅) |
22 | | mul02 11341 |
. . . . . . 7
β’ (π΅ β β β (0
Β· π΅) =
0) |
23 | 20, 21, 22 | ifbieq12d 4518 |
. . . . . 6
β’ (π΅ β β β if(π = 1, (1 Β· π΅), (0 Β· π΅)) = if(π β {1}, π΅, 0)) |
24 | 10, 23 | syl 17 |
. . . . 5
β’ ((π β§ π β π΄) β if(π = 1, (1 Β· π΅), (0 Β· π΅)) = if(π β {1}, π΅, 0)) |
25 | 17, 24 | eqtrid 2785 |
. . . 4
β’ ((π β§ π β π΄) β (if(π = 1, 1, 0) Β· π΅) = if(π β {1}, π΅, 0)) |
26 | 5, 16, 25 | 3eqtr3d 2781 |
. . 3
β’ ((π β§ π β π΄) β Ξ£π β {π β β β£ π β₯ π} ((ΞΌβπ) Β· π΅) = if(π β {1}, π΅, 0)) |
27 | 26 | sumeq2dv 15596 |
. 2
β’ (π β Ξ£π β π΄ Ξ£π β {π β β β£ π β₯ π} ((ΞΌβπ) Β· π΅) = Ξ£π β π΄ if(π β {1}, π΅, 0)) |
28 | | musumsum.4 |
. . . 4
β’ (π β 1 β π΄) |
29 | 28 | snssd 4773 |
. . 3
β’ (π β {1} β π΄) |
30 | 29 | sselda 3948 |
. . . . 5
β’ ((π β§ π β {1}) β π β π΄) |
31 | 30, 10 | syldan 592 |
. . . 4
β’ ((π β§ π β {1}) β π΅ β β) |
32 | 31 | ralrimiva 3140 |
. . 3
β’ (π β βπ β {1}π΅ β β) |
33 | | musumsum.2 |
. . . 4
β’ (π β π΄ β Fin) |
34 | 33 | olcd 873 |
. . 3
β’ (π β (π΄ β (β€β₯β1)
β¨ π΄ β
Fin)) |
35 | | sumss2 15619 |
. . 3
β’ ((({1}
β π΄ β§
βπ β {1}π΅ β β) β§ (π΄ β
(β€β₯β1) β¨ π΄ β Fin)) β Ξ£π β {1}π΅ = Ξ£π β π΄ if(π β {1}, π΅, 0)) |
36 | 29, 32, 34, 35 | syl21anc 837 |
. 2
β’ (π β Ξ£π β {1}π΅ = Ξ£π β π΄ if(π β {1}, π΅, 0)) |
37 | | musumsum.1 |
. . . . 5
β’ (π = 1 β π΅ = πΆ) |
38 | 37 | eleq1d 2819 |
. . . 4
β’ (π = 1 β (π΅ β β β πΆ β β)) |
39 | 10 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β π΄ π΅ β β) |
40 | 38, 39, 28 | rspcdva 3584 |
. . 3
β’ (π β πΆ β β) |
41 | 37 | sumsn 15639 |
. . 3
β’ ((1
β π΄ β§ πΆ β β) β
Ξ£π β {1}π΅ = πΆ) |
42 | 28, 40, 41 | syl2anc 585 |
. 2
β’ (π β Ξ£π β {1}π΅ = πΆ) |
43 | 27, 36, 42 | 3eqtr2d 2779 |
1
β’ (π β Ξ£π β π΄ Ξ£π β {π β β β£ π β₯ π} ((ΞΌβπ) Β· π΅) = πΆ) |