Step | Hyp | Ref
| Expression |
1 | | breq2 5114 |
. . . . . 6
β’ (π = π β (7 < π β 7 < π)) |
2 | | eleq1 2826 |
. . . . . 6
β’ (π = π β (π β GoldbachOdd β π β GoldbachOdd )) |
3 | 1, 2 | imbi12d 345 |
. . . . 5
β’ (π = π β ((7 < π β π β GoldbachOdd ) β (7 < π β π β GoldbachOdd ))) |
4 | 3 | rspcv 3580 |
. . . 4
β’ (π β Odd β
(βπ β Odd (7
< π β π β GoldbachOdd ) β (7
< π β π β GoldbachOdd
))) |
5 | 4 | adantl 483 |
. . 3
β’ ((π β
(β€β₯β8) β§ π β Odd ) β (βπ β Odd (7 < π β π β GoldbachOdd ) β (7 < π β π β GoldbachOdd ))) |
6 | | eluz2 12776 |
. . . . . 6
β’ (π β
(β€β₯β8) β (8 β β€ β§ π β β€ β§ 8 β€
π)) |
7 | | 7lt8 12352 |
. . . . . . . . 9
β’ 7 <
8 |
8 | | 7re 12253 |
. . . . . . . . . . 11
β’ 7 β
β |
9 | 8 | a1i 11 |
. . . . . . . . . 10
β’ (π β β€ β 7 β
β) |
10 | | 8re 12256 |
. . . . . . . . . . 11
β’ 8 β
β |
11 | 10 | a1i 11 |
. . . . . . . . . 10
β’ (π β β€ β 8 β
β) |
12 | | zre 12510 |
. . . . . . . . . 10
β’ (π β β€ β π β
β) |
13 | | ltletr 11254 |
. . . . . . . . . 10
β’ ((7
β β β§ 8 β β β§ π β β) β ((7 < 8 β§ 8
β€ π) β 7 < π)) |
14 | 9, 11, 12, 13 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β β€ β ((7 <
8 β§ 8 β€ π) β 7
< π)) |
15 | 7, 14 | mpani 695 |
. . . . . . . 8
β’ (π β β€ β (8 β€
π β 7 < π)) |
16 | 15 | imp 408 |
. . . . . . 7
β’ ((π β β€ β§ 8 β€
π) β 7 < π) |
17 | 16 | 3adant1 1131 |
. . . . . 6
β’ ((8
β β€ β§ π
β β€ β§ 8 β€ π) β 7 < π) |
18 | 6, 17 | sylbi 216 |
. . . . 5
β’ (π β
(β€β₯β8) β 7 < π) |
19 | 18 | adantr 482 |
. . . 4
β’ ((π β
(β€β₯β8) β§ π β Odd ) β 7 < π) |
20 | | pm2.27 42 |
. . . 4
β’ (7 <
π β ((7 < π β π β GoldbachOdd ) β π β GoldbachOdd
)) |
21 | 19, 20 | syl 17 |
. . 3
β’ ((π β
(β€β₯β8) β§ π β Odd ) β ((7 < π β π β GoldbachOdd ) β π β GoldbachOdd
)) |
22 | | isgbo 46019 |
. . . . 5
β’ (π β GoldbachOdd β
(π β Odd β§
βπ β β
βπ β β
βπ β β
((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) |
23 | | 1ex 11158 |
. . . . . . . . . . . . . . . 16
β’ 1 β
V |
24 | | 2ex 12237 |
. . . . . . . . . . . . . . . 16
β’ 2 β
V |
25 | | 3ex 12242 |
. . . . . . . . . . . . . . . 16
β’ 3 β
V |
26 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π β V |
27 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π β V |
28 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π β V |
29 | | 1ne2 12368 |
. . . . . . . . . . . . . . . 16
β’ 1 β
2 |
30 | | 1re 11162 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
31 | | 1lt3 12333 |
. . . . . . . . . . . . . . . . 17
β’ 1 <
3 |
32 | 30, 31 | ltneii 11275 |
. . . . . . . . . . . . . . . 16
β’ 1 β
3 |
33 | | 2re 12234 |
. . . . . . . . . . . . . . . . 17
β’ 2 β
β |
34 | | 2lt3 12332 |
. . . . . . . . . . . . . . . . 17
β’ 2 <
3 |
35 | 33, 34 | ltneii 11275 |
. . . . . . . . . . . . . . . 16
β’ 2 β
3 |
36 | 23, 24, 25, 26, 27, 28, 29, 32, 35 | ftp 7108 |
. . . . . . . . . . . . . . 15
β’ {β¨1,
πβ©, β¨2, πβ©, β¨3, πβ©}:{1, 2, 3}βΆ{π, π, π} |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (((π β β β§ π β β) β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©, β¨3, πβ©}:{1, 2, 3}βΆ{π, π, π}) |
38 | | 1p2e3 12303 |
. . . . . . . . . . . . . . . . . 18
β’ (1 + 2) =
3 |
39 | 38 | eqcomi 2746 |
. . . . . . . . . . . . . . . . 17
β’ 3 = (1 +
2) |
40 | 39 | oveq2i 7373 |
. . . . . . . . . . . . . . . 16
β’ (1...3) =
(1...(1 + 2)) |
41 | | 1z 12540 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β€ |
42 | | fztp 13504 |
. . . . . . . . . . . . . . . . 17
β’ (1 β
β€ β (1...(1 + 2)) = {1, (1 + 1), (1 + 2)}) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (1...(1 +
2)) = {1, (1 + 1), (1 + 2)} |
44 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’ 1 =
1 |
45 | | id 22 |
. . . . . . . . . . . . . . . . . 18
β’ (1 = 1
β 1 = 1) |
46 | | 1p1e2 12285 |
. . . . . . . . . . . . . . . . . . 19
β’ (1 + 1) =
2 |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (1 = 1
β (1 + 1) = 2) |
48 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (1 = 1
β (1 + 2) = 3) |
49 | 45, 47, 48 | tpeq123d 4714 |
. . . . . . . . . . . . . . . . 17
β’ (1 = 1
β {1, (1 + 1), (1 + 2)} = {1, 2, 3}) |
50 | 44, 49 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ {1, (1 +
1), (1 + 2)} = {1, 2, 3} |
51 | 40, 43, 50 | 3eqtri 2769 |
. . . . . . . . . . . . . . 15
β’ (1...3) =
{1, 2, 3} |
52 | 51 | feq2i 6665 |
. . . . . . . . . . . . . 14
β’
({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©}:(1...3)βΆ{π, π, π} β {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}:{1, 2, 3}βΆ{π, π, π}) |
53 | 37, 52 | sylibr 233 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©, β¨3, πβ©}:(1...3)βΆ{π, π, π}) |
54 | | df-3an 1090 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β β§ π β β) β ((π β β β§ π β β) β§ π β
β)) |
55 | 26, 27, 28 | tpss 4800 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β β§ π β β) β {π, π, π} β β) |
56 | 54, 55 | sylbb1 236 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β {π, π, π} β β) |
57 | 53, 56 | fssd 6691 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β) β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©, β¨3, πβ©}:(1...3)βΆβ) |
58 | | prmex 16560 |
. . . . . . . . . . . . . 14
β’ β
β V |
59 | | ovex 7395 |
. . . . . . . . . . . . . 14
β’ (1...3)
β V |
60 | 58, 59 | pm3.2i 472 |
. . . . . . . . . . . . 13
β’ (β
β V β§ (1...3) β V) |
61 | | elmapg 8785 |
. . . . . . . . . . . . 13
β’ ((β
β V β§ (1...3) β V) β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©} β (β βm
(1...3)) β {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}:(1...3)βΆβ)) |
62 | 60, 61 | mp1i 13 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β) β§ π β β) β
({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©} β (β
βm (1...3)) β {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}:(1...3)βΆβ)) |
63 | 57, 62 | mpbird 257 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β) β§ π β β) β
{β¨1, πβ©, β¨2,
πβ©, β¨3, πβ©} β (β
βm (1...3))) |
64 | | fveq1 6846 |
. . . . . . . . . . . . . 14
β’ (π = {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©} β (πβπ) = ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ)) |
65 | 64 | sumeq2sdv 15596 |
. . . . . . . . . . . . 13
β’ (π = {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©} β Ξ£π β (1...3)(πβπ) = Ξ£π β (1...3)({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ)) |
66 | 65 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π = {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©} β (((π + π) + π) = Ξ£π β (1...3)(πβπ) β ((π + π) + π) = Ξ£π β (1...3)({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ))) |
67 | 66 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β β β§ π β β) β§ π β β) β§ π = {β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}) β (((π + π) + π) = Ξ£π β (1...3)(πβπ) β ((π + π) + π) = Ξ£π β (1...3)({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ))) |
68 | 51 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β (1...3)
= {1, 2, 3}) |
69 | 68 | sumeq1d 15593 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β) β§ π β β) β
Ξ£π β
(1...3)({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©}βπ) = Ξ£π β {1, 2, 3} ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ)) |
70 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 1 β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ) = ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}β1)) |
71 | 23, 26 | fvtp1 7149 |
. . . . . . . . . . . . . . 15
β’ ((1 β
2 β§ 1 β 3) β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}β1) = π) |
72 | 29, 32, 71 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©}β1) = π |
73 | 70, 72 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 1 β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ) = π) |
74 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 2 β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ) = ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}β2)) |
75 | 24, 27 | fvtp2 7150 |
. . . . . . . . . . . . . . 15
β’ ((1 β
2 β§ 2 β 3) β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}β2) = π) |
76 | 29, 35, 75 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©}β2) = π |
77 | 74, 76 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 2 β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ) = π) |
78 | | fveq2 6847 |
. . . . . . . . . . . . . 14
β’ (π = 3 β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ) = ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}β3)) |
79 | 25, 28 | fvtp3 7151 |
. . . . . . . . . . . . . . 15
β’ ((1 β
3 β§ 2 β 3) β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}β3) = π) |
80 | 32, 35, 79 | mp2an 691 |
. . . . . . . . . . . . . 14
β’
({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©}β3) = π |
81 | 78, 80 | eqtrdi 2793 |
. . . . . . . . . . . . 13
β’ (π = 3 β ({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ) = π) |
82 | | prmz 16558 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
83 | 82 | zcnd 12615 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
84 | | prmz 16558 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
85 | 84 | zcnd 12615 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
86 | | prmz 16558 |
. . . . . . . . . . . . . . . 16
β’ (π β β β π β
β€) |
87 | 86 | zcnd 12615 |
. . . . . . . . . . . . . . 15
β’ (π β β β π β
β) |
88 | 83, 85, 87 | 3anim123i 1152 |
. . . . . . . . . . . . . 14
β’ ((π β β β§ π β β β§ π β β) β (π β β β§ π β β β§ π β
β)) |
89 | 88 | 3expa 1119 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β (π β β β§ π β β β§ π β
β)) |
90 | | 2z 12542 |
. . . . . . . . . . . . . . 15
β’ 2 β
β€ |
91 | | 3z 12543 |
. . . . . . . . . . . . . . 15
β’ 3 β
β€ |
92 | 41, 90, 91 | 3pm3.2i 1340 |
. . . . . . . . . . . . . 14
β’ (1 β
β€ β§ 2 β β€ β§ 3 β β€) |
93 | 92 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β (1
β β€ β§ 2 β β€ β§ 3 β β€)) |
94 | 29 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β 1 β
2) |
95 | 32 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β 1 β
3) |
96 | 35 | a1i 11 |
. . . . . . . . . . . . 13
β’ (((π β β β§ π β β) β§ π β β) β 2 β
3) |
97 | 73, 77, 81, 89, 93, 94, 95, 96 | sumtp 15641 |
. . . . . . . . . . . 12
β’ (((π β β β§ π β β) β§ π β β) β
Ξ£π β {1, 2, 3}
({β¨1, πβ©,
β¨2, πβ©, β¨3,
πβ©}βπ) = ((π + π) + π)) |
98 | 69, 97 | eqtr2d 2778 |
. . . . . . . . . . 11
β’ (((π β β β§ π β β) β§ π β β) β ((π + π) + π) = Ξ£π β (1...3)({β¨1, πβ©, β¨2, πβ©, β¨3, πβ©}βπ)) |
99 | 63, 67, 98 | rspcedvd 3586 |
. . . . . . . . . 10
β’ (((π β β β§ π β β) β§ π β β) β
βπ β (β
βm (1...3))((π + π) + π) = Ξ£π β (1...3)(πβπ)) |
100 | | eqeq1 2741 |
. . . . . . . . . . 11
β’ (π = ((π + π) + π) β (π = Ξ£π β (1...3)(πβπ) β ((π + π) + π) = Ξ£π β (1...3)(πβπ))) |
101 | 100 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π = ((π + π) + π) β (βπ β (β βm
(1...3))π = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...3))((π + π) + π) = Ξ£π β (1...3)(πβπ))) |
102 | 99, 101 | syl5ibrcom 247 |
. . . . . . . . 9
β’ (((π β β β§ π β β) β§ π β β) β (π = ((π + π) + π) β βπ β (β βm
(1...3))π = Ξ£π β (1...3)(πβπ))) |
103 | 102 | adantld 492 |
. . . . . . . 8
β’ (((π β β β§ π β β) β§ π β β) β (((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)) β βπ β (β βm
(1...3))π = Ξ£π β (1...3)(πβπ))) |
104 | 103 | rexlimdva 3153 |
. . . . . . 7
β’ ((π β β β§ π β β) β
(βπ β β
((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)) β βπ β (β βm
(1...3))π = Ξ£π β (1...3)(πβπ))) |
105 | 104 | rexlimivv 3197 |
. . . . . 6
β’
(βπ β
β βπ β
β βπ β
β ((π β Odd
β§ π β Odd β§
π β Odd ) β§ π = ((π + π) + π)) β βπ β (β βm
(1...3))π = Ξ£π β (1...3)(πβπ)) |
106 | 105 | adantl 483 |
. . . . 5
β’ ((π β Odd β§ βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))) β βπ β (β βm
(1...3))π = Ξ£π β (1...3)(πβπ)) |
107 | 22, 106 | sylbi 216 |
. . . 4
β’ (π β GoldbachOdd β
βπ β (β
βm (1...3))π = Ξ£π β (1...3)(πβπ)) |
108 | 107 | a1i 11 |
. . 3
β’ ((π β
(β€β₯β8) β§ π β Odd ) β (π β GoldbachOdd β βπ β (β
βm (1...3))π = Ξ£π β (1...3)(πβπ))) |
109 | 5, 21, 108 | 3syld 60 |
. 2
β’ ((π β
(β€β₯β8) β§ π β Odd ) β (βπ β Odd (7 < π β π β GoldbachOdd ) β βπ β (β
βm (1...3))π = Ξ£π β (1...3)(πβπ))) |
110 | 109 | com12 32 |
1
β’
(βπ β
Odd (7 < π β π β GoldbachOdd ) β
((π β
(β€β₯β8) β§ π β Odd ) β βπ β (β
βm (1...3))π = Ξ£π β (1...3)(πβπ))) |