Step | Hyp | Ref
| Expression |
1 | | sticksstones9.2 |
. . . . 5
β’ (π β πΎ = 0) |
2 | 1 | iftrued 4495 |
. . . 4
β’ (π β if(πΎ = 0, {β¨1, πβ©}, (π β (1...(πΎ + 1)) β¦ if(π = (πΎ + 1), ((π + πΎ) β (πβπΎ)), if(π = 1, ((πβ1) β 1), (((πβπ) β (πβ(π β 1))) β 1))))) = {β¨1,
πβ©}) |
3 | 2 | adantr 482 |
. . 3
β’ ((π β§ π β π΅) β if(πΎ = 0, {β¨1, πβ©}, (π β (1...(πΎ + 1)) β¦ if(π = (πΎ + 1), ((π + πΎ) β (πβπΎ)), if(π = 1, ((πβ1) β 1), (((πβπ) β (πβ(π β 1))) β 1))))) = {β¨1,
πβ©}) |
4 | | eqid 2733 |
. . . . . . . . . . 11
β’ {β¨1,
πβ©} = {β¨1, πβ©} |
5 | | 1nn 12169 |
. . . . . . . . . . . . 13
β’ 1 β
β |
6 | 5 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β 1 β
β) |
7 | | sticksstones9.1 |
. . . . . . . . . . . 12
β’ (π β π β
β0) |
8 | | fsng 7084 |
. . . . . . . . . . . 12
β’ ((1
β β β§ π
β β0) β ({β¨1, πβ©}:{1}βΆ{π} β {β¨1, πβ©} = {β¨1, πβ©})) |
9 | 6, 7, 8 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β ({β¨1, πβ©}:{1}βΆ{π} β {β¨1, πβ©} = {β¨1, πβ©})) |
10 | 4, 9 | mpbiri 258 |
. . . . . . . . . 10
β’ (π β {β¨1, πβ©}:{1}βΆ{π}) |
11 | 7 | snssd 4770 |
. . . . . . . . . 10
β’ (π β {π} β
β0) |
12 | 10, 11 | jca 513 |
. . . . . . . . 9
β’ (π β ({β¨1, πβ©}:{1}βΆ{π} β§ {π} β
β0)) |
13 | | fss 6686 |
. . . . . . . . 9
β’
(({β¨1, πβ©}:{1}βΆ{π} β§ {π} β β0) β
{β¨1, πβ©}:{1}βΆβ0) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
β’ (π β {β¨1, πβ©}:{1}βΆβ0) |
15 | 1 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (π β (πΎ + 1) = (0 + 1)) |
16 | | 0p1e1 12280 |
. . . . . . . . . . . . 13
β’ (0 + 1) =
1 |
17 | 15, 16 | eqtrdi 2789 |
. . . . . . . . . . . 12
β’ (π β (πΎ + 1) = 1) |
18 | 17 | oveq2d 7374 |
. . . . . . . . . . 11
β’ (π β (1...(πΎ + 1)) = (1...1)) |
19 | | 1zzd 12539 |
. . . . . . . . . . . 12
β’ (π β 1 β
β€) |
20 | | fzsn 13489 |
. . . . . . . . . . . 12
β’ (1 β
β€ β (1...1) = {1}) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β (1...1) =
{1}) |
22 | 18, 21 | eqtrd 2773 |
. . . . . . . . . 10
β’ (π β (1...(πΎ + 1)) = {1}) |
23 | 22 | eqcomd 2739 |
. . . . . . . . 9
β’ (π β {1} = (1...(πΎ + 1))) |
24 | 23 | feq2d 6655 |
. . . . . . . 8
β’ (π β ({β¨1, πβ©}:{1}βΆβ0
β {β¨1, πβ©}:(1...(πΎ +
1))βΆβ0)) |
25 | 14, 24 | mpbid 231 |
. . . . . . 7
β’ (π β {β¨1, πβ©}:(1...(πΎ +
1))βΆβ0) |
26 | 22 | sumeq1d 15591 |
. . . . . . . 8
β’ (π β Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = Ξ£π β {1} ({β¨1, πβ©}βπ)) |
27 | | fvsng 7127 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ π
β β0) β ({β¨1, πβ©}β1) = π) |
28 | 6, 7, 27 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ({β¨1, πβ©}β1) = π) |
29 | 7 | nn0cnd 12480 |
. . . . . . . . . . . 12
β’ (π β π β β) |
30 | 28, 29 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ (π β ({β¨1, πβ©}β1) β
β) |
31 | 6, 30 | jca 513 |
. . . . . . . . . 10
β’ (π β (1 β β β§
({β¨1, πβ©}β1) β
β)) |
32 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π = 1 β ({β¨1, πβ©}βπ) = ({β¨1, πβ©}β1)) |
33 | 32 | sumsn 15636 |
. . . . . . . . . 10
β’ ((1
β β β§ ({β¨1, πβ©}β1) β β) β
Ξ£π β {1}
({β¨1, πβ©}βπ) = ({β¨1, πβ©}β1)) |
34 | 31, 33 | syl 17 |
. . . . . . . . 9
β’ (π β Ξ£π β {1} ({β¨1, πβ©}βπ) = ({β¨1, πβ©}β1)) |
35 | 6, 7 | jca 513 |
. . . . . . . . . 10
β’ (π β (1 β β β§
π β
β0)) |
36 | 35, 27 | syl 17 |
. . . . . . . . 9
β’ (π β ({β¨1, πβ©}β1) = π) |
37 | 34, 36 | eqtrd 2773 |
. . . . . . . 8
β’ (π β Ξ£π β {1} ({β¨1, πβ©}βπ) = π) |
38 | 26, 37 | eqtrd 2773 |
. . . . . . 7
β’ (π β Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π) |
39 | 25, 38 | jca 513 |
. . . . . 6
β’ (π β ({β¨1, πβ©}:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π)) |
40 | 39 | adantr 482 |
. . . . 5
β’ ((π β§ π β π΅) β ({β¨1, πβ©}:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π)) |
41 | | snex 5389 |
. . . . . 6
β’ {β¨1,
πβ©} β
V |
42 | | feq1 6650 |
. . . . . . . 8
β’ (π = {β¨1, πβ©} β (π:(1...(πΎ + 1))βΆβ0 β
{β¨1, πβ©}:(1...(πΎ +
1))βΆβ0)) |
43 | | simpl 484 |
. . . . . . . . . . 11
β’ ((π = {β¨1, πβ©} β§ π β (1...(πΎ + 1))) β π = {β¨1, πβ©}) |
44 | 43 | fveq1d 6845 |
. . . . . . . . . 10
β’ ((π = {β¨1, πβ©} β§ π β (1...(πΎ + 1))) β (πβπ) = ({β¨1, πβ©}βπ)) |
45 | 44 | sumeq2dv 15593 |
. . . . . . . . 9
β’ (π = {β¨1, πβ©} β Ξ£π β (1...(πΎ + 1))(πβπ) = Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ)) |
46 | 45 | eqeq1d 2735 |
. . . . . . . 8
β’ (π = {β¨1, πβ©} β (Ξ£π β (1...(πΎ + 1))(πβπ) = π β Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π)) |
47 | 42, 46 | anbi12d 632 |
. . . . . . 7
β’ (π = {β¨1, πβ©} β ((π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π) β ({β¨1, πβ©}:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π))) |
48 | 47 | elabg 3629 |
. . . . . 6
β’
({β¨1, πβ©}
β V β ({β¨1, πβ©} β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β ({β¨1, πβ©}:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π))) |
49 | 41, 48 | ax-mp 5 |
. . . . 5
β’
({β¨1, πβ©}
β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} β ({β¨1, πβ©}:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))({β¨1, πβ©}βπ) = π)) |
50 | 40, 49 | sylibr 233 |
. . . 4
β’ ((π β§ π β π΅) β {β¨1, πβ©} β {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
51 | | sticksstones9.4 |
. . . . 5
β’ π΄ = {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)} |
52 | 51 | a1i 11 |
. . . 4
β’ ((π β§ π β π΅) β π΄ = {π β£ (π:(1...(πΎ + 1))βΆβ0 β§
Ξ£π β (1...(πΎ + 1))(πβπ) = π)}) |
53 | 50, 52 | eleqtrrd 2837 |
. . 3
β’ ((π β§ π β π΅) β {β¨1, πβ©} β π΄) |
54 | 3, 53 | eqeltrd 2834 |
. 2
β’ ((π β§ π β π΅) β if(πΎ = 0, {β¨1, πβ©}, (π β (1...(πΎ + 1)) β¦ if(π = (πΎ + 1), ((π + πΎ) β (πβπΎ)), if(π = 1, ((πβ1) β 1), (((πβπ) β (πβ(π β 1))) β 1))))) β π΄) |
55 | | sticksstones9.3 |
. 2
β’ πΊ = (π β π΅ β¦ if(πΎ = 0, {β¨1, πβ©}, (π β (1...(πΎ + 1)) β¦ if(π = (πΎ + 1), ((π + πΎ) β (πβπΎ)), if(π = 1, ((πβ1) β 1), (((πβπ) β (πβ(π β 1))) β
1)))))) |
56 | 54, 55 | fmptd 7063 |
1
β’ (π β πΊ:π΅βΆπ΄) |