Step | Hyp | Ref
| Expression |
1 | | elply 25572 |
. . 3
β’ (πΉ β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
2 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β π β ((π βͺ {0}) βm
β0)) |
3 | | simpll 766 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β π β β) |
4 | | cnex 11139 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
5 | | ssexg 5285 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ β
β V) β π β
V) |
6 | 3, 4, 5 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β π β V) |
7 | | snex 5393 |
. . . . . . . . . . . . . . 15
β’ {0}
β V |
8 | | unexg 7688 |
. . . . . . . . . . . . . . 15
β’ ((π β V β§ {0} β V)
β (π βͺ {0}) β
V) |
9 | 6, 7, 8 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π βͺ {0}) β V) |
10 | | nn0ex 12426 |
. . . . . . . . . . . . . 14
β’
β0 β V |
11 | | elmapg 8785 |
. . . . . . . . . . . . . 14
β’ (((π βͺ {0}) β V β§
β0 β V) β (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0}))) |
12 | 9, 10, 11 | sylancl 587 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0}))) |
13 | 2, 12 | mpbid 231 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β π:β0βΆ(π βͺ {0})) |
14 | 13 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β§ π₯ β β0) β (πβπ₯) β (π βͺ {0})) |
15 | | ssun2 4138 |
. . . . . . . . . . . 12
β’ {0}
β (π βͺ
{0}) |
16 | | c0ex 11156 |
. . . . . . . . . . . . 13
β’ 0 β
V |
17 | 16 | snss 4751 |
. . . . . . . . . . . 12
β’ (0 β
(π βͺ {0}) β {0}
β (π βͺ
{0})) |
18 | 15, 17 | mpbir 230 |
. . . . . . . . . . 11
β’ 0 β
(π βͺ
{0}) |
19 | | ifcl 4536 |
. . . . . . . . . . 11
β’ (((πβπ₯) β (π βͺ {0}) β§ 0 β (π βͺ {0})) β if(π₯ β (0...π), (πβπ₯), 0) β (π βͺ {0})) |
20 | 14, 18, 19 | sylancl 587 |
. . . . . . . . . 10
β’ ((((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β§ π₯ β β0) β if(π₯ β (0...π), (πβπ₯), 0) β (π βͺ {0})) |
21 | 20 | fmpttd 7068 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)):β0βΆ(π βͺ {0})) |
22 | | elmapg 8785 |
. . . . . . . . . 10
β’ (((π βͺ {0}) β V β§
β0 β V) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β ((π βͺ {0}) βm
β0) β (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)):β0βΆ(π βͺ {0}))) |
23 | 9, 10, 22 | sylancl 587 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β ((π βͺ {0}) βm
β0) β (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)):β0βΆ(π βͺ {0}))) |
24 | 21, 23 | mpbird 257 |
. . . . . . . 8
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β ((π βͺ {0}) βm
β0)) |
25 | | eleq1w 2821 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (π₯ β (0...π) β π β (0...π))) |
26 | | fveq2 6847 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π β (πβπ₯) = (πβπ)) |
27 | 25, 26 | ifbieq1d 4515 |
. . . . . . . . . . . . . . . 16
β’ (π₯ = π β if(π₯ β (0...π), (πβπ₯), 0) = if(π β (0...π), (πβπ), 0)) |
28 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0)) = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) |
29 | | fvex 6860 |
. . . . . . . . . . . . . . . . 17
β’ (πβπ) β V |
30 | 29, 16 | ifex 4541 |
. . . . . . . . . . . . . . . 16
β’ if(π β (0...π), (πβπ), 0) β V |
31 | 27, 28, 30 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β ((π₯ β
β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) = if(π β (0...π), (πβπ), 0)) |
32 | 31 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β0)
β§ (π β ((π βͺ {0}) βm
β0) β§ π β β0)) β ((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0))βπ) = if(π β (0...π), (πβπ), 0)) |
33 | | iffalse 4500 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π β (0...π) β if(π β (0...π), (πβπ), 0) = 0) |
34 | 33 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
β’ (Β¬
π β (0...π) β (((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) = if(π β (0...π), (πβπ), 0) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) = 0)) |
35 | 32, 34 | syl5ibcom 244 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β0)
β§ (π β ((π βͺ {0}) βm
β0) β§ π β β0)) β (Β¬
π β (0...π) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) = 0)) |
36 | 35 | necon1ad 2961 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β0)
β§ (π β ((π βͺ {0}) βm
β0) β§ π β β0)) β (((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0))βπ) β 0 β π β (0...π))) |
37 | | elfzle2 13452 |
. . . . . . . . . . . 12
β’ (π β (0...π) β π β€ π) |
38 | 36, 37 | syl6 35 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β0)
β§ (π β ((π βͺ {0}) βm
β0) β§ π β β0)) β (((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0))βπ) β 0 β π β€ π)) |
39 | 38 | anassrs 469 |
. . . . . . . . . 10
β’ ((((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β§ π β β0) β (((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0))βπ) β 0 β π β€ π)) |
40 | 39 | ralrimiva 3144 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β βπ β β0 (((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0))βπ) β 0 β π β€ π)) |
41 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β π β β0) |
42 | | 0cnd 11155 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β 0 β β) |
43 | 42 | snssd 4774 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β {0} β β) |
44 | 3, 43 | unssd 4151 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π βͺ {0}) β
β) |
45 | 21, 44 | fssd 6691 |
. . . . . . . . . 10
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯),
0)):β0βΆβ) |
46 | | plyco0 25569 |
. . . . . . . . . 10
β’ ((π β β0
β§ (π₯ β
β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)):β0βΆβ)
β (((π₯ β
β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1))) = {0} β βπ β β0
(((π₯ β
β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) β 0 β π β€ π))) |
47 | 41, 45, 46 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1))) = {0} β βπ β β0
(((π₯ β
β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) β 0 β π β€ π))) |
48 | 40, 47 | mpbird 257 |
. . . . . . . 8
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1))) = {0}) |
49 | | eqidd 2738 |
. . . . . . . 8
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
50 | | imaeq1 6013 |
. . . . . . . . . . 11
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β (π β (β€β₯β(π + 1))) = ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1)))) |
51 | 50 | eqeq1d 2739 |
. . . . . . . . . 10
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β ((π β (β€β₯β(π + 1))) = {0} β ((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1))) = {0})) |
52 | | fveq1 6846 |
. . . . . . . . . . . . . . 15
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β (πβπ) = ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ)) |
53 | | elfznn0 13541 |
. . . . . . . . . . . . . . . . 17
β’ (π β (0...π) β π β β0) |
54 | 53, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) = if(π β (0...π), (πβπ), 0)) |
55 | | iftrue 4497 |
. . . . . . . . . . . . . . . 16
β’ (π β (0...π) β if(π β (0...π), (πβπ), 0) = (πβπ)) |
56 | 54, 55 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
β’ (π β (0...π) β ((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0))βπ) = (πβπ)) |
57 | 52, 56 | sylan9eq 2797 |
. . . . . . . . . . . . . 14
β’ ((π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β§ π β (0...π)) β (πβπ) = (πβπ)) |
58 | 57 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β§ π β (0...π)) β ((πβπ) Β· (π§βπ)) = ((πβπ) Β· (π§βπ))) |
59 | 58 | sumeq2dv 15595 |
. . . . . . . . . . . 12
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β Ξ£π β (0...π)((πβπ) Β· (π§βπ)) = Ξ£π β (0...π)((πβπ) Β· (π§βπ))) |
60 | 59 | mpteq2dv 5212 |
. . . . . . . . . . 11
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
61 | 60 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β ((π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
62 | 51, 61 | anbi12d 632 |
. . . . . . . . 9
β’ (π = (π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β (((π β (β€β₯β(π + 1))) = {0} β§ (π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β (((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1))) = {0} β§ (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
63 | 62 | rspcev 3584 |
. . . . . . . 8
β’ (((π₯ β β0
β¦ if(π₯ β
(0...π), (πβπ₯), 0)) β ((π βͺ {0}) βm
β0) β§ (((π₯ β β0 β¦ if(π₯ β (0...π), (πβπ₯), 0)) β
(β€β₯β(π + 1))) = {0} β§ (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
64 | 24, 48, 49, 63 | syl12anc 836 |
. . . . . . 7
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
65 | | eqeq1 2741 |
. . . . . . . . 9
β’ (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
66 | 65 | anbi2d 630 |
. . . . . . . 8
β’ (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β ((π β (β€β₯β(π + 1))) = {0} β§ (π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
67 | 66 | rexbidv 3176 |
. . . . . . 7
β’ (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
68 | 64, 67 | syl5ibrcom 247 |
. . . . . 6
β’ (((π β β β§ π β β0)
β§ π β ((π βͺ {0}) βm
β0)) β (πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
69 | 68 | rexlimdva 3153 |
. . . . 5
β’ ((π β β β§ π β β0)
β (βπ β
((π βͺ {0})
βm β0)πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
70 | 69 | reximdva 3166 |
. . . 4
β’ (π β β β
(βπ β
β0 βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β βπ β β0 βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
71 | 70 | imdistani 570 |
. . 3
β’ ((π β β β§
βπ β
β0 βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
72 | 1, 71 | sylbi 216 |
. 2
β’ (πΉ β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |
73 | | simpr 486 |
. . . . . 6
β’ (((π β
(β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
74 | 73 | reximi 3088 |
. . . . 5
β’
(βπ β
((π βͺ {0})
βm β0)((π β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
75 | 74 | reximi 3088 |
. . . 4
β’
(βπ β
β0 βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) β βπ β β0 βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
76 | 75 | anim2i 618 |
. . 3
β’ ((π β β β§
βπ β
β0 βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
77 | | elply 25572 |
. . 3
β’ (πΉ β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)πΉ =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
78 | 76, 77 | sylibr 233 |
. 2
β’ ((π β β β§
βπ β
β0 βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) β πΉ β (Polyβπ)) |
79 | 72, 78 | impbii 208 |
1
β’ (πΉ β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)((π
β (β€β₯β(π + 1))) = {0} β§ πΉ = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))))) |