Step | Hyp | Ref
| Expression |
1 | | evengpop3 46080 |
. . . 4
β’
(βπ β
Odd (5 < π β π β GoldbachOddW ) β
((π β
(β€β₯β9) β§ π β Even ) β βπ β GoldbachOddW π = (π + 3))) |
2 | 1 | imp 408 |
. . 3
β’
((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β βπ β GoldbachOddW π = (π + 3)) |
3 | | simplll 774 |
. . . . . 6
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β βπ β Odd (5 < π β π β GoldbachOddW )) |
4 | | 6nn 12250 |
. . . . . . . . . . 11
β’ 6 β
β |
5 | 4 | nnzi 12535 |
. . . . . . . . . 10
β’ 6 β
β€ |
6 | 5 | a1i 11 |
. . . . . . . . 9
β’ (π β
(β€β₯β9) β 6 β β€) |
7 | | 3z 12544 |
. . . . . . . . . 10
β’ 3 β
β€ |
8 | 7 | a1i 11 |
. . . . . . . . 9
β’ (π β
(β€β₯β9) β 3 β β€) |
9 | | 6p3e9 12321 |
. . . . . . . . . . . . 13
β’ (6 + 3) =
9 |
10 | 9 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ 9 = (6 +
3) |
11 | 10 | fveq2i 6849 |
. . . . . . . . . . 11
β’
(β€β₯β9) = (β€β₯β(6 +
3)) |
12 | 11 | eleq2i 2826 |
. . . . . . . . . 10
β’ (π β
(β€β₯β9) β π β (β€β₯β(6 +
3))) |
13 | 12 | biimpi 215 |
. . . . . . . . 9
β’ (π β
(β€β₯β9) β π β (β€β₯β(6 +
3))) |
14 | | eluzsub 12801 |
. . . . . . . . 9
β’ ((6
β β€ β§ 3 β β€ β§ π β (β€β₯β(6 +
3))) β (π β 3)
β (β€β₯β6)) |
15 | 6, 8, 13, 14 | syl3anc 1372 |
. . . . . . . 8
β’ (π β
(β€β₯β9) β (π β 3) β
(β€β₯β6)) |
16 | 15 | adantr 482 |
. . . . . . 7
β’ ((π β
(β€β₯β9) β§ π β Even ) β (π β 3) β
(β€β₯β6)) |
17 | 16 | ad3antlr 730 |
. . . . . 6
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β (π β 3) β
(β€β₯β6)) |
18 | | 3odd 45990 |
. . . . . . . . . . . . 13
β’ 3 β
Odd |
19 | 18 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β
(β€β₯β9) β 3 β Odd ) |
20 | 19 | anim1i 616 |
. . . . . . . . . . 11
β’ ((π β
(β€β₯β9) β§ π β Even ) β (3 β Odd β§
π β Even
)) |
21 | 20 | adantl 483 |
. . . . . . . . . 10
β’
((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β (3 β Odd β§
π β Even
)) |
22 | 21 | ancomd 463 |
. . . . . . . . 9
β’
((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β (π β Even β§ 3 β Odd
)) |
23 | 22 | adantr 482 |
. . . . . . . 8
β’
(((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β (π β Even β§ 3 β Odd
)) |
24 | 23 | adantr 482 |
. . . . . . 7
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β (π β Even β§ 3 β Odd
)) |
25 | | emoo 45986 |
. . . . . . 7
β’ ((π β Even β§ 3 β Odd
) β (π β 3)
β Odd ) |
26 | 24, 25 | syl 17 |
. . . . . 6
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β (π β 3) β Odd ) |
27 | | nnsum4primesodd 46078 |
. . . . . . 7
β’
(βπ β
Odd (5 < π β π β GoldbachOddW ) β
(((π β 3) β
(β€β₯β6) β§ (π β 3) β Odd ) β βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ))) |
28 | 27 | imp 408 |
. . . . . 6
β’
((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
((π β 3) β
(β€β₯β6) β§ (π β 3) β Odd )) β
βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ)) |
29 | 3, 17, 26, 28 | syl12anc 836 |
. . . . 5
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β βπ β (β βm
(1...3))(π β 3) =
Ξ£π β
(1...3)(πβπ)) |
30 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β π:(1...3)βΆβ) |
31 | | 4z 12545 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
β€ |
32 | | fzonel 13595 |
. . . . . . . . . . . . . . . . . . 19
β’ Β¬ 4
β (1..^4) |
33 | | fzoval 13582 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
β€ β (1..^4) = (1...(4 β 1))) |
34 | 31, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1..^4) =
(1...(4 β 1)) |
35 | | 4cn 12246 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 4 β
β |
36 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 1 β
β |
37 | | 3cn 12242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 3 β
β |
38 | 35, 36, 37 | 3pm3.2i 1340 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (4 β
β β§ 1 β β β§ 3 β β) |
39 | | 3p1e4 12306 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (3 + 1) =
4 |
40 | | subadd2 11413 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((4
β β β§ 1 β β β§ 3 β β) β ((4
β 1) = 3 β (3 + 1) = 4)) |
41 | 39, 40 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((4
β β β§ 1 β β β§ 3 β β) β (4 β
1) = 3) |
42 | 38, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4
β 1) = 3 |
43 | 42 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1...(4
β 1)) = (1...3) |
44 | 34, 43 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1..^4) =
(1...3) |
45 | 44 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1...3) =
(1..^4) |
46 | 45 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . . 19
β’ (4 β
(1...3) β 4 β (1..^4)) |
47 | 32, 46 | mtbir 323 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬ 4
β (1...3) |
48 | 31, 47 | pm3.2i 472 |
. . . . . . . . . . . . . . . . 17
β’ (4 β
β€ β§ Β¬ 4 β (1...3)) |
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β (4 β
β€ β§ Β¬ 4 β (1...3))) |
50 | | 3prm 16578 |
. . . . . . . . . . . . . . . . 17
β’ 3 β
β |
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β 3 β
β) |
52 | | fsnunf 7135 |
. . . . . . . . . . . . . . . 16
β’ ((π:(1...3)βΆβ β§ (4
β β€ β§ Β¬ 4 β (1...3)) β§ 3 β β) β
(π βͺ {β¨4,
3β©}):((1...3) βͺ {4})βΆβ) |
53 | 30, 49, 51, 52 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β (π βͺ {β¨4,
3β©}):((1...3) βͺ {4})βΆβ) |
54 | | fzval3 13650 |
. . . . . . . . . . . . . . . . . 18
β’ (4 β
β€ β (1...4) = (1..^(4 + 1))) |
55 | 31, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (1...4) =
(1..^(4 + 1)) |
56 | | 1z 12541 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β€ |
57 | | 1re 11163 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 β
β |
58 | | 4re 12245 |
. . . . . . . . . . . . . . . . . . . 20
β’ 4 β
β |
59 | | 1lt4 12337 |
. . . . . . . . . . . . . . . . . . . 20
β’ 1 <
4 |
60 | 57, 58, 59 | ltleii 11286 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β€
4 |
61 | | eluz2 12777 |
. . . . . . . . . . . . . . . . . . 19
β’ (4 β
(β€β₯β1) β (1 β β€ β§ 4 β
β€ β§ 1 β€ 4)) |
62 | 56, 31, 60, 61 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . . 18
β’ 4 β
(β€β₯β1) |
63 | | fzosplitsn 13689 |
. . . . . . . . . . . . . . . . . 18
β’ (4 β
(β€β₯β1) β (1..^(4 + 1)) = ((1..^4) βͺ
{4})) |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (1..^(4 +
1)) = ((1..^4) βͺ {4}) |
65 | 44 | uneq1i 4123 |
. . . . . . . . . . . . . . . . 17
β’ ((1..^4)
βͺ {4}) = ((1...3) βͺ {4}) |
66 | 55, 64, 65 | 3eqtri 2765 |
. . . . . . . . . . . . . . . 16
β’ (1...4) =
((1...3) βͺ {4}) |
67 | 66 | feq2i 6664 |
. . . . . . . . . . . . . . 15
β’ ((π βͺ {β¨4,
3β©}):(1...4)βΆβ β (π βͺ {β¨4, 3β©}):((1...3) βͺ
{4})βΆβ) |
68 | 53, 67 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β (π βͺ {β¨4,
3β©}):(1...4)βΆβ) |
69 | | prmex 16561 |
. . . . . . . . . . . . . . . 16
β’ β
β V |
70 | | ovex 7394 |
. . . . . . . . . . . . . . . 16
β’ (1...4)
β V |
71 | 69, 70 | pm3.2i 472 |
. . . . . . . . . . . . . . 15
β’ (β
β V β§ (1...4) β V) |
72 | | elmapg 8784 |
. . . . . . . . . . . . . . 15
β’ ((β
β V β§ (1...4) β V) β ((π βͺ {β¨4, 3β©}) β (β
βm (1...4)) β (π βͺ {β¨4,
3β©}):(1...4)βΆβ)) |
73 | 71, 72 | mp1i 13 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π βͺ {β¨4, 3β©})
β (β βm (1...4)) β (π βͺ {β¨4,
3β©}):(1...4)βΆβ)) |
74 | 68, 73 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β (π βͺ {β¨4, 3β©})
β (β βm (1...4))) |
75 | 74 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β (π βͺ {β¨4, 3β©}) β (β
βm (1...4))) |
76 | | fveq1 6845 |
. . . . . . . . . . . . . . . 16
β’ (π = (π βͺ {β¨4, 3β©}) β (πβπ) = ((π βͺ {β¨4, 3β©})βπ)) |
77 | 76 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π = (π βͺ {β¨4, 3β©}) β§ π β (1...4)) β (πβπ) = ((π βͺ {β¨4, 3β©})βπ)) |
78 | 77 | sumeq2dv 15596 |
. . . . . . . . . . . . . 14
β’ (π = (π βͺ {β¨4, 3β©}) β
Ξ£π β
(1...4)(πβπ) = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ)) |
79 | 78 | eqeq2d 2744 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ {β¨4, 3β©}) β (π = Ξ£π β (1...4)(πβπ) β π = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ))) |
80 | 79 | adantl 483 |
. . . . . . . . . . . 12
β’ ((((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β§ π = (π βͺ {β¨4, 3β©})) β (π = Ξ£π β (1...4)(πβπ) β π = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ))) |
81 | 62 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β 4 β
(β€β₯β1)) |
82 | 66 | eleq2i 2826 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...4) β π β ((1...3) βͺ
{4})) |
83 | | elun 4112 |
. . . . . . . . . . . . . . . . . 18
β’ (π β ((1...3) βͺ {4})
β (π β (1...3)
β¨ π β
{4})) |
84 | | velsn 4606 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β {4} β π = 4) |
85 | 84 | orbi2i 912 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (1...3) β¨ π β {4}) β (π β (1...3) β¨ π = 4)) |
86 | 82, 83, 85 | 3bitri 297 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...4) β (π β (1...3) β¨ π = 4)) |
87 | | elfz2 13440 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β (1...3) β ((1
β β€ β§ 3 β β€ β§ π β β€) β§ (1 β€ π β§ π β€ 3))) |
88 | | 3re 12241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ 3 β
β |
89 | 88, 58 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (3 β
β β§ 4 β β) |
90 | | 3lt4 12335 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ 3 <
4 |
91 | | ltnle 11242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((3
β β β§ 4 β β) β (3 < 4 β Β¬ 4 β€
3)) |
92 | 90, 91 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((3
β β β§ 4 β β) β Β¬ 4 β€ 3) |
93 | 89, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ Β¬ 4
β€ 3 |
94 | | breq1 5112 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = 4 β (π β€ 3 β 4 β€ 3)) |
95 | 94 | eqcoms 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (4 =
π β (π β€ 3 β 4 β€
3)) |
96 | 93, 95 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (4 =
π β Β¬ π β€ 3) |
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β β€ β (4 =
π β Β¬ π β€ 3)) |
98 | 97 | necon2ad 2955 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β€ β (π β€ 3 β 4 β π)) |
99 | 98 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β€ β ((1 β€
π β§ π β€ 3) β 4 β π)) |
100 | 99 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((1
β β€ β§ 3 β β€ β§ π β β€) β ((1 β€ π β§ π β€ 3) β 4 β π)) |
101 | 100 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((1
β β€ β§ 3 β β€ β§ π β β€) β§ (1 β€ π β§ π β€ 3)) β 4 β π) |
102 | 87, 101 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...3) β 4 β
π) |
103 | 102 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
4 β π) |
104 | | fvunsn 7129 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (4 β
π β ((π βͺ {β¨4,
3β©})βπ) = (πβπ)) |
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
((π βͺ {β¨4,
3β©})βπ) = (πβπ)) |
106 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π:(1...3)βΆβ β§
π β (1...3)) β
(πβπ) β β) |
107 | 106 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
(πβπ) β β) |
108 | | prmz 16559 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((πβπ) β β β (πβπ) β β€) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
(πβπ) β β€) |
110 | 109 | zcnd 12616 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
(πβπ) β β) |
111 | 105, 110 | eqeltrd 2834 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
((π βͺ {β¨4,
3β©})βπ) β
β) |
112 | 111 | ex 414 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...3) β (π:(1...3)βΆβ β
((π βͺ {β¨4,
3β©})βπ) β
β)) |
113 | 112 | adantld 492 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...3) β ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
114 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = 4 β ((π βͺ {β¨4, 3β©})βπ) = ((π βͺ {β¨4,
3β©})β4)) |
115 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:(1...3)βΆβ β 4
β β€) |
116 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:(1...3)βΆβ β 3
β β€) |
117 | | fdm 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π:(1...3)βΆβ β
dom π =
(1...3)) |
118 | | eleq2 2823 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (dom
π = (1...3) β (4
β dom π β 4
β (1...3))) |
119 | 47, 118 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (dom
π = (1...3) β Β¬ 4
β dom π) |
120 | 117, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:(1...3)βΆβ β
Β¬ 4 β dom π) |
121 | | fsnunfv 7137 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((4
β β€ β§ 3 β β€ β§ Β¬ 4 β dom π) β ((π βͺ {β¨4, 3β©})β4) =
3) |
122 | 115, 116,
120, 121 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(1...3)βΆβ β
((π βͺ {β¨4,
3β©})β4) = 3) |
123 | 122 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})β4) = 3) |
124 | 114, 123 | sylan9eq 2793 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π = 4 β§ (π β (β€β₯β9)
β§ π:(1...3)βΆβ)) β ((π βͺ {β¨4,
3β©})βπ) =
3) |
125 | 124, 37 | eqeltrdi 2842 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = 4 β§ (π β (β€β₯β9)
β§ π:(1...3)βΆβ)) β ((π βͺ {β¨4,
3β©})βπ) β
β) |
126 | 125 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = 4 β ((π β (β€β₯β9)
β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
127 | 113, 126 | jaoi 856 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β (1...3) β¨ π = 4) β ((π β (β€β₯β9)
β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π β (1...3) β¨ π = 4) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
129 | 86, 128 | biimtrid 241 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β (π β (1...4) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
130 | 129 | imp 408 |
. . . . . . . . . . . . . . 15
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ π β (1...4)) β ((π βͺ {β¨4,
3β©})βπ) β
β) |
131 | 81, 130, 114 | fsumm1 15644 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β Ξ£π β (1...4)((π βͺ {β¨4,
3β©})βπ) =
(Ξ£π β (1...(4
β 1))((π βͺ
{β¨4, 3β©})βπ) + ((π βͺ {β¨4,
3β©})β4))) |
132 | 131 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ) = (Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ) +
((π βͺ {β¨4,
3β©})β4))) |
133 | 42 | eqcomi 2742 |
. . . . . . . . . . . . . . . . . . . 20
β’ 3 = (4
β 1) |
134 | 133 | oveq2i 7372 |
. . . . . . . . . . . . . . . . . . 19
β’ (1...3) =
(1...(4 β 1)) |
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β (1...3) =
(1...(4 β 1))) |
136 | 102 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ π β (1...3)) β 4 β
π) |
137 | 136, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ π β (1...3)) β ((π βͺ {β¨4,
3β©})βπ) = (πβπ)) |
138 | 137 | eqcomd 2739 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ π β (1...3)) β (πβπ) = ((π βͺ {β¨4, 3β©})βπ)) |
139 | 135, 138 | sumeq12dv 15599 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β Ξ£π β (1...3)(πβπ) = Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ)) |
140 | 139 | eqeq2d 2744 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π β 3) = Ξ£π β (1...3)(πβπ) β (π β 3) = Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ))) |
141 | 140 | biimpa 478 |
. . . . . . . . . . . . . . 15
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β (π β 3) = Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ)) |
142 | 141 | eqcomd 2739 |
. . . . . . . . . . . . . 14
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ) = (π β 3)) |
143 | 142 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β (Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ) +
((π βͺ {β¨4,
3β©})β4)) = ((π
β 3) + ((π βͺ
{β¨4, 3β©})β4))) |
144 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β 4 β
β€) |
145 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β 3 β
β€) |
146 | 120 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β Β¬ 4
β dom π) |
147 | 144, 145,
146, 121 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})β4) = 3) |
148 | 147 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π β 3) + ((π βͺ {β¨4,
3β©})β4)) = ((π
β 3) + 3)) |
149 | | eluzelcn 12783 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β9) β π β β) |
150 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯β9) β 3 β β) |
151 | 149, 150 | npcand 11524 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β9) β ((π β 3) + 3) = π) |
152 | 151 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π β 3) + 3) = π) |
153 | 148, 152 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π β 3) + ((π βͺ {β¨4,
3β©})β4)) = π) |
154 | 153 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β ((π β 3) + ((π βͺ {β¨4, 3β©})β4)) = π) |
155 | 132, 143,
154 | 3eqtrrd 2778 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β π = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ)) |
156 | 75, 80, 155 | rspcedvd 3585 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ)) |
157 | 156 | ex 414 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β9) β§ π:(1...3)βΆβ) β ((π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
158 | 157 | expcom 415 |
. . . . . . . . 9
β’ (π:(1...3)βΆβ β
(π β
(β€β₯β9) β ((π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ)))) |
159 | | elmapi 8793 |
. . . . . . . . 9
β’ (π β (β
βm (1...3)) β π:(1...3)βΆβ) |
160 | 158, 159 | syl11 33 |
. . . . . . . 8
β’ (π β
(β€β₯β9) β (π β (β βm (1...3))
β ((π β 3) =
Ξ£π β
(1...3)(πβπ) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ)))) |
161 | 160 | rexlimdv 3147 |
. . . . . . 7
β’ (π β
(β€β₯β9) β (βπ β (β βm
(1...3))(π β 3) =
Ξ£π β
(1...3)(πβπ) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ))) |
162 | 161 | adantr 482 |
. . . . . 6
β’ ((π β
(β€β₯β9) β§ π β Even ) β (βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
163 | 162 | ad3antlr 730 |
. . . . 5
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β (βπ β (β βm
(1...3))(π β 3) =
Ξ£π β
(1...3)(πβπ) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ))) |
164 | 29, 163 | mpd 15 |
. . . 4
β’
((((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β§ π β GoldbachOddW ) β§ π = (π + 3)) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ)) |
165 | 164 | rexlimdva2 3151 |
. . 3
β’
((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β (βπ β GoldbachOddW π = (π + 3) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
166 | 2, 165 | mpd 15 |
. 2
β’
((βπ β
Odd (5 < π β π β GoldbachOddW ) β§
(π β
(β€β₯β9) β§ π β Even )) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ)) |
167 | 166 | ex 414 |
1
β’
(βπ β
Odd (5 < π β π β GoldbachOddW ) β
((π β
(β€β₯β9) β§ π β Even ) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ))) |