Step | Hyp | Ref
| Expression |
1 | | 2nn 12285 |
. 2
β’ 2 β
β |
2 | | 1ne2 12420 |
. . . . 5
β’ 1 β
2 |
3 | | 1ex 11210 |
. . . . . 6
β’ 1 β
V |
4 | | 2ex 12289 |
. . . . . 6
β’ 2 β
V |
5 | 3, 4, 4, 4 | fpr 7152 |
. . . . 5
β’ (1 β 2
β {β¨1, 2β©, β¨2, 2β©}:{1, 2}βΆ{2,
2}) |
6 | | 2prm 16629 |
. . . . . . . 8
β’ 2 β
β |
7 | 6, 6 | pm3.2i 472 |
. . . . . . 7
β’ (2 β
β β§ 2 β β) |
8 | 4, 4 | prss 4824 |
. . . . . . 7
β’ ((2
β β β§ 2 β β) β {2, 2} β
β) |
9 | 7, 8 | mpbi 229 |
. . . . . 6
β’ {2, 2}
β β |
10 | | fss 6735 |
. . . . . 6
β’
(({β¨1, 2β©, β¨2, 2β©}:{1, 2}βΆ{2, 2} β§ {2, 2}
β β) β {β¨1, 2β©, β¨2, 2β©}:{1,
2}βΆβ) |
11 | 9, 10 | mpan2 690 |
. . . . 5
β’
({β¨1, 2β©, β¨2, 2β©}:{1, 2}βΆ{2, 2} β
{β¨1, 2β©, β¨2, 2β©}:{1, 2}βΆβ) |
12 | 2, 5, 11 | mp2b 10 |
. . . 4
β’ {β¨1,
2β©, β¨2, 2β©}:{1, 2}βΆβ |
13 | | prmex 16614 |
. . . . 5
β’ β
β V |
14 | | prex 5433 |
. . . . 5
β’ {1, 2}
β V |
15 | 13, 14 | elmap 8865 |
. . . 4
β’
({β¨1, 2β©, β¨2, 2β©} β (β βm
{1, 2}) β {β¨1, 2β©, β¨2, 2β©}:{1,
2}βΆβ) |
16 | 12, 15 | mpbir 230 |
. . 3
β’ {β¨1,
2β©, β¨2, 2β©} β (β βm {1,
2}) |
17 | | 2re 12286 |
. . . . 5
β’ 2 β
β |
18 | | 3re 12292 |
. . . . 5
β’ 3 β
β |
19 | | 2lt3 12384 |
. . . . 5
β’ 2 <
3 |
20 | 17, 18, 19 | ltleii 11337 |
. . . 4
β’ 2 β€
3 |
21 | | 2cn 12287 |
. . . . . 6
β’ 2 β
β |
22 | | fveq2 6892 |
. . . . . . . 8
β’ (π = 1 β ({β¨1, 2β©,
β¨2, 2β©}βπ)
= ({β¨1, 2β©, β¨2, 2β©}β1)) |
23 | 3, 4 | fvpr1 7191 |
. . . . . . . . 9
β’ (1 β 2
β ({β¨1, 2β©, β¨2, 2β©}β1) = 2) |
24 | 2, 23 | ax-mp 5 |
. . . . . . . 8
β’
({β¨1, 2β©, β¨2, 2β©}β1) = 2 |
25 | 22, 24 | eqtrdi 2789 |
. . . . . . 7
β’ (π = 1 β ({β¨1, 2β©,
β¨2, 2β©}βπ)
= 2) |
26 | | fveq2 6892 |
. . . . . . . 8
β’ (π = 2 β ({β¨1, 2β©,
β¨2, 2β©}βπ)
= ({β¨1, 2β©, β¨2, 2β©}β2)) |
27 | 4, 4 | fvpr2 7193 |
. . . . . . . . 9
β’ (1 β 2
β ({β¨1, 2β©, β¨2, 2β©}β2) = 2) |
28 | 2, 27 | ax-mp 5 |
. . . . . . . 8
β’
({β¨1, 2β©, β¨2, 2β©}β2) = 2 |
29 | 26, 28 | eqtrdi 2789 |
. . . . . . 7
β’ (π = 2 β ({β¨1, 2β©,
β¨2, 2β©}βπ)
= 2) |
30 | | id 22 |
. . . . . . . 8
β’ (2 β
β β 2 β β) |
31 | 30 | ancri 551 |
. . . . . . 7
β’ (2 β
β β (2 β β β§ 2 β β)) |
32 | 3 | jctl 525 |
. . . . . . 7
β’ (2 β
β β (1 β V β§ 2 β β)) |
33 | 2 | a1i 11 |
. . . . . . 7
β’ (2 β
β β 1 β 2) |
34 | 25, 29, 31, 32, 33 | sumpr 15694 |
. . . . . 6
β’ (2 β
β β Ξ£π
β {1, 2} ({β¨1, 2β©, β¨2, 2β©}βπ) = (2 + 2)) |
35 | 21, 34 | ax-mp 5 |
. . . . 5
β’
Ξ£π β {1,
2} ({β¨1, 2β©, β¨2, 2β©}βπ) = (2 + 2) |
36 | | 2p2e4 12347 |
. . . . 5
β’ (2 + 2) =
4 |
37 | 35, 36 | eqtr2i 2762 |
. . . 4
β’ 4 =
Ξ£π β {1, 2}
({β¨1, 2β©, β¨2, 2β©}βπ) |
38 | 20, 37 | pm3.2i 472 |
. . 3
β’ (2 β€ 3
β§ 4 = Ξ£π β
{1, 2} ({β¨1, 2β©, β¨2, 2β©}βπ)) |
39 | | fveq1 6891 |
. . . . . . 7
β’ (π = {β¨1, 2β©, β¨2,
2β©} β (πβπ) = ({β¨1, 2β©, β¨2,
2β©}βπ)) |
40 | 39 | sumeq2sdv 15650 |
. . . . . 6
β’ (π = {β¨1, 2β©, β¨2,
2β©} β Ξ£π
β {1, 2} (πβπ) = Ξ£π β {1, 2} ({β¨1, 2β©, β¨2,
2β©}βπ)) |
41 | 40 | eqeq2d 2744 |
. . . . 5
β’ (π = {β¨1, 2β©, β¨2,
2β©} β (4 = Ξ£π β {1, 2} (πβπ) β 4 = Ξ£π β {1, 2} ({β¨1, 2β©, β¨2,
2β©}βπ))) |
42 | 41 | anbi2d 630 |
. . . 4
β’ (π = {β¨1, 2β©, β¨2,
2β©} β ((2 β€ 3 β§ 4 = Ξ£π β {1, 2} (πβπ)) β (2 β€ 3 β§ 4 = Ξ£π β {1, 2} ({β¨1,
2β©, β¨2, 2β©}βπ)))) |
43 | 42 | rspcev 3613 |
. . 3
β’
(({β¨1, 2β©, β¨2, 2β©} β (β
βm {1, 2}) β§ (2 β€ 3 β§ 4 = Ξ£π β {1, 2} ({β¨1, 2β©, β¨2,
2β©}βπ))) β
βπ β (β
βm {1, 2})(2 β€ 3 β§ 4 = Ξ£π β {1, 2} (πβπ))) |
44 | 16, 38, 43 | mp2an 691 |
. 2
β’
βπ β
(β βm {1, 2})(2 β€ 3 β§ 4 = Ξ£π β {1, 2} (πβπ)) |
45 | | oveq2 7417 |
. . . . . 6
β’ (π = 2 β (1...π) = (1...2)) |
46 | | df-2 12275 |
. . . . . . . 8
β’ 2 = (1 +
1) |
47 | 46 | oveq2i 7420 |
. . . . . . 7
β’ (1...2) =
(1...(1 + 1)) |
48 | | 1z 12592 |
. . . . . . . . 9
β’ 1 β
β€ |
49 | | fzpr 13556 |
. . . . . . . . 9
β’ (1 β
β€ β (1...(1 + 1)) = {1, (1 + 1)}) |
50 | 48, 49 | ax-mp 5 |
. . . . . . . 8
β’ (1...(1 +
1)) = {1, (1 + 1)} |
51 | | 1p1e2 12337 |
. . . . . . . . 9
β’ (1 + 1) =
2 |
52 | 51 | preq2i 4742 |
. . . . . . . 8
β’ {1, (1 +
1)} = {1, 2} |
53 | 50, 52 | eqtri 2761 |
. . . . . . 7
β’ (1...(1 +
1)) = {1, 2} |
54 | 47, 53 | eqtri 2761 |
. . . . . 6
β’ (1...2) =
{1, 2} |
55 | 45, 54 | eqtrdi 2789 |
. . . . 5
β’ (π = 2 β (1...π) = {1, 2}) |
56 | 55 | oveq2d 7425 |
. . . 4
β’ (π = 2 β (β
βm (1...π))
= (β βm {1, 2})) |
57 | | breq1 5152 |
. . . . 5
β’ (π = 2 β (π β€ 3 β 2 β€ 3)) |
58 | 55 | sumeq1d 15647 |
. . . . . 6
β’ (π = 2 β Ξ£π β (1...π)(πβπ) = Ξ£π β {1, 2} (πβπ)) |
59 | 58 | eqeq2d 2744 |
. . . . 5
β’ (π = 2 β (4 = Ξ£π β (1...π)(πβπ) β 4 = Ξ£π β {1, 2} (πβπ))) |
60 | 57, 59 | anbi12d 632 |
. . . 4
β’ (π = 2 β ((π β€ 3 β§ 4 = Ξ£π β (1...π)(πβπ)) β (2 β€ 3 β§ 4 = Ξ£π β {1, 2} (πβπ)))) |
61 | 56, 60 | rexeqbidv 3344 |
. . 3
β’ (π = 2 β (βπ β (β
βm (1...π))(π β€ 3 β§ 4 = Ξ£π β (1...π)(πβπ)) β βπ β (β βm {1, 2})(2
β€ 3 β§ 4 = Ξ£π
β {1, 2} (πβπ)))) |
62 | 61 | rspcev 3613 |
. 2
β’ ((2
β β β§ βπ β (β βm {1, 2})(2
β€ 3 β§ 4 = Ξ£π
β {1, 2} (πβπ))) β βπ β β βπ β (β βm
(1...π))(π β€ 3 β§ 4 = Ξ£π β (1...π)(πβπ))) |
63 | 1, 44, 62 | mp2an 691 |
1
β’
βπ β
β βπ β
(β βm (1...π))(π β€ 3 β§ 4 = Ξ£π β (1...π)(πβπ)) |