Step | Hyp | Ref
| Expression |
1 | | simpl 473 |
. . . . . . 7
Odd Odd |
2 | | 3odd 41617 |
. . . . . . 7
Odd |
3 | 1, 2 | jctir 561 |
. . . . . 6
Odd Odd
Odd |
4 | | omoeALTV 41596 |
. . . . . 6
Odd Odd
Even |
5 | | breq2 4657 |
. . . . . . . 8
|
6 | | eleq1 2689 |
. . . . . . . 8
GoldbachEven GoldbachEven |
7 | 5, 6 | imbi12d 334 |
. . . . . . 7
GoldbachEven
GoldbachEven |
8 | 7 | rspcv 3305 |
. . . . . 6
Even Even
GoldbachEven
GoldbachEven |
9 | 3, 4, 8 | 3syl 18 |
. . . . 5
Odd
Even GoldbachEven
GoldbachEven |
10 | | 4p3e7 11163 |
. . . . . . . . 9
|
11 | 10 | breq1i 4660 |
. . . . . . . 8
|
12 | | 4re 11097 |
. . . . . . . . . . 11
|
13 | 12 | a1i 11 |
. . . . . . . . . 10
Odd |
14 | | 3re 11094 |
. . . . . . . . . . 11
|
15 | 14 | a1i 11 |
. . . . . . . . . 10
Odd |
16 | | oddz 41544 |
. . . . . . . . . . 11
Odd |
17 | 16 | zred 11482 |
. . . . . . . . . 10
Odd |
18 | 13, 15, 17 | ltaddsubd 10627 |
. . . . . . . . 9
Odd |
19 | 18 | biimpd 219 |
. . . . . . . 8
Odd
|
20 | 11, 19 | syl5bir 233 |
. . . . . . 7
Odd
|
21 | 20 | imp 445 |
. . . . . 6
Odd |
22 | | pm2.27 42 |
. . . . . 6
GoldbachEven
GoldbachEven |
23 | 21, 22 | syl 17 |
. . . . 5
Odd GoldbachEven
GoldbachEven |
24 | | isgbe 41639 |
. . . . . 6
GoldbachEven Even Odd
Odd |
25 | | 3prm 15406 |
. . . . . . . . . . . . . 14
|
26 | 25 | a1i 11 |
. . . . . . . . . . . . 13
Odd
Odd
Odd |
27 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
Odd
Odd |
28 | 27 | 3anbi3d 1405 |
. . . . . . . . . . . . . . 15
Odd
Odd Odd Odd
Odd Odd |
29 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
30 | 29 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
31 | 28, 30 | anbi12d 747 |
. . . . . . . . . . . . . 14
Odd
Odd Odd
Odd
Odd Odd
|
32 | 31 | adantl 482 |
. . . . . . . . . . . . 13
Odd Odd
Odd Odd
Odd Odd
Odd
Odd Odd |
33 | | simp1 1061 |
. . . . . . . . . . . . . . . 16
Odd Odd
Odd |
34 | | simp2 1062 |
. . . . . . . . . . . . . . . 16
Odd Odd
Odd |
35 | 2 | a1i 11 |
. . . . . . . . . . . . . . . 16
Odd Odd
Odd |
36 | 33, 34, 35 | 3jca 1242 |
. . . . . . . . . . . . . . 15
Odd Odd
Odd Odd
Odd |
37 | 36 | adantl 482 |
. . . . . . . . . . . . . 14
Odd
Odd
Odd Odd
Odd Odd |
38 | 16 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
Odd |
39 | 38 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . 18
Odd
|
40 | | 3cn 11095 |
. . . . . . . . . . . . . . . . . . 19
|
41 | 40 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
Odd
|
42 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . 21
|
44 | | zaddcl 11417 |
. . . . . . . . . . . . . . . . . . . . 21
|
45 | 42, 43, 44 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . 20
|
46 | 45 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
|
47 | 46 | adantll 750 |
. . . . . . . . . . . . . . . . . 18
Odd
|
48 | 39, 41, 47 | subadd2d 10411 |
. . . . . . . . . . . . . . . . 17
Odd
|
49 | 48 | biimpa 501 |
. . . . . . . . . . . . . . . 16
Odd
|
50 | 49 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Odd
|
51 | 50 | 3ad2antr3 1228 |
. . . . . . . . . . . . . 14
Odd
Odd
Odd |
52 | 37, 51 | jca 554 |
. . . . . . . . . . . . 13
Odd
Odd
Odd Odd
Odd Odd
|
53 | 26, 32, 52 | rspcedvd 3317 |
. . . . . . . . . . . 12
Odd
Odd
Odd Odd
Odd Odd
|
54 | 53 | ex 450 |
. . . . . . . . . . 11
Odd
Odd
Odd Odd
Odd Odd
|
55 | 54 | reximdva 3017 |
. . . . . . . . . 10
Odd
Odd
Odd Odd
Odd Odd
|
56 | 55 | reximdva 3017 |
. . . . . . . . 9
Odd
Odd
Odd
Odd
Odd Odd
|
57 | 56, 1 | jctild 566 |
. . . . . . . 8
Odd
Odd
Odd
Odd Odd
Odd Odd
|
58 | | isgbo 41641 |
. . . . . . . 8
GoldbachOdd Odd Odd
Odd Odd
|
59 | 57, 58 | syl6ibr 242 |
. . . . . . 7
Odd
Odd
Odd
GoldbachOdd |
60 | 59 | adantld 483 |
. . . . . 6
Odd Even Odd
Odd GoldbachOdd |
61 | 24, 60 | syl5bi 232 |
. . . . 5
Odd
GoldbachEven
GoldbachOdd |
62 | 9, 23, 61 | 3syld 60 |
. . . 4
Odd
Even GoldbachEven
GoldbachOdd |
63 | 62 | com12 32 |
. . 3
Even
GoldbachEven Odd
GoldbachOdd |
64 | 63 | expd 452 |
. 2
Even
GoldbachEven Odd
GoldbachOdd |
65 | 64 | ralrimiv 2965 |
1
Even
GoldbachEven Odd
GoldbachOdd |