Step | Hyp | Ref
| Expression |
1 | | isgbe 46017 |
. 2
β’ (π β GoldbachEven β
(π β Even β§
βπ β β
βπ β β
(π β Odd β§ π β Odd β§ π = (π + π)))) |
2 | | 2nn 12233 |
. . . . . . . 8
β’ 2 β
β |
3 | 2 | a1i 11 |
. . . . . . 7
β’ (((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β 2 β β) |
4 | | oveq2 7370 |
. . . . . . . . . . 11
β’ (π = 2 β (1...π) = (1...2)) |
5 | | df-2 12223 |
. . . . . . . . . . . . 13
β’ 2 = (1 +
1) |
6 | 5 | oveq2i 7373 |
. . . . . . . . . . . 12
β’ (1...2) =
(1...(1 + 1)) |
7 | | 1z 12540 |
. . . . . . . . . . . . 13
β’ 1 β
β€ |
8 | | fzpr 13503 |
. . . . . . . . . . . . 13
β’ (1 β
β€ β (1...(1 + 1)) = {1, (1 + 1)}) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . 12
β’ (1...(1 +
1)) = {1, (1 + 1)} |
10 | | 1p1e2 12285 |
. . . . . . . . . . . . 13
β’ (1 + 1) =
2 |
11 | 10 | preq2i 4703 |
. . . . . . . . . . . 12
β’ {1, (1 +
1)} = {1, 2} |
12 | 6, 9, 11 | 3eqtri 2769 |
. . . . . . . . . . 11
β’ (1...2) =
{1, 2} |
13 | 4, 12 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π = 2 β (1...π) = {1, 2}) |
14 | 13 | oveq2d 7378 |
. . . . . . . . 9
β’ (π = 2 β (β
βm (1...π))
= (β βm {1, 2})) |
15 | | breq1 5113 |
. . . . . . . . . 10
β’ (π = 2 β (π β€ 3 β 2 β€ 3)) |
16 | 13 | sumeq1d 15593 |
. . . . . . . . . . 11
β’ (π = 2 β Ξ£π β (1...π)(πβπ) = Ξ£π β {1, 2} (πβπ)) |
17 | 16 | eqeq2d 2748 |
. . . . . . . . . 10
β’ (π = 2 β (π = Ξ£π β (1...π)(πβπ) β π = Ξ£π β {1, 2} (πβπ))) |
18 | 15, 17 | anbi12d 632 |
. . . . . . . . 9
β’ (π = 2 β ((π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)) β (2 β€ 3 β§ π = Ξ£π β {1, 2} (πβπ)))) |
19 | 14, 18 | rexeqbidv 3323 |
. . . . . . . 8
β’ (π = 2 β (βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)) β βπ β (β βm {1, 2})(2
β€ 3 β§ π =
Ξ£π β {1, 2}
(πβπ)))) |
20 | 19 | adantl 483 |
. . . . . . 7
β’ ((((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β§ π = 2) β (βπ β (β βm
(1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)) β βπ β (β βm {1, 2})(2
β€ 3 β§ π =
Ξ£π β {1, 2}
(πβπ)))) |
21 | | 1ne2 12368 |
. . . . . . . . . . . . 13
β’ 1 β
2 |
22 | | 1ex 11158 |
. . . . . . . . . . . . . 14
β’ 1 β
V |
23 | | 2ex 12237 |
. . . . . . . . . . . . . 14
β’ 2 β
V |
24 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π β V |
25 | | vex 3452 |
. . . . . . . . . . . . . 14
β’ π β V |
26 | 22, 23, 24, 25 | fpr 7105 |
. . . . . . . . . . . . 13
β’ (1 β 2
β {β¨1, πβ©,
β¨2, πβ©}:{1,
2}βΆ{π, π}) |
27 | 21, 26 | mp1i 13 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©}:{1,
2}βΆ{π, π}) |
28 | | prssi 4786 |
. . . . . . . . . . . 12
β’ ((π β β β§ π β β) β {π, π} β β) |
29 | 27, 28 | fssd 6691 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©}:{1,
2}βΆβ) |
30 | | prmex 16560 |
. . . . . . . . . . . . 13
β’ β
β V |
31 | | prex 5394 |
. . . . . . . . . . . . 13
β’ {1, 2}
β V |
32 | 30, 31 | pm3.2i 472 |
. . . . . . . . . . . 12
β’ (β
β V β§ {1, 2} β V) |
33 | | elmapg 8785 |
. . . . . . . . . . . 12
β’ ((β
β V β§ {1, 2} β V) β ({β¨1, πβ©, β¨2, πβ©} β (β βm
{1, 2}) β {β¨1, πβ©, β¨2, πβ©}:{1,
2}βΆβ)) |
34 | 32, 33 | mp1i 13 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
({β¨1, πβ©,
β¨2, πβ©} β
(β βm {1, 2}) β {β¨1, πβ©, β¨2, πβ©}:{1,
2}βΆβ)) |
35 | 29, 34 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©} β (β
βm {1, 2})) |
36 | | fveq1 6846 |
. . . . . . . . . . . . . . 15
β’ (π = {β¨1, πβ©, β¨2, πβ©} β (πβπ) = ({β¨1, πβ©, β¨2, πβ©}βπ)) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π = {β¨1, πβ©, β¨2, πβ©} β§ π β {1, 2}) β (πβπ) = ({β¨1, πβ©, β¨2, πβ©}βπ)) |
38 | 37 | sumeq2dv 15595 |
. . . . . . . . . . . . 13
β’ (π = {β¨1, πβ©, β¨2, πβ©} β Ξ£π β {1, 2} (πβπ) = Ξ£π β {1, 2} ({β¨1, πβ©, β¨2, πβ©}βπ)) |
39 | 38 | eqeq1d 2739 |
. . . . . . . . . . . 12
β’ (π = {β¨1, πβ©, β¨2, πβ©} β (Ξ£π β {1, 2} (πβπ) = (π + π) β Ξ£π β {1, 2} ({β¨1, πβ©, β¨2, πβ©}βπ) = (π + π))) |
40 | 39 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = {β¨1, πβ©, β¨2, πβ©} β ((2 β€ 3 β§ Ξ£π β {1, 2} (πβπ) = (π + π)) β (2 β€ 3 β§ Ξ£π β {1, 2} ({β¨1, πβ©, β¨2, πβ©}βπ) = (π + π)))) |
41 | 40 | adantl 483 |
. . . . . . . . . 10
β’ (((π β β β§ π β β) β§ π = {β¨1, πβ©, β¨2, πβ©}) β ((2 β€ 3 β§ Ξ£π β {1, 2} (πβπ) = (π + π)) β (2 β€ 3 β§ Ξ£π β {1, 2} ({β¨1, πβ©, β¨2, πβ©}βπ) = (π + π)))) |
42 | | prmz 16558 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
43 | | prmz 16558 |
. . . . . . . . . . . 12
β’ (π β β β π β
β€) |
44 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ({β¨1, πβ©, β¨2, πβ©}βπ) = ({β¨1, πβ©, β¨2, πβ©}β1)) |
45 | 22, 24 | fvpr1 7144 |
. . . . . . . . . . . . . . 15
β’ (1 β 2
β ({β¨1, πβ©,
β¨2, πβ©}β1)
= π) |
46 | 21, 45 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
({β¨1, πβ©,
β¨2, πβ©}β1)
= π |
47 | 44, 46 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 1 β ({β¨1, πβ©, β¨2, πβ©}βπ) = π) |
48 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 2 β ({β¨1, πβ©, β¨2, πβ©}βπ) = ({β¨1, πβ©, β¨2, πβ©}β2)) |
49 | 23, 25 | fvpr2 7146 |
. . . . . . . . . . . . . . 15
β’ (1 β 2
β ({β¨1, πβ©,
β¨2, πβ©}β2)
= π) |
50 | 21, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
({β¨1, πβ©,
β¨2, πβ©}β2)
= π |
51 | 48, 50 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 2 β ({β¨1, πβ©, β¨2, πβ©}βπ) = π) |
52 | | zcn 12511 |
. . . . . . . . . . . . . 14
β’ (π β β€ β π β
β) |
53 | | zcn 12511 |
. . . . . . . . . . . . . 14
β’ (π β β€ β π β
β) |
54 | 52, 53 | anim12i 614 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€) β (π β β β§ π β
β)) |
55 | 7, 2 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (1 β
β€ β§ 2 β β) |
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€) β (1
β β€ β§ 2 β β)) |
57 | 21 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β β€ β§ π β β€) β 1 β
2) |
58 | 47, 51, 54, 56, 57 | sumpr 15640 |
. . . . . . . . . . . 12
β’ ((π β β€ β§ π β β€) β
Ξ£π β {1, 2}
({β¨1, πβ©,
β¨2, πβ©}βπ) = (π + π)) |
59 | 42, 43, 58 | syl2an 597 |
. . . . . . . . . . 11
β’ ((π β β β§ π β β) β
Ξ£π β {1, 2}
({β¨1, πβ©,
β¨2, πβ©}βπ) = (π + π)) |
60 | | 2re 12234 |
. . . . . . . . . . . 12
β’ 2 β
β |
61 | | 3re 12240 |
. . . . . . . . . . . 12
β’ 3 β
β |
62 | | 2lt3 12332 |
. . . . . . . . . . . 12
β’ 2 <
3 |
63 | 60, 61, 62 | ltleii 11285 |
. . . . . . . . . . 11
β’ 2 β€
3 |
64 | 59, 63 | jctil 521 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β (2 β€
3 β§ Ξ£π β {1,
2} ({β¨1, πβ©,
β¨2, πβ©}βπ) = (π + π))) |
65 | 35, 41, 64 | rspcedvd 3586 |
. . . . . . . . 9
β’ ((π β β β§ π β β) β
βπ β (β
βm {1, 2})(2 β€ 3 β§ Ξ£π β {1, 2} (πβπ) = (π + π))) |
66 | 65 | adantr 482 |
. . . . . . . 8
β’ (((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β βπ β (β βm {1, 2})(2
β€ 3 β§ Ξ£π
β {1, 2} (πβπ) = (π + π))) |
67 | | eqeq1 2741 |
. . . . . . . . . . . . 13
β’ (π = (π + π) β (π = Ξ£π β {1, 2} (πβπ) β (π + π) = Ξ£π β {1, 2} (πβπ))) |
68 | | eqcom 2744 |
. . . . . . . . . . . . 13
β’ ((π + π) = Ξ£π β {1, 2} (πβπ) β Ξ£π β {1, 2} (πβπ) = (π + π)) |
69 | 67, 68 | bitrdi 287 |
. . . . . . . . . . . 12
β’ (π = (π + π) β (π = Ξ£π β {1, 2} (πβπ) β Ξ£π β {1, 2} (πβπ) = (π + π))) |
70 | 69 | anbi2d 630 |
. . . . . . . . . . 11
β’ (π = (π + π) β ((2 β€ 3 β§ π = Ξ£π β {1, 2} (πβπ)) β (2 β€ 3 β§ Ξ£π β {1, 2} (πβπ) = (π + π)))) |
71 | 70 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π = (π + π) β (βπ β (β βm {1, 2})(2
β€ 3 β§ π =
Ξ£π β {1, 2}
(πβπ)) β βπ β (β βm {1, 2})(2
β€ 3 β§ Ξ£π
β {1, 2} (πβπ) = (π + π)))) |
72 | 71 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ ((π β Odd β§ π β Odd β§ π = (π + π)) β (βπ β (β βm {1, 2})(2
β€ 3 β§ π =
Ξ£π β {1, 2}
(πβπ)) β βπ β (β βm {1, 2})(2
β€ 3 β§ Ξ£π
β {1, 2} (πβπ) = (π + π)))) |
73 | 72 | adantl 483 |
. . . . . . . 8
β’ (((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β (βπ β (β βm {1, 2})(2
β€ 3 β§ π =
Ξ£π β {1, 2}
(πβπ)) β βπ β (β βm {1, 2})(2
β€ 3 β§ Ξ£π
β {1, 2} (πβπ) = (π + π)))) |
74 | 66, 73 | mpbird 257 |
. . . . . . 7
β’ (((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β βπ β (β βm {1, 2})(2
β€ 3 β§ π =
Ξ£π β {1, 2}
(πβπ))) |
75 | 3, 20, 74 | rspcedvd 3586 |
. . . . . 6
β’ (((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β βπ β β βπ β (β βm
(1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) |
76 | 75 | a1d 25 |
. . . . 5
β’ (((π β β β§ π β β) β§ (π β Odd β§ π β Odd β§ π = (π + π))) β (π β Even β βπ β β βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)))) |
77 | 76 | ex 414 |
. . . 4
β’ ((π β β β§ π β β) β ((π β Odd β§ π β Odd β§ π = (π + π)) β (π β Even β βπ β β βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))))) |
78 | 77 | rexlimivv 3197 |
. . 3
β’
(βπ β
β βπ β
β (π β Odd β§
π β Odd β§ π = (π + π)) β (π β Even β βπ β β βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ)))) |
79 | 78 | impcom 409 |
. 2
β’ ((π β Even β§ βπ β β βπ β β (π β Odd β§ π β Odd β§ π = (π + π))) β βπ β β βπ β (β βm
(1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) |
80 | 1, 79 | sylbi 216 |
1
β’ (π β GoldbachEven β
βπ β β
βπ β (β
βm (1...π))(π β€ 3 β§ π = Ξ£π β (1...π)(πβπ))) |