Step | Hyp | Ref
| Expression |
1 | | sticksstones16.3 |
. . . . . 6
β’ π΄ = {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} |
2 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π β (πβπ) = (πβπ)) |
3 | 2 | cbvsumv 15586 |
. . . . . . . . 9
β’
Ξ£π β
(1...πΎ)(πβπ) = Ξ£π β (1...πΎ)(πβπ) |
4 | 3 | eqeq1i 2738 |
. . . . . . . 8
β’
(Ξ£π β
(1...πΎ)(πβπ) = π β Ξ£π β (1...πΎ)(πβπ) = π) |
5 | 4 | anbi2i 624 |
. . . . . . 7
β’ ((π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π) β (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)) |
6 | 5 | abbii 2803 |
. . . . . 6
β’ {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} = {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} |
7 | 1, 6 | eqtri 2761 |
. . . . 5
β’ π΄ = {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} |
8 | 7 | a1i 11 |
. . . 4
β’ (π β π΄ = {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)}) |
9 | | nfv 1918 |
. . . . 5
β’
β²ππ |
10 | | sticksstones16.2 |
. . . . . . . . . . 11
β’ (π β πΎ β β) |
11 | 10 | nncnd 12174 |
. . . . . . . . . 10
β’ (π β πΎ β β) |
12 | | 1cnd 11155 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
13 | 11, 12 | npcand 11521 |
. . . . . . . . 9
β’ (π β ((πΎ β 1) + 1) = πΎ) |
14 | 13 | eqcomd 2739 |
. . . . . . . 8
β’ (π β πΎ = ((πΎ β 1) + 1)) |
15 | 14 | oveq2d 7374 |
. . . . . . 7
β’ (π β (1...πΎ) = (1...((πΎ β 1) + 1))) |
16 | 15 | feq2d 6655 |
. . . . . 6
β’ (π β (π:(1...πΎ)βΆβ0 β π:(1...((πΎ β 1) +
1))βΆβ0)) |
17 | 15 | sumeq1d 15591 |
. . . . . . 7
β’ (π β Ξ£π β (1...πΎ)(πβπ) = Ξ£π β (1...((πΎ β 1) + 1))(πβπ)) |
18 | 17 | eqeq1d 2735 |
. . . . . 6
β’ (π β (Ξ£π β (1...πΎ)(πβπ) = π β Ξ£π β (1...((πΎ β 1) + 1))(πβπ) = π)) |
19 | 16, 18 | anbi12d 632 |
. . . . 5
β’ (π β ((π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π) β (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π))) |
20 | 9, 19 | abbid 2804 |
. . . 4
β’ (π β {π β£ (π:(1...πΎ)βΆβ0 β§
Ξ£π β (1...πΎ)(πβπ) = π)} = {π β£ (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)}) |
21 | 8, 20 | eqtrd 2773 |
. . 3
β’ (π β π΄ = {π β£ (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)}) |
22 | 21 | fveq2d 6847 |
. 2
β’ (π β (β―βπ΄) = (β―β{π β£ (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)})) |
23 | | sticksstones16.1 |
. . 3
β’ (π β π β
β0) |
24 | | nnm1nn0 12459 |
. . . 4
β’ (πΎ β β β (πΎ β 1) β
β0) |
25 | 10, 24 | syl 17 |
. . 3
β’ (π β (πΎ β 1) β
β0) |
26 | | fveq2 6843 |
. . . . . . 7
β’ (π = π β (πβπ) = (πβπ)) |
27 | 26 | cbvsumv 15586 |
. . . . . 6
β’
Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = Ξ£π β (1...((πΎ β 1) + 1))(πβπ) |
28 | 27 | eqeq1i 2738 |
. . . . 5
β’
(Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π β Ξ£π β (1...((πΎ β 1) + 1))(πβπ) = π) |
29 | 28 | anbi2i 624 |
. . . 4
β’ ((π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π) β (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)) |
30 | 29 | abbii 2803 |
. . 3
β’ {π β£ (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)} = {π β£ (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)} |
31 | 23, 25, 30 | sticksstones15 40615 |
. 2
β’ (π β (β―β{π β£ (π:(1...((πΎ β 1) + 1))βΆβ0
β§ Ξ£π β
(1...((πΎ β 1) +
1))(πβπ) = π)}) = ((π + (πΎ β 1))C(πΎ β 1))) |
32 | 22, 31 | eqtrd 2773 |
1
β’ (π β (β―βπ΄) = ((π + (πΎ β 1))C(πΎ β 1))) |