Step | Hyp | Ref
| Expression |
1 | | oddz 41544 |
. . . 4
Odd |
2 | | 5nn 11188 |
. . . . . . . 8
|
3 | 2 | nnzi 11401 |
. . . . . . 7
|
4 | | zltp1le 11427 |
. . . . . . 7
|
5 | 3, 4 | mpan 706 |
. . . . . 6
|
6 | | 5p1e6 11155 |
. . . . . . . . 9
|
7 | 6 | breq1i 4660 |
. . . . . . . 8
|
8 | | 6re 11101 |
. . . . . . . . . 10
|
9 | 8 | a1i 11 |
. . . . . . . . 9
|
10 | | zre 11381 |
. . . . . . . . 9
|
11 | 9, 10 | leloed 10180 |
. . . . . . . 8
|
12 | 7, 11 | syl5bb 272 |
. . . . . . 7
|
13 | | 6nn 11189 |
. . . . . . . . . . . . 13
|
14 | 13 | nnzi 11401 |
. . . . . . . . . . . 12
|
15 | | zltp1le 11427 |
. . . . . . . . . . . 12
|
16 | 14, 15 | mpan 706 |
. . . . . . . . . . 11
|
17 | | 6p1e7 11156 |
. . . . . . . . . . . . . 14
|
18 | 17 | breq1i 4660 |
. . . . . . . . . . . . 13
|
19 | | 7re 11103 |
. . . . . . . . . . . . . . 15
|
20 | 19 | a1i 11 |
. . . . . . . . . . . . . 14
|
21 | 20, 10 | leloed 10180 |
. . . . . . . . . . . . 13
|
22 | 18, 21 | syl5bb 272 |
. . . . . . . . . . . 12
|
23 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
Odd Odd |
24 | | 3odd 41617 |
. . . . . . . . . . . . . . . . . . . 20
Odd |
25 | 23, 24 | jctir 561 |
. . . . . . . . . . . . . . . . . . 19
Odd Odd
Odd |
26 | | omoeALTV 41596 |
. . . . . . . . . . . . . . . . . . 19
Odd Odd
Even |
27 | | breq2 4657 |
. . . . . . . . . . . . . . . . . . . . 21
|
28 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
GoldbachEven GoldbachEven |
29 | 27, 28 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
GoldbachEven
GoldbachEven |
30 | 29 | rspcv 3305 |
. . . . . . . . . . . . . . . . . . 19
Even Even
GoldbachEven
GoldbachEven |
31 | 25, 26, 30 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
Odd Even
GoldbachEven
GoldbachEven |
32 | | 4p3e7 11163 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
33 | 32 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
34 | 33 | breq1i 4660 |
. . . . . . . . . . . . . . . . . . . . . 22
|
35 | | 4re 11097 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
36 | 35 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
37 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
38 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
39 | | ltaddsub 10502 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
40 | 39 | biimpd 219 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | 36, 38, 10, 40 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
|
42 | 34, 41 | syl5bi 232 |
. . . . . . . . . . . . . . . . . . . . 21
|
43 | 42 | impcom 446 |
. . . . . . . . . . . . . . . . . . . 20
|
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
Odd |
45 | | pm2.27 42 |
. . . . . . . . . . . . . . . . . . 19
GoldbachEven
GoldbachEven |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Odd
GoldbachEven GoldbachEven |
47 | | isgbe 41639 |
. . . . . . . . . . . . . . . . . . 19
GoldbachEven Even Odd
Odd |
48 | | 3prm 15406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
50 | | zcn 11382 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
51 | | 3cn 11095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
52 | 50, 51 | jctir 561 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
53 | | npcan 10290 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
54 | 53 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
55 | 52, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
56 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
57 | 56 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
58 | 55, 57 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
59 | 49, 58 | rspcedeq2vd 3319 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
60 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
61 | 60 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
62 | 61 | rexbidv 3052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
63 | 59, 62 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
64 | 63 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
Odd Odd
|
65 | 64 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
Odd
Odd |
66 | 65 | ad4antlr 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Odd
Odd
Odd |
67 | 66 | reximdva 3017 |
. . . . . . . . . . . . . . . . . . . . . . 23
Odd
Odd
Odd
|
68 | 67 | reximdva 3017 |
. . . . . . . . . . . . . . . . . . . . . 22
Odd Odd Odd
|
69 | 68, 23 | jctild 566 |
. . . . . . . . . . . . . . . . . . . . 21
Odd Odd Odd
Odd |
70 | | isgbow 41640 |
. . . . . . . . . . . . . . . . . . . . 21
GoldbachOddW Odd |
71 | 69, 70 | syl6ibr 242 |
. . . . . . . . . . . . . . . . . . . 20
Odd Odd Odd
GoldbachOddW |
72 | 71 | adantld 483 |
. . . . . . . . . . . . . . . . . . 19
Odd Even Odd
Odd GoldbachOddW |
73 | 47, 72 | syl5bi 232 |
. . . . . . . . . . . . . . . . . 18
Odd GoldbachEven GoldbachOddW |
74 | 31, 46, 73 | 3syld 60 |
. . . . . . . . . . . . . . . . 17
Odd Even
GoldbachEven GoldbachOddW |
75 | 74 | ex 450 |
. . . . . . . . . . . . . . . 16
Odd Even
GoldbachEven
GoldbachOddW |
76 | 75 | com23 86 |
. . . . . . . . . . . . . . 15
Even
GoldbachEven Odd
GoldbachOddW |
77 | 76 | ex 450 |
. . . . . . . . . . . . . 14
Even
GoldbachEven
Odd GoldbachOddW |
78 | | 7gbow 41660 |
. . . . . . . . . . . . . . . . . 18
GoldbachOddW |
79 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
GoldbachOddW
GoldbachOddW |
80 | 78, 79 | mpbii 223 |
. . . . . . . . . . . . . . . . 17
GoldbachOddW |
81 | 80 | a1d 25 |
. . . . . . . . . . . . . . . 16
Odd
GoldbachOddW |
82 | 81 | a1d 25 |
. . . . . . . . . . . . . . 15
Even GoldbachEven
Odd GoldbachOddW |
83 | 82 | a1d 25 |
. . . . . . . . . . . . . 14
Even
GoldbachEven
Odd GoldbachOddW |
84 | 77, 83 | jaoi 394 |
. . . . . . . . . . . . 13
Even
GoldbachEven Odd
GoldbachOddW |
85 | 84 | com12 32 |
. . . . . . . . . . . 12
Even
GoldbachEven Odd
GoldbachOddW |
86 | 22, 85 | sylbid 230 |
. . . . . . . . . . 11
Even
GoldbachEven
Odd GoldbachOddW |
87 | 16, 86 | sylbid 230 |
. . . . . . . . . 10
Even
GoldbachEven
Odd GoldbachOddW |
88 | 87 | com12 32 |
. . . . . . . . 9
Even
GoldbachEven
Odd GoldbachOddW |
89 | | eleq1 2689 |
. . . . . . . . . . . 12
Odd
Odd |
90 | | 6even 41620 |
. . . . . . . . . . . . 13
Even |
91 | | evennodd 41556 |
. . . . . . . . . . . . . 14
Even
Odd |
92 | 91 | pm2.21d 118 |
. . . . . . . . . . . . 13
Even Odd
GoldbachOddW |
93 | 90, 92 | ax-mp 5 |
. . . . . . . . . . . 12
Odd GoldbachOddW |
94 | 89, 93 | syl6bir 244 |
. . . . . . . . . . 11
Odd
GoldbachOddW |
95 | 94 | a1d 25 |
. . . . . . . . . 10
Even GoldbachEven
Odd GoldbachOddW |
96 | 95 | a1d 25 |
. . . . . . . . 9
Even
GoldbachEven
Odd GoldbachOddW |
97 | 88, 96 | jaoi 394 |
. . . . . . . 8
Even
GoldbachEven Odd
GoldbachOddW |
98 | 97 | com12 32 |
. . . . . . 7
Even
GoldbachEven Odd
GoldbachOddW |
99 | 12, 98 | sylbid 230 |
. . . . . 6
Even
GoldbachEven
Odd GoldbachOddW |
100 | 5, 99 | sylbid 230 |
. . . . 5
Even
GoldbachEven
Odd GoldbachOddW |
101 | 100 | com24 95 |
. . . 4
Odd
Even
GoldbachEven
GoldbachOddW |
102 | 1, 101 | mpcom 38 |
. . 3
Odd Even
GoldbachEven
GoldbachOddW |
103 | 102 | impcom 446 |
. 2
Even
GoldbachEven Odd
GoldbachOddW |
104 | 103 | ralrimiva 2966 |
1
Even
GoldbachEven Odd
GoldbachOddW |