Step | Hyp | Ref
| Expression |
1 | | evengpop3 41686 |
. . . 4
Odd
GoldbachOddW
Even GoldbachOddW |
2 | 1 | imp 445 |
. . 3
Odd
GoldbachOddW
Even
GoldbachOddW |
3 | | simplll 798 |
. . . . . . 7
Odd
GoldbachOddW
Even GoldbachOddW Odd
GoldbachOddW |
4 | | 6nn 11189 |
. . . . . . . . . . . 12
|
5 | 4 | nnzi 11401 |
. . . . . . . . . . 11
|
6 | 5 | a1i 11 |
. . . . . . . . . 10
|
7 | | 3z 11410 |
. . . . . . . . . . 11
|
8 | 7 | a1i 11 |
. . . . . . . . . 10
|
9 | | 6p3e9 11170 |
. . . . . . . . . . . . . 14
|
10 | 9 | eqcomi 2631 |
. . . . . . . . . . . . 13
|
11 | 10 | fveq2i 6194 |
. . . . . . . . . . . 12
|
12 | 11 | eleq2i 2693 |
. . . . . . . . . . 11
|
13 | 12 | biimpi 206 |
. . . . . . . . . 10
|
14 | | eluzsub 11717 |
. . . . . . . . . 10
|
15 | 6, 8, 13, 14 | syl3anc 1326 |
. . . . . . . . 9
|
16 | 15 | adantr 481 |
. . . . . . . 8
Even
|
17 | 16 | ad3antlr 767 |
. . . . . . 7
Odd
GoldbachOddW
Even GoldbachOddW
|
18 | | 3odd 41617 |
. . . . . . . . . . . . . 14
Odd |
19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
Odd |
20 | 19 | anim1i 592 |
. . . . . . . . . . . 12
Even
Odd
Even |
21 | 20 | adantl 482 |
. . . . . . . . . . 11
Odd
GoldbachOddW
Even
Odd
Even |
22 | 21 | ancomd 467 |
. . . . . . . . . 10
Odd
GoldbachOddW
Even
Even Odd |
23 | 22 | adantr 481 |
. . . . . . . . 9
Odd
GoldbachOddW
Even GoldbachOddW
Even Odd |
24 | 23 | adantr 481 |
. . . . . . . 8
Odd
GoldbachOddW
Even GoldbachOddW
Even Odd |
25 | | emoo 41613 |
. . . . . . . 8
Even Odd
Odd |
26 | 24, 25 | syl 17 |
. . . . . . 7
Odd
GoldbachOddW
Even GoldbachOddW
Odd |
27 | | nnsum4primesodd 41684 |
. . . . . . . 8
Odd
GoldbachOddW
Odd
|
28 | 27 | imp 445 |
. . . . . . 7
Odd
GoldbachOddW
Odd
|
29 | 3, 17, 26, 28 | syl12anc 1324 |
. . . . . 6
Odd
GoldbachOddW
Even GoldbachOddW
|
30 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
31 | | 4z 11411 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | fzonel 12483 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
33 | | fzoval 12471 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^ |
34 | 31, 33 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
35 | | 4cn 11098 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
36 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
37 | | 3cn 11095 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
38 | 35, 36, 37 | 3pm3.2i 1239 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
39 | | 3p1e4 11153 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
40 | | subadd2 10285 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
41 | 39, 40 | mpbiri 248 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
42 | 38, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
43 | 42 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
44 | 34, 43 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
45 | 44 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
46 | 45 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
47 | 32, 46 | mtbir 313 |
. . . . . . . . . . . . . . . . . . 19
|
48 | 31, 47 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
50 | | 3prm 15406 |
. . . . . . . . . . . . . . . . . 18
|
51 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . 17
|
52 | | fsnunf 6451 |
. . . . . . . . . . . . . . . . 17
|
53 | 30, 49, 51, 52 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
|
54 | | fzval3 12536 |
. . . . . . . . . . . . . . . . . . 19
..^ |
55 | 31, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
..^ |
56 | | 1z 11407 |
. . . . . . . . . . . . . . . . . . . 20
|
57 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . 21
|
58 | | 4re 11097 |
. . . . . . . . . . . . . . . . . . . . 21
|
59 | | 1lt4 11199 |
. . . . . . . . . . . . . . . . . . . . 21
|
60 | 57, 58, 59 | ltleii 10160 |
. . . . . . . . . . . . . . . . . . . 20
|
61 | | eluz2 11693 |
. . . . . . . . . . . . . . . . . . . 20
|
62 | 56, 31, 60, 61 | mpbir3an 1244 |
. . . . . . . . . . . . . . . . . . 19
|
63 | | fzosplitsn 12576 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ |
64 | 62, 63 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ |
65 | 44 | uneq1i 3763 |
. . . . . . . . . . . . . . . . . 18
..^ |
66 | 55, 64, 65 | 3eqtri 2648 |
. . . . . . . . . . . . . . . . 17
|
67 | 66 | feq2i 6037 |
. . . . . . . . . . . . . . . 16
|
68 | 53, 67 | sylibr 224 |
. . . . . . . . . . . . . . 15
|
69 | | prmex 15391 |
. . . . . . . . . . . . . . . . 17
|
70 | | ovex 6678 |
. . . . . . . . . . . . . . . . 17
|
71 | 69, 70 | pm3.2i 471 |
. . . . . . . . . . . . . . . 16
|
72 | | elmapg 7870 |
. . . . . . . . . . . . . . . 16
|
73 | 71, 72 | mp1i 13 |
. . . . . . . . . . . . . . 15
|
74 | 68, 73 | mpbird 247 |
. . . . . . . . . . . . . 14
|
75 | 74 | adantr 481 |
. . . . . . . . . . . . 13
|
76 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
77 | 76 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
78 | 77 | sumeq2dv 14433 |
. . . . . . . . . . . . . . 15
|
79 | 78 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
80 | 79 | adantl 482 |
. . . . . . . . . . . . 13
|
81 | 62 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
82 | 66 | eleq2i 2693 |
. . . . . . . . . . . . . . . . . . 19
|
83 | | elun 3753 |
. . . . . . . . . . . . . . . . . . 19
|
84 | | velsn 4193 |
. . . . . . . . . . . . . . . . . . . 20
|
85 | 84 | orbi2i 541 |
. . . . . . . . . . . . . . . . . . 19
|
86 | 82, 83, 85 | 3bitri 286 |
. . . . . . . . . . . . . . . . . 18
|
87 | | elfz2 12333 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
88 | | 3re 11094 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
89 | 88, 58 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
90 | | 3lt4 11197 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
91 | | ltnle 10117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
92 | 90, 91 | mpbii 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
93 | 89, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
94 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
95 | 94 | eqcoms 2630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
96 | 93, 95 | mtbiri 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
97 | 96 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
98 | 97 | necon2ad 2809 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
99 | 98 | adantld 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
100 | 99 | 3ad2ant3 1084 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
101 | 100 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
102 | 87, 101 | sylbi 207 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
103 | 102 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
104 | | fvunsn 6445 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
105 | 103, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
106 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
107 | 106 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
108 | | prmz 15389 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
110 | 109 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
111 | 105, 110 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . . 22
|
112 | 111 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
|
113 | 112 | adantld 483 |
. . . . . . . . . . . . . . . . . . . 20
|
114 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
115 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
116 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
117 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
118 | | eleq2 2690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
119 | 47, 118 | mtbiri 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
120 | 117, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
121 | | fsnunfv 6453 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
122 | 115, 116,
120, 121 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
123 | 122 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
124 | 114, 123 | sylan9eq 2676 |
. . . . . . . . . . . . . . . . . . . . . 22
|
125 | 124, 37 | syl6eqel 2709 |
. . . . . . . . . . . . . . . . . . . . 21
|
126 | 125 | ex 450 |
. . . . . . . . . . . . . . . . . . . 20
|
127 | 113, 126 | jaoi 394 |
. . . . . . . . . . . . . . . . . . 19
|
128 | 127 | com12 32 |
. . . . . . . . . . . . . . . . . 18
|
129 | 86, 128 | syl5bi 232 |
. . . . . . . . . . . . . . . . 17
|
130 | 129 | imp 445 |
. . . . . . . . . . . . . . . 16
|
131 | 81, 130, 114 | fsumm1 14480 |
. . . . . . . . . . . . . . 15
|
132 | 131 | adantr 481 |
. . . . . . . . . . . . . 14
|
133 | 42 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . . . 21
|
134 | 133 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . 20
|
135 | 134 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
136 | 102 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
137 | 136, 104 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
138 | 137 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . 19
|
139 | 135, 138 | sumeq12dv 14437 |
. . . . . . . . . . . . . . . . . 18
|
140 | 139 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
141 | 140 | biimpa 501 |
. . . . . . . . . . . . . . . 16
|
142 | 141 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
|
143 | 142 | oveq1d 6665 |
. . . . . . . . . . . . . 14
|
144 | 31 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
145 | 7 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
146 | 120 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
|
147 | 144, 145,
146, 121 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
148 | 147 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
|
149 | | eluzelcn 11699 |
. . . . . . . . . . . . . . . . . 18
|
150 | 37 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
|
151 | 149, 150 | npcand 10396 |
. . . . . . . . . . . . . . . . 17
|
152 | 151 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
153 | 148, 152 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
|
154 | 153 | adantr 481 |
. . . . . . . . . . . . . 14
|
155 | 132, 143,
154 | 3eqtrrd 2661 |
. . . . . . . . . . . . 13
|
156 | 75, 80, 155 | rspcedvd 3317 |
. . . . . . . . . . . 12
|
157 | 156 | ex 450 |
. . . . . . . . . . 11
|
158 | 157 | expcom 451 |
. . . . . . . . . 10
|
159 | | elmapi 7879 |
. . . . . . . . . 10
|
160 | 158, 159 | syl11 33 |
. . . . . . . . 9
|
161 | 160 | rexlimdv 3030 |
. . . . . . . 8
|
162 | 161 | adantr 481 |
. . . . . . 7
Even
|
163 | 162 | ad3antlr 767 |
. . . . . 6
Odd
GoldbachOddW
Even GoldbachOddW
|
164 | 29, 163 | mpd 15 |
. . . . 5
Odd
GoldbachOddW
Even GoldbachOddW
|
165 | 164 | ex 450 |
. . . 4
Odd
GoldbachOddW
Even GoldbachOddW
|
166 | 165 | rexlimdva 3031 |
. . 3
Odd
GoldbachOddW
Even
GoldbachOddW
|
167 | 2, 166 | mpd 15 |
. 2
Odd
GoldbachOddW
Even
|
168 | 167 | ex 450 |
1
Odd
GoldbachOddW
Even
|