Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . 3
β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β π) |
2 | | simpr 486 |
. . 3
β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β π β Odd ) |
3 | | simplr 768 |
. . 3
β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β πΌ β (1..^π·)) |
4 | | bgoldbtbnd.m |
. . . 4
β’ (π β π β (β€β₯β;11)) |
5 | | bgoldbtbnd.n |
. . . 4
β’ (π β π β (β€β₯β;11)) |
6 | | bgoldbtbnd.b |
. . . 4
β’ (π β βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) |
7 | | bgoldbtbnd.d |
. . . 4
β’ (π β π· β
(β€β₯β3)) |
8 | | bgoldbtbnd.f |
. . . 4
β’ (π β πΉ β (RePartβπ·)) |
9 | | bgoldbtbnd.i |
. . . 4
β’ (π β βπ β (0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ)))) |
10 | | bgoldbtbnd.0 |
. . . 4
β’ (π β (πΉβ0) = 7) |
11 | | bgoldbtbnd.1 |
. . . 4
β’ (π β (πΉβ1) = ;13) |
12 | | bgoldbtbnd.l |
. . . 4
β’ (π β π < (πΉβπ·)) |
13 | | eqid 2732 |
. . . 4
β’ (π β (πΉβ(πΌ β 1))) = (π β (πΉβ(πΌ β 1))) |
14 | 4, 5, 6, 7, 8, 9, 10, 11, 12, 13 | bgoldbtbndlem2 46100 |
. . 3
β’ ((π β§ π β Odd β§ πΌ β (1..^π·)) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β ((π β (πΉβ(πΌ β 1))) β Even β§ (π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))))) |
15 | 1, 2, 3, 14 | syl3anc 1372 |
. 2
β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β ((π β (πΉβ(πΌ β 1))) β Even β§ (π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))))) |
16 | | breq2 5115 |
. . . . . . . . . . . 12
β’ (π = π β (4 < π β 4 < π)) |
17 | | breq1 5114 |
. . . . . . . . . . . 12
β’ (π = π β (π < π β π < π)) |
18 | 16, 17 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = π β ((4 < π β§ π < π) β (4 < π β§ π < π))) |
19 | | eleq1 2821 |
. . . . . . . . . . 11
β’ (π = π β (π β GoldbachEven β π β GoldbachEven
)) |
20 | 18, 19 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = π β (((4 < π β§ π < π) β π β GoldbachEven ) β ((4 < π β§ π < π) β π β GoldbachEven ))) |
21 | 20 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ β
Even ((4 < π β§ π < π) β π β GoldbachEven ) β βπ β Even ((4 < π β§ π < π) β π β GoldbachEven )) |
22 | | breq2 5115 |
. . . . . . . . . . . 12
β’ (π = (π β (πΉβ(πΌ β 1))) β (4 < π β 4 < (π β (πΉβ(πΌ β 1))))) |
23 | | breq1 5114 |
. . . . . . . . . . . 12
β’ (π = (π β (πΉβ(πΌ β 1))) β (π < π β (π β (πΉβ(πΌ β 1))) < π)) |
24 | 22, 23 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = (π β (πΉβ(πΌ β 1))) β ((4 < π β§ π < π) β (4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π))) |
25 | | eleq1 2821 |
. . . . . . . . . . 11
β’ (π = (π β (πΉβ(πΌ β 1))) β (π β GoldbachEven β (π β (πΉβ(πΌ β 1))) β GoldbachEven
)) |
26 | 24, 25 | imbi12d 345 |
. . . . . . . . . 10
β’ (π = (π β (πΉβ(πΌ β 1))) β (((4 < π β§ π < π) β π β GoldbachEven ) β ((4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven
))) |
27 | 26 | rspcv 3579 |
. . . . . . . . 9
β’ ((π β (πΉβ(πΌ β 1))) β Even β
(βπ β Even ((4
< π β§ π < π) β π β GoldbachEven ) β ((4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven
))) |
28 | 21, 27 | biimtrid 241 |
. . . . . . . 8
β’ ((π β (πΉβ(πΌ β 1))) β Even β
(βπ β Even ((4
< π β§ π < π) β π β GoldbachEven ) β ((4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven
))) |
29 | | id 22 |
. . . . . . . . . . 11
β’ (((4 <
(π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven ) β
((4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven
)) |
30 | | isgbe 46045 |
. . . . . . . . . . . . 13
β’ ((π β (πΉβ(πΌ β 1))) β GoldbachEven β
((π β (πΉβ(πΌ β 1))) β Even β§ βπ β β βπ β β (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)))) |
31 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (πΉβπ) β (β β
{2})) |
32 | 31 | ralimi 3083 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
(0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β βπ β (0..^π·)(πΉβπ) β (β β
{2})) |
33 | | elfzo1 13633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (πΌ β (1..^π·) β (πΌ β β β§ π· β β β§ πΌ < π·)) |
34 | | nnm1nn0 12464 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (πΌ β β β (πΌ β 1) β
β0) |
35 | 34 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((πΌ β β β§ π· β β β§ πΌ < π·) β (πΌ β 1) β
β0) |
36 | 33, 35 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (πΌ β (1..^π·) β (πΌ β 1) β
β0) |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π· β
(β€β₯β3) β (πΌ β (1..^π·) β (πΌ β 1) β
β0)) |
38 | | eluzge3nn 12825 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π· β
(β€β₯β3) β π· β β) |
39 | 38 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π· β
(β€β₯β3) β (πΌ β (1..^π·) β π· β β)) |
40 | | elfzo2 13586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (πΌ β (1..^π·) β (πΌ β (β€β₯β1)
β§ π· β β€
β§ πΌ < π·)) |
41 | | eluzelre 12784 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (πΌ β
(β€β₯β1) β πΌ β β) |
42 | 41 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β πΌ β β) |
43 | 42 | ltm1d 12097 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β (πΌ β 1) < πΌ) |
44 | | 1red 11166 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β 1 β
β) |
45 | 42, 44 | resubcld 11593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β (πΌ β 1) β β) |
46 | | zre 12513 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π· β β€ β π· β
β) |
47 | 46 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β π· β β) |
48 | | lttr 11241 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ (((πΌ β 1) β β β§
πΌ β β β§
π· β β) β
(((πΌ β 1) < πΌ β§ πΌ < π·) β (πΌ β 1) < π·)) |
49 | 45, 42, 47, 48 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β (((πΌ β 1) < πΌ β§ πΌ < π·) β (πΌ β 1) < π·)) |
50 | 43, 49 | mpand 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΌ β
(β€β₯β1) β§ π· β β€) β (πΌ < π· β (πΌ β 1) < π·)) |
51 | 50 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((πΌ β
(β€β₯β1) β§ π· β β€ β§ πΌ < π·) β (πΌ β 1) < π·) |
52 | 40, 51 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (πΌ β (1..^π·) β (πΌ β 1) < π·) |
53 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π· β
(β€β₯β3) β (πΌ β (1..^π·) β (πΌ β 1) < π·)) |
54 | 37, 39, 53 | 3jcad 1130 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π· β
(β€β₯β3) β (πΌ β (1..^π·) β ((πΌ β 1) β β0 β§
π· β β β§
(πΌ β 1) < π·))) |
55 | 7, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β (πΌ β (1..^π·) β ((πΌ β 1) β β0 β§
π· β β β§
(πΌ β 1) < π·))) |
56 | 55 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π β§ πΌ β (1..^π·)) β ((πΌ β 1) β β0 β§
π· β β β§
(πΌ β 1) < π·)) |
57 | | elfzo0 13624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΌ β 1) β (0..^π·) β ((πΌ β 1) β β0 β§
π· β β β§
(πΌ β 1) < π·)) |
58 | 56, 57 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ πΌ β (1..^π·)) β (πΌ β 1) β (0..^π·)) |
59 | | fveq2 6848 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π = (πΌ β 1) β (πΉβπ) = (πΉβ(πΌ β 1))) |
60 | 59 | eleq1d 2818 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = (πΌ β 1) β ((πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β (β β
{2}))) |
61 | 60 | rspcv 3579 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((πΌ β 1) β (0..^π·) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β (β β
{2}))) |
62 | 58, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β (β β
{2}))) |
63 | | eldifi 4092 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (πΉβ(πΌ β 1)) β
β) |
64 | 62, 63 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β
β)) |
65 | 64 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (πΌ β (1..^π·) β (π β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β
β))) |
66 | 65 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
(0..^π·)(πΉβπ) β (β β {2}) β (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β))) |
67 | 32, 66 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β))) |
68 | 9, 67 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β)) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β (πΉβ(πΌ β 1))) β Even β§ π) β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β)) |
70 | 69 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β (πΉβ(πΌ β 1)) β
β) |
71 | 70 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β (πΉβ(πΌ β 1)) β
β) |
72 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β (πΉβ(πΌ β 1)) β
β) |
73 | | eleq1 2821 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πΉβ(πΌ β 1)) β (π β Odd β (πΉβ(πΌ β 1)) β Odd )) |
74 | 73 | 3anbi3d 1443 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πΉβ(πΌ β 1)) β ((π β Odd β§ π β Odd β§ π β Odd ) β (π β Odd β§ π β Odd β§ (πΉβ(πΌ β 1)) β Odd ))) |
75 | | oveq2 7371 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = (πΉβ(πΌ β 1)) β ((π + π) + π) = ((π + π) + (πΉβ(πΌ β 1)))) |
76 | 75 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (πΉβ(πΌ β 1)) β (π = ((π + π) + π) β π = ((π + π) + (πΉβ(πΌ β 1))))) |
77 | 74, 76 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (πΉβ(πΌ β 1)) β (((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)) β ((π β Odd β§ π β Odd β§ (πΉβ(πΌ β 1)) β Odd ) β§ π = ((π + π) + (πΉβ(πΌ β 1)))))) |
78 | 77 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’
(((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β§ π = (πΉβ(πΌ β 1))) β (((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)) β ((π β Odd β§ π β Odd β§ (πΉβ(πΌ β 1)) β Odd ) β§ π = ((π + π) + (πΉβ(πΌ β 1)))))) |
79 | | oddprmALTV 45981 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (πΉβ(πΌ β 1)) β Odd
) |
80 | 62, 79 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β Odd )) |
81 | 80 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (πΌ β (1..^π·) β (π β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β Odd ))) |
82 | 81 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
(0..^π·)(πΉβπ) β (β β {2}) β (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β Odd ))) |
83 | 32, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
(0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β Odd ))) |
84 | 9, 83 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β Odd )) |
85 | 84 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β (πΉβ(πΌ β 1))) β Even β§ π) β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β Odd )) |
86 | 85 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β (πΉβ(πΌ β 1)) β Odd ) |
87 | 86 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β (πΉβ(πΌ β 1)) β Odd ) |
88 | | 3simpa 1149 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β (π β Odd β§ π β Odd )) |
89 | 87, 88 | anim12ci 615 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β ((π β Odd β§ π β Odd ) β§ (πΉβ(πΌ β 1)) β Odd )) |
90 | | df-3an 1090 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Odd β§ π β Odd β§ (πΉβ(πΌ β 1)) β Odd ) β ((π β Odd β§ π β Odd ) β§ (πΉβ(πΌ β 1)) β Odd )) |
91 | 89, 90 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β (π β Odd β§ π β Odd β§ (πΉβ(πΌ β 1)) β Odd )) |
92 | | oddz 45925 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β Odd β π β
β€) |
93 | 92 | zcnd 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β Odd β π β
β) |
94 | 93 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β π β β) |
95 | 94 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β π β β) |
96 | 95 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Odd β§ π β Odd ) β§ ((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β)) β π β β) |
97 | | prmz 16563 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((πΉβ(πΌ β 1)) β β β (πΉβ(πΌ β 1)) β
β€) |
98 | 97 | zcnd 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((πΉβ(πΌ β 1)) β β β (πΉβ(πΌ β 1)) β
β) |
99 | 63, 98 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((πΉβ(πΌ β 1)) β (β β {2})
β (πΉβ(πΌ β 1)) β
β) |
100 | 62, 99 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β§ πΌ β (1..^π·)) β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β
β)) |
101 | 100 | expcom 415 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (πΌ β (1..^π·) β (π β (βπ β (0..^π·)(πΉβπ) β (β β {2}) β (πΉβ(πΌ β 1)) β
β))) |
102 | 101 | com13 88 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(βπ β
(0..^π·)(πΉβπ) β (β β {2}) β (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β))) |
103 | 32, 102 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(βπ β
(0..^π·)((πΉβπ) β (β β {2}) β§ ((πΉβ(π + 1)) β (πΉβπ)) < (π β 4) β§ 4 < ((πΉβ(π + 1)) β (πΉβπ))) β (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β))) |
104 | 9, 103 | mpcom 38 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β)) |
105 | 104 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (((π β (πΉβ(πΌ β 1))) β Even β§ π) β (πΌ β (1..^π·) β (πΉβ(πΌ β 1)) β
β)) |
106 | 105 | imp 408 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β (πΉβ(πΌ β 1)) β
β) |
107 | 106 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β (πΉβ(πΌ β 1)) β
β) |
108 | 107 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((π β Odd β§ π β Odd ) β§ ((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β)) β (πΉβ(πΌ β 1)) β
β) |
109 | 96, 108 | npcand 11526 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π β Odd β§ π β Odd ) β§ ((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β)) β ((π β (πΉβ(πΌ β 1))) + (πΉβ(πΌ β 1))) = π) |
110 | | oveq1 7370 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β (πΉβ(πΌ β 1))) = (π + π) β ((π β (πΉβ(πΌ β 1))) + (πΉβ(πΌ β 1))) = ((π + π) + (πΉβ(πΌ β 1)))) |
111 | 109, 110 | sylan9req 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π β Odd β§ π β Odd ) β§ ((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β)) β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β π = ((π + π) + (πΉβ(πΌ β 1)))) |
112 | 111 | exp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β Odd β§ π β Odd ) β
(((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β ((π β (πΉβ(πΌ β 1))) = (π + π) β π = ((π + π) + (πΉβ(πΌ β 1)))))) |
113 | 112 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Odd β§ π β Odd ) β ((π β (πΉβ(πΌ β 1))) = (π + π) β (((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β π = ((π + π) + (πΉβ(πΌ β 1)))))) |
114 | 113 | 3impia 1118 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β (((((((π β (πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β π = ((π + π) + (πΉβ(πΌ β 1))))) |
115 | 114 | impcom 409 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β π = ((π + π) + (πΉβ(πΌ β 1)))) |
116 | 91, 115 | jca 513 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β ((π β Odd β§ π β Odd β§ (πΉβ(πΌ β 1)) β Odd ) β§ π = ((π + π) + (πΉβ(πΌ β 1))))) |
117 | 72, 78, 116 | rspcedvd 3585 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β§ (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))) |
118 | 117 | ex 414 |
. . . . . . . . . . . . . . . . . 18
β’
(((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β§ π β β) β ((π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) |
119 | 118 | reximdva 3162 |
. . . . . . . . . . . . . . . . 17
β’
((((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β§ π β β) β (βπ β β (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) |
120 | 119 | reximdva 3162 |
. . . . . . . . . . . . . . . 16
β’
(((((π β
(πΉβ(πΌ β 1))) β Even β§ π) β§ πΌ β (1..^π·)) β§ π β Odd ) β (βπ β β βπ β β (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) |
121 | 120 | exp41 436 |
. . . . . . . . . . . . . . 15
β’ ((π β (πΉβ(πΌ β 1))) β Even β (π β (πΌ β (1..^π·) β (π β Odd β (βπ β β βπ β β (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))))))) |
122 | 121 | com25 99 |
. . . . . . . . . . . . . 14
β’ ((π β (πΉβ(πΌ β 1))) β Even β
(βπ β β
βπ β β
(π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π)) β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))))))) |
123 | 122 | imp 408 |
. . . . . . . . . . . . 13
β’ (((π β (πΉβ(πΌ β 1))) β Even β§ βπ β β βπ β β (π β Odd β§ π β Odd β§ (π β (πΉβ(πΌ β 1))) = (π + π))) β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))) |
124 | 30, 123 | sylbi 216 |
. . . . . . . . . . . 12
β’ ((π β (πΉβ(πΌ β 1))) β GoldbachEven β
(πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))) |
125 | 124 | a1d 25 |
. . . . . . . . . . 11
β’ ((π β (πΉβ(πΌ β 1))) β GoldbachEven β
((π β (πΉβ(πΌ β 1))) β Even β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))))))) |
126 | 29, 125 | syl6com 37 |
. . . . . . . . . 10
β’ ((4 <
(π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (((4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven ) β
((π β (πΉβ(πΌ β 1))) β Even β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))))) |
127 | 126 | ancoms 460 |
. . . . . . . . 9
β’ (((π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β (((4 < (π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven ) β
((π β (πΉβ(πΌ β 1))) β Even β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))))) |
128 | 127 | com13 88 |
. . . . . . . 8
β’ ((π β (πΉβ(πΌ β 1))) β Even β (((4 <
(π β (πΉβ(πΌ β 1))) β§ (π β (πΉβ(πΌ β 1))) < π) β (π β (πΉβ(πΌ β 1))) β GoldbachEven ) β
(((π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))))) |
129 | 28, 128 | syld 47 |
. . . . . . 7
β’ ((π β (πΉβ(πΌ β 1))) β Even β
(βπ β Even ((4
< π β§ π < π) β π β GoldbachEven ) β (((π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))))) |
130 | 129 | com23 86 |
. . . . . 6
β’ ((π β (πΉβ(πΌ β 1))) β Even β (((π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β (βπ β Even ((4 < π β§ π < π) β π β GoldbachEven ) β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))))) |
131 | 130 | 3impib 1117 |
. . . . 5
β’ (((π β (πΉβ(πΌ β 1))) β Even β§ (π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β (βπ β Even ((4 < π β§ π < π) β π β GoldbachEven ) β (πΌ β (1..^π·) β (π β Odd β (π β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))))))) |
132 | 131 | com15 101 |
. . . 4
β’ (π β (βπ β Even ((4 < π β§ π < π) β π β GoldbachEven ) β (πΌ β (1..^π·) β (π β Odd β (((π β (πΉβ(πΌ β 1))) β Even β§ (π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π))))))) |
133 | 6, 132 | mpd 15 |
. . 3
β’ (π β (πΌ β (1..^π·) β (π β Odd β (((π β (πΉβ(πΌ β 1))) β Even β§ (π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))))) |
134 | 133 | imp31 419 |
. 2
β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β (((π β (πΉβ(πΌ β 1))) β Even β§ (π β (πΉβ(πΌ β 1))) < π β§ 4 < (π β (πΉβ(πΌ β 1)))) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) |
135 | 15, 134 | syld 47 |
1
β’ (((π β§ πΌ β (1..^π·)) β§ π β Odd ) β ((π β ((πΉβπΌ)[,)(πΉβ(πΌ + 1))) β§ (π β (πΉβπΌ)) β€ 4) β βπ β β βπ β β βπ β β ((π β Odd β§ π β Odd β§ π β Odd ) β§ π = ((π + π) + π)))) |