Step | Hyp | Ref
| Expression |
1 | | 1nn 12172 |
. 2
β’ 1 β
β |
2 | | 1zzd 12542 |
. . . . 5
β’ (π β β β 1 β
β€) |
3 | | id 22 |
. . . . 5
β’ (π β β β π β
β) |
4 | 2, 3 | fsnd 6831 |
. . . 4
β’ (π β β β {β¨1,
πβ©}:{1}βΆβ) |
5 | | prmex 16561 |
. . . . 5
β’ β
β V |
6 | | snex 5392 |
. . . . 5
β’ {1}
β V |
7 | 5, 6 | elmap 8815 |
. . . 4
β’
({β¨1, πβ©}
β (β βm {1}) β {β¨1, πβ©}:{1}βΆβ) |
8 | 4, 7 | sylibr 233 |
. . 3
β’ (π β β β {β¨1,
πβ©} β (β
βm {1})) |
9 | | 1re 11163 |
. . . . . . 7
β’ 1 β
β |
10 | | simpl 484 |
. . . . . . 7
β’ ((π β β β§ π β {1}) β π β
β) |
11 | | fvsng 7130 |
. . . . . . 7
β’ ((1
β β β§ π
β β) β ({β¨1, πβ©}β1) = π) |
12 | 9, 10, 11 | sylancr 588 |
. . . . . 6
β’ ((π β β β§ π β {1}) β ({β¨1,
πβ©}β1) = π) |
13 | 12 | sumeq2dv 15596 |
. . . . 5
β’ (π β β β
Ξ£π β {1}
({β¨1, πβ©}β1) = Ξ£π β {1}π) |
14 | | prmz 16559 |
. . . . . . 7
β’ (π β β β π β
β€) |
15 | 14 | zcnd 12616 |
. . . . . 6
β’ (π β β β π β
β) |
16 | | eqidd 2734 |
. . . . . . 7
β’ (π = 1 β π = π) |
17 | 16 | sumsn 15639 |
. . . . . 6
β’ ((1
β β β§ π
β β) β Ξ£π β {1}π = π) |
18 | 9, 15, 17 | sylancr 588 |
. . . . 5
β’ (π β β β
Ξ£π β {1}π = π) |
19 | 13, 18 | eqtr2d 2774 |
. . . 4
β’ (π β β β π = Ξ£π β {1} ({β¨1, πβ©}β1)) |
20 | | 1le3 12373 |
. . . 4
β’ 1 β€
3 |
21 | 19, 20 | jctil 521 |
. . 3
β’ (π β β β (1 β€ 3
β§ π = Ξ£π β {1} ({β¨1, πβ©}β1))) |
22 | | simpl 484 |
. . . . . . . 8
β’ ((π = {β¨1, πβ©} β§ π β {1}) β π = {β¨1, πβ©}) |
23 | | elsni 4607 |
. . . . . . . . 9
β’ (π β {1} β π = 1) |
24 | 23 | adantl 483 |
. . . . . . . 8
β’ ((π = {β¨1, πβ©} β§ π β {1}) β π = 1) |
25 | 22, 24 | fveq12d 6853 |
. . . . . . 7
β’ ((π = {β¨1, πβ©} β§ π β {1}) β (πβπ) = ({β¨1, πβ©}β1)) |
26 | 25 | sumeq2dv 15596 |
. . . . . 6
β’ (π = {β¨1, πβ©} β Ξ£π β {1} (πβπ) = Ξ£π β {1} ({β¨1, πβ©}β1)) |
27 | 26 | eqeq2d 2744 |
. . . . 5
β’ (π = {β¨1, πβ©} β (π = Ξ£π β {1} (πβπ) β π = Ξ£π β {1} ({β¨1, πβ©}β1))) |
28 | 27 | anbi2d 630 |
. . . 4
β’ (π = {β¨1, πβ©} β ((1 β€ 3 β§ π = Ξ£π β {1} (πβπ)) β (1 β€ 3 β§ π = Ξ£π β {1} ({β¨1, πβ©}β1)))) |
29 | 28 | rspcev 3583 |
. . 3
β’
(({β¨1, πβ©}
β (β βm {1}) β§ (1 β€ 3 β§ π = Ξ£π β {1} ({β¨1, πβ©}β1))) β βπ β (β
βm {1})(1 β€ 3 β§ π = Ξ£π β {1} (πβπ))) |
30 | 8, 21, 29 | syl2anc 585 |
. 2
β’ (π β β β
βπ β (β
βm {1})(1 β€ 3 β§ π = Ξ£π β {1} (πβπ))) |
31 | | oveq2 7369 |
. . . . . 6
β’ (π = 1 β (1...π) = (1...1)) |
32 | | 1z 12541 |
. . . . . . 7
β’ 1 β
β€ |
33 | | fzsn 13492 |
. . . . . . 7
β’ (1 β
β€ β (1...1) = {1}) |
34 | 32, 33 | ax-mp 5 |
. . . . . 6
β’ (1...1) =
{1} |
35 | 31, 34 | eqtrdi 2789 |
. . . . 5
β’ (π = 1 β (1...π) = {1}) |
36 | 35 | oveq2d 7377 |
. . . 4
β’ (π = 1 β (β
βm (1...π))
= (β βm {1})) |
37 | | breq1 5112 |
. . . . 5
β’ (π = 1 β (π β€ 3 β 1 β€ 3)) |
38 | 35 | sumeq1d 15594 |
. . . . . 6
β’ (π = 1 β Ξ£π β (1...π)(πβπ) = Ξ£π β {1} (πβπ)) |
39 | 38 | eqeq2d 2744 |
. . . . 5
β’ (π = 1 β (π = Ξ£π β (1...π)(πβπ) β π = Ξ£π β {1} (πβπ))) |
40 | 37, 39 | anbi12d 632 |
. . . 4
β’ (π = 1 β ((π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)) β (1 β€ 3 β§ π = Ξ£π β {1} (πβπ)))) |
41 | 36, 40 | rexeqbidv 3319 |
. . 3
β’ (π = 1 β (βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)) β βπ β (β βm {1})(1
β€ 3 β§ π =
Ξ£π β {1} (πβπ)))) |
42 | 41 | rspcev 3583 |
. 2
β’ ((1
β β β§ βπ β (β βm {1})(1
β€ 3 β§ π =
Ξ£π β {1} (πβπ))) β βπ β β βπ β (β βm
(1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) |
43 | 1, 30, 42 | sylancr 588 |
1
β’ (π β β β
βπ β β
βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) |