Step | Hyp | Ref
| Expression |
1 | | simplll 774 |
. . . . 5
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β βπ β Odd (7 < π β π β GoldbachOdd )) |
2 | | 8nn 12255 |
. . . . . . . . . 10
β’ 8 β
β |
3 | 2 | nnzi 12534 |
. . . . . . . . 9
β’ 8 β
β€ |
4 | 3 | a1i 11 |
. . . . . . . 8
β’ (π β
(β€β₯β;12)
β 8 β β€) |
5 | | 3z 12543 |
. . . . . . . . 9
β’ 3 β
β€ |
6 | 5 | a1i 11 |
. . . . . . . 8
β’ (π β
(β€β₯β;12)
β 3 β β€) |
7 | 4, 6 | zaddcld 12618 |
. . . . . . . . 9
β’ (π β
(β€β₯β;12)
β (8 + 3) β β€) |
8 | | eluzelz 12780 |
. . . . . . . . 9
β’ (π β
(β€β₯β;12)
β π β
β€) |
9 | | eluz2 12776 |
. . . . . . . . . 10
β’ (π β
(β€β₯β;12)
β (;12 β β€ β§
π β β€ β§
;12 β€ π)) |
10 | | 8p4e12 12707 |
. . . . . . . . . . . . . 14
β’ (8 + 4) =
;12 |
11 | 10 | breq1i 5117 |
. . . . . . . . . . . . 13
β’ ((8 + 4)
β€ π β ;12 β€ π) |
12 | | 1nn0 12436 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β0 |
13 | | 2nn 12233 |
. . . . . . . . . . . . . . . 16
β’ 2 β
β |
14 | | 1lt2 12331 |
. . . . . . . . . . . . . . . 16
β’ 1 <
2 |
15 | 12, 12, 13, 14 | declt 12653 |
. . . . . . . . . . . . . . 15
β’ ;11 < ;12 |
16 | | 8p3e11 12706 |
. . . . . . . . . . . . . . 15
β’ (8 + 3) =
;11 |
17 | 15, 16, 10 | 3brtr4i 5140 |
. . . . . . . . . . . . . 14
β’ (8 + 3)
< (8 + 4) |
18 | | 8re 12256 |
. . . . . . . . . . . . . . . . 17
β’ 8 β
β |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β 8 β
β) |
20 | | 3re 12240 |
. . . . . . . . . . . . . . . . 17
β’ 3 β
β |
21 | 20 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β 3 β
β) |
22 | 19, 21 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β (8 + 3)
β β) |
23 | | 4re 12244 |
. . . . . . . . . . . . . . . . 17
β’ 4 β
β |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β β€ β 4 β
β) |
25 | 19, 24 | readdcld 11191 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β (8 + 4)
β β) |
26 | | zre 12510 |
. . . . . . . . . . . . . . 15
β’ (π β β€ β π β
β) |
27 | | ltleletr 11255 |
. . . . . . . . . . . . . . 15
β’ (((8 + 3)
β β β§ (8 + 4) β β β§ π β β) β (((8 + 3) < (8 +
4) β§ (8 + 4) β€ π)
β (8 + 3) β€ π)) |
28 | 22, 25, 26, 27 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (π β β€ β (((8 + 3)
< (8 + 4) β§ (8 + 4) β€ π) β (8 + 3) β€ π)) |
29 | 17, 28 | mpani 695 |
. . . . . . . . . . . . 13
β’ (π β β€ β ((8 + 4)
β€ π β (8 + 3) β€
π)) |
30 | 11, 29 | biimtrrid 242 |
. . . . . . . . . . . 12
β’ (π β β€ β (;12 β€ π β (8 + 3) β€ π)) |
31 | 30 | imp 408 |
. . . . . . . . . . 11
β’ ((π β β€ β§ ;12 β€ π) β (8 + 3) β€ π) |
32 | 31 | 3adant1 1131 |
. . . . . . . . . 10
β’ ((;12 β β€ β§ π β β€ β§ ;12 β€ π) β (8 + 3) β€ π) |
33 | 9, 32 | sylbi 216 |
. . . . . . . . 9
β’ (π β
(β€β₯β;12)
β (8 + 3) β€ π) |
34 | | eluz2 12776 |
. . . . . . . . 9
β’ (π β
(β€β₯β(8 + 3)) β ((8 + 3) β β€ β§
π β β€ β§ (8 +
3) β€ π)) |
35 | 7, 8, 33, 34 | syl3anbrc 1344 |
. . . . . . . 8
β’ (π β
(β€β₯β;12)
β π β
(β€β₯β(8 + 3))) |
36 | | eluzsub 12800 |
. . . . . . . 8
β’ ((8
β β€ β§ 3 β β€ β§ π β (β€β₯β(8 +
3))) β (π β 3)
β (β€β₯β8)) |
37 | 4, 6, 35, 36 | syl3anc 1372 |
. . . . . . 7
β’ (π β
(β€β₯β;12)
β (π β 3) β
(β€β₯β8)) |
38 | 37 | adantr 482 |
. . . . . 6
β’ ((π β
(β€β₯β;12)
β§ π β Even )
β (π β 3) β
(β€β₯β8)) |
39 | 38 | ad3antlr 730 |
. . . . 5
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β (π β 3) β
(β€β₯β8)) |
40 | | 3odd 45974 |
. . . . . . . . . . . 12
β’ 3 β
Odd |
41 | 40 | a1i 11 |
. . . . . . . . . . 11
β’ (π β
(β€β₯β;12)
β 3 β Odd ) |
42 | 41 | anim1i 616 |
. . . . . . . . . 10
β’ ((π β
(β€β₯β;12)
β§ π β Even )
β (3 β Odd β§ π β Even )) |
43 | 42 | adantl 483 |
. . . . . . . . 9
β’
((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β (3 β Odd β§ π β Even )) |
44 | 43 | ancomd 463 |
. . . . . . . 8
β’
((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β (π β Even β§
3 β Odd )) |
45 | 44 | adantr 482 |
. . . . . . 7
β’
(((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β (π β Even
β§ 3 β Odd )) |
46 | 45 | adantr 482 |
. . . . . 6
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β (π β Even β§ 3 β Odd
)) |
47 | | emoo 45970 |
. . . . . 6
β’ ((π β Even β§ 3 β Odd
) β (π β 3)
β Odd ) |
48 | 46, 47 | syl 17 |
. . . . 5
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β (π β 3) β Odd ) |
49 | | nnsum4primesoddALTV 46063 |
. . . . . 6
β’
(βπ β
Odd (7 < π β π β GoldbachOdd ) β
(((π β 3) β
(β€β₯β8) β§ (π β 3) β Odd ) β βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ))) |
50 | 49 | imp 408 |
. . . . 5
β’
((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
((π β 3) β
(β€β₯β8) β§ (π β 3) β Odd )) β
βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ)) |
51 | 1, 39, 48, 50 | syl12anc 836 |
. . . 4
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ)) |
52 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β π:(1...3)βΆβ) |
53 | | 4z 12544 |
. . . . . . . . . . . . . . . . 17
β’ 4 β
β€ |
54 | | fzonel 13593 |
. . . . . . . . . . . . . . . . . 18
β’ Β¬ 4
β (1..^4) |
55 | | fzoval 13580 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4 β
β€ β (1..^4) = (1...(4 β 1))) |
56 | 53, 55 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1..^4) =
(1...(4 β 1)) |
57 | | 4cn 12245 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 4 β
β |
58 | | ax-1cn 11116 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 β
β |
59 | | 3cn 12241 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 3 β
β |
60 | | 3p1e4 12305 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (3 + 1) =
4 |
61 | | subadd2 11412 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((4
β β β§ 1 β β β§ 3 β β) β ((4
β 1) = 3 β (3 + 1) = 4)) |
62 | 60, 61 | mpbiri 258 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((4
β β β§ 1 β β β§ 3 β β) β (4 β
1) = 3) |
63 | 57, 58, 59, 62 | mp3an 1462 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4
β 1) = 3 |
64 | 63 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (1...(4
β 1)) = (1...3) |
65 | 56, 64 | eqtri 2765 |
. . . . . . . . . . . . . . . . . . . 20
β’ (1..^4) =
(1...3) |
66 | 65 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . 19
β’ (1...3) =
(1..^4) |
67 | 66 | eleq2i 2830 |
. . . . . . . . . . . . . . . . . 18
β’ (4 β
(1...3) β 4 β (1..^4)) |
68 | 54, 67 | mtbir 323 |
. . . . . . . . . . . . . . . . 17
β’ Β¬ 4
β (1...3) |
69 | 53, 68 | pm3.2i 472 |
. . . . . . . . . . . . . . . 16
β’ (4 β
β€ β§ Β¬ 4 β (1...3)) |
70 | 69 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β (4 β
β€ β§ Β¬ 4 β (1...3))) |
71 | | 3prm 16577 |
. . . . . . . . . . . . . . . 16
β’ 3 β
β |
72 | 71 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β 3 β
β) |
73 | | fsnunf 7136 |
. . . . . . . . . . . . . . 15
β’ ((π:(1...3)βΆβ β§ (4
β β€ β§ Β¬ 4 β (1...3)) β§ 3 β β) β
(π βͺ {β¨4,
3β©}):((1...3) βͺ {4})βΆβ) |
74 | 52, 70, 72, 73 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β (π βͺ {β¨4,
3β©}):((1...3) βͺ {4})βΆβ) |
75 | | fzval3 13648 |
. . . . . . . . . . . . . . . . 17
β’ (4 β
β€ β (1...4) = (1..^(4 + 1))) |
76 | 53, 75 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (1...4) =
(1..^(4 + 1)) |
77 | | 1z 12540 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β€ |
78 | | 1re 11162 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 β
β |
79 | | 1lt4 12336 |
. . . . . . . . . . . . . . . . . . 19
β’ 1 <
4 |
80 | 78, 23, 79 | ltleii 11285 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β€
4 |
81 | | eluz2 12776 |
. . . . . . . . . . . . . . . . . 18
β’ (4 β
(β€β₯β1) β (1 β β€ β§ 4 β
β€ β§ 1 β€ 4)) |
82 | 77, 53, 80, 81 | mpbir3an 1342 |
. . . . . . . . . . . . . . . . 17
β’ 4 β
(β€β₯β1) |
83 | | fzosplitsn 13687 |
. . . . . . . . . . . . . . . . 17
β’ (4 β
(β€β₯β1) β (1..^(4 + 1)) = ((1..^4) βͺ
{4})) |
84 | 82, 83 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
β’ (1..^(4 +
1)) = ((1..^4) βͺ {4}) |
85 | 65 | uneq1i 4124 |
. . . . . . . . . . . . . . . 16
β’ ((1..^4)
βͺ {4}) = ((1...3) βͺ {4}) |
86 | 76, 84, 85 | 3eqtri 2769 |
. . . . . . . . . . . . . . 15
β’ (1...4) =
((1...3) βͺ {4}) |
87 | 86 | feq2i 6665 |
. . . . . . . . . . . . . 14
β’ ((π βͺ {β¨4,
3β©}):(1...4)βΆβ β (π βͺ {β¨4, 3β©}):((1...3) βͺ
{4})βΆβ) |
88 | 74, 87 | sylibr 233 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β (π βͺ {β¨4,
3β©}):(1...4)βΆβ) |
89 | | prmex 16560 |
. . . . . . . . . . . . . . 15
β’ β
β V |
90 | | ovex 7395 |
. . . . . . . . . . . . . . 15
β’ (1...4)
β V |
91 | 89, 90 | pm3.2i 472 |
. . . . . . . . . . . . . 14
β’ (β
β V β§ (1...4) β V) |
92 | | elmapg 8785 |
. . . . . . . . . . . . . 14
β’ ((β
β V β§ (1...4) β V) β ((π βͺ {β¨4, 3β©}) β (β
βm (1...4)) β (π βͺ {β¨4,
3β©}):(1...4)βΆβ)) |
93 | 91, 92 | mp1i 13 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π βͺ {β¨4, 3β©})
β (β βm (1...4)) β (π βͺ {β¨4,
3β©}):(1...4)βΆβ)) |
94 | 88, 93 | mpbird 257 |
. . . . . . . . . . . 12
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β (π βͺ {β¨4, 3β©})
β (β βm (1...4))) |
95 | 94 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β (π βͺ {β¨4, 3β©}) β (β
βm (1...4))) |
96 | | fveq1 6846 |
. . . . . . . . . . . . . 14
β’ (π = (π βͺ {β¨4, 3β©}) β (πβπ) = ((π βͺ {β¨4, 3β©})βπ)) |
97 | 96 | sumeq2sdv 15596 |
. . . . . . . . . . . . 13
β’ (π = (π βͺ {β¨4, 3β©}) β
Ξ£π β
(1...4)(πβπ) = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ)) |
98 | 97 | eqeq2d 2748 |
. . . . . . . . . . . 12
β’ (π = (π βͺ {β¨4, 3β©}) β (π = Ξ£π β (1...4)(πβπ) β π = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ))) |
99 | 98 | adantl 483 |
. . . . . . . . . . 11
β’ ((((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β§ π = (π βͺ {β¨4, 3β©})) β (π = Ξ£π β (1...4)(πβπ) β π = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ))) |
100 | 82 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β 4 β
(β€β₯β1)) |
101 | 86 | eleq2i 2830 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...4) β π β ((1...3) βͺ
{4})) |
102 | | elun 4113 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((1...3) βͺ {4})
β (π β (1...3)
β¨ π β
{4})) |
103 | | velsn 4607 |
. . . . . . . . . . . . . . . . . 18
β’ (π β {4} β π = 4) |
104 | 103 | orbi2i 912 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...3) β¨ π β {4}) β (π β (1...3) β¨ π = 4)) |
105 | 101, 102,
104 | 3bitri 297 |
. . . . . . . . . . . . . . . 16
β’ (π β (1...4) β (π β (1...3) β¨ π = 4)) |
106 | | elfz2 13438 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (1...3) β ((1
β β€ β§ 3 β β€ β§ π β β€) β§ (1 β€ π β§ π β€ 3))) |
107 | 20, 23 | pm3.2i 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (3 β
β β§ 4 β β) |
108 | | 3lt4 12334 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ 3 <
4 |
109 | | ltnle 11241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((3
β β β§ 4 β β) β (3 < 4 β Β¬ 4 β€
3)) |
110 | 108, 109 | mpbii 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((3
β β β§ 4 β β) β Β¬ 4 β€ 3) |
111 | 107, 110 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ Β¬ 4
β€ 3 |
112 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = 4 β (π β€ 3 β 4 β€ 3)) |
113 | 112 | eqcoms 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (4 =
π β (π β€ 3 β 4 β€
3)) |
114 | 111, 113 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (4 =
π β Β¬ π β€ 3) |
115 | 114 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β β€ β (4 =
π β Β¬ π β€ 3)) |
116 | 115 | necon2ad 2959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β β€ β (π β€ 3 β 4 β π)) |
117 | 116 | adantld 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β β€ β ((1 β€
π β§ π β€ 3) β 4 β π)) |
118 | 117 | 3ad2ant3 1136 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((1
β β€ β§ 3 β β€ β§ π β β€) β ((1 β€ π β§ π β€ 3) β 4 β π)) |
119 | 118 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((1
β β€ β§ 3 β β€ β§ π β β€) β§ (1 β€ π β§ π β€ 3)) β 4 β π) |
120 | 106, 119 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (1...3) β 4 β
π) |
121 | 120 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
4 β π) |
122 | | fvunsn 7130 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (4 β
π β ((π βͺ {β¨4,
3β©})βπ) = (πβπ)) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
((π βͺ {β¨4,
3β©})βπ) = (πβπ)) |
124 | | ffvelcdm 7037 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π:(1...3)βΆβ β§
π β (1...3)) β
(πβπ) β β) |
125 | 124 | ancoms 460 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
(πβπ) β β) |
126 | | prmz 16558 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((πβπ) β β β (πβπ) β β€) |
127 | 125, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
(πβπ) β β€) |
128 | 127 | zcnd 12615 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
(πβπ) β β) |
129 | 123, 128 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β (1...3) β§ π:(1...3)βΆβ) β
((π βͺ {β¨4,
3β©})βπ) β
β) |
130 | 129 | ex 414 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...3) β (π:(1...3)βΆβ β
((π βͺ {β¨4,
3β©})βπ) β
β)) |
131 | 130 | adantld 492 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (1...3) β ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
132 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = 4 β ((π βͺ {β¨4, 3β©})βπ) = ((π βͺ {β¨4,
3β©})β4)) |
133 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(1...3)βΆβ β 4
β β€) |
134 | 5 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(1...3)βΆβ β 3
β β€) |
135 | | fdm 6682 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π:(1...3)βΆβ β
dom π =
(1...3)) |
136 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (dom
π = (1...3) β (4
β dom π β 4
β (1...3))) |
137 | 68, 136 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (dom
π = (1...3) β Β¬ 4
β dom π) |
138 | 135, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π:(1...3)βΆβ β
Β¬ 4 β dom π) |
139 | | fsnunfv 7138 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((4
β β€ β§ 3 β β€ β§ Β¬ 4 β dom π) β ((π βͺ {β¨4, 3β©})β4) =
3) |
140 | 133, 134,
138, 139 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π:(1...3)βΆβ β
((π βͺ {β¨4,
3β©})β4) = 3) |
141 | 140 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})β4) = 3) |
142 | 132, 141 | sylan9eq 2797 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π = 4 β§ (π β (β€β₯β;12) β§ π:(1...3)βΆβ)) β ((π βͺ {β¨4,
3β©})βπ) =
3) |
143 | 142, 59 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π = 4 β§ (π β (β€β₯β;12) β§ π:(1...3)βΆβ)) β ((π βͺ {β¨4,
3β©})βπ) β
β) |
144 | 143 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’ (π = 4 β ((π β (β€β₯β;12) β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
145 | 131, 144 | jaoi 856 |
. . . . . . . . . . . . . . . . 17
β’ ((π β (1...3) β¨ π = 4) β ((π β (β€β₯β;12) β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
146 | 145 | com12 32 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π β (1...3) β¨ π = 4) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
147 | 105, 146 | biimtrid 241 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β (π β (1...4) β ((π βͺ {β¨4,
3β©})βπ) β
β)) |
148 | 147 | imp 408 |
. . . . . . . . . . . . . 14
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ π β (1...4)) β ((π βͺ {β¨4,
3β©})βπ) β
β) |
149 | 100, 148,
132 | fsumm1 15643 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β Ξ£π β (1...4)((π βͺ {β¨4,
3β©})βπ) =
(Ξ£π β (1...(4
β 1))((π βͺ
{β¨4, 3β©})βπ) + ((π βͺ {β¨4,
3β©})β4))) |
150 | 149 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ) = (Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ) +
((π βͺ {β¨4,
3β©})β4))) |
151 | 63 | eqcomi 2746 |
. . . . . . . . . . . . . . . . . . 19
β’ 3 = (4
β 1) |
152 | 151 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . 18
β’ (1...3) =
(1...(4 β 1)) |
153 | 152 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β (1...3) =
(1...(4 β 1))) |
154 | 120 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ π β (1...3)) β 4 β
π) |
155 | 154, 122 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ π β (1...3)) β ((π βͺ {β¨4,
3β©})βπ) = (πβπ)) |
156 | 155 | eqcomd 2743 |
. . . . . . . . . . . . . . . . 17
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ π β (1...3)) β (πβπ) = ((π βͺ {β¨4, 3β©})βπ)) |
157 | 153, 156 | sumeq12dv 15598 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β Ξ£π β (1...3)(πβπ) = Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ)) |
158 | 157 | eqeq2d 2748 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π β 3) = Ξ£π β (1...3)(πβπ) β (π β 3) = Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ))) |
159 | 158 | biimpa 478 |
. . . . . . . . . . . . . 14
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β (π β 3) = Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ)) |
160 | 159 | eqcomd 2743 |
. . . . . . . . . . . . 13
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ) = (π β 3)) |
161 | 160 | oveq1d 7377 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β (Ξ£π β (1...(4 β 1))((π βͺ {β¨4,
3β©})βπ) +
((π βͺ {β¨4,
3β©})β4)) = ((π
β 3) + ((π βͺ
{β¨4, 3β©})β4))) |
162 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β 4 β
β€) |
163 | 5 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β 3 β
β€) |
164 | 138 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β Β¬ 4
β dom π) |
165 | 162, 163,
164, 139 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π βͺ {β¨4,
3β©})β4) = 3) |
166 | 165 | oveq2d 7378 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π β 3) + ((π βͺ {β¨4,
3β©})β4)) = ((π
β 3) + 3)) |
167 | | eluzelcn 12782 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β;12)
β π β
β) |
168 | 59 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π β
(β€β₯β;12)
β 3 β β) |
169 | 167, 168 | npcand 11523 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β;12)
β ((π β 3) + 3)
= π) |
170 | 169 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π β 3) + 3) = π) |
171 | 166, 170 | eqtrd 2777 |
. . . . . . . . . . . . 13
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π β 3) + ((π βͺ {β¨4,
3β©})β4)) = π) |
172 | 171 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β ((π β 3) + ((π βͺ {β¨4, 3β©})β4)) = π) |
173 | 150, 161,
172 | 3eqtrrd 2782 |
. . . . . . . . . . 11
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β π = Ξ£π β (1...4)((π βͺ {β¨4, 3β©})βπ)) |
174 | 95, 99, 173 | rspcedvd 3586 |
. . . . . . . . . 10
β’ (((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β§ (π β 3) = Ξ£π β (1...3)(πβπ)) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ)) |
175 | 174 | ex 414 |
. . . . . . . . 9
β’ ((π β
(β€β₯β;12)
β§ π:(1...3)βΆβ) β ((π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
176 | 175 | expcom 415 |
. . . . . . . 8
β’ (π:(1...3)βΆβ β
(π β
(β€β₯β;12)
β ((π β 3) =
Ξ£π β
(1...3)(πβπ) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ)))) |
177 | | elmapi 8794 |
. . . . . . . 8
β’ (π β (β
βm (1...3)) β π:(1...3)βΆβ) |
178 | 176, 177 | syl11 33 |
. . . . . . 7
β’ (π β
(β€β₯β;12)
β (π β (β
βm (1...3)) β ((π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ)))) |
179 | 178 | rexlimdv 3151 |
. . . . . 6
β’ (π β
(β€β₯β;12)
β (βπ β
(β βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
180 | 179 | adantr 482 |
. . . . 5
β’ ((π β
(β€β₯β;12)
β§ π β Even )
β (βπ β
(β βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
181 | 180 | ad3antlr 730 |
. . . 4
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β (βπ β (β
βm (1...3))(π β 3) = Ξ£π β (1...3)(πβπ) β βπ β (β βm
(1...4))π = Ξ£π β (1...4)(πβπ))) |
182 | 51, 181 | mpd 15 |
. . 3
β’
((((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β§ π β GoldbachOdd
) β§ π = (π + 3)) β βπ β (β
βm (1...4))π = Ξ£π β (1...4)(πβπ)) |
183 | | evengpoap3 46065 |
. . . 4
β’
(βπ β
Odd (7 < π β π β GoldbachOdd ) β
((π β
(β€β₯β;12)
β§ π β Even )
β βπ β
GoldbachOdd π = (π + 3))) |
184 | 183 | imp 408 |
. . 3
β’
((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β βπ β
GoldbachOdd π = (π + 3)) |
185 | 182, 184 | r19.29a 3160 |
. 2
β’
((βπ β
Odd (7 < π β π β GoldbachOdd ) β§
(π β
(β€β₯β;12)
β§ π β Even ))
β βπ β
(β βm (1...4))π = Ξ£π β (1...4)(πβπ)) |
186 | 185 | ex 414 |
1
β’
(βπ β
Odd (7 < π β π β GoldbachOdd ) β
((π β
(β€β₯β;12)
β§ π β Even )
β βπ β
(β βm (1...4))π = Ξ£π β (1...4)(πβπ))) |