Step | Hyp | Ref
| Expression |
1 | | isgbe 41639 |
. 2
GoldbachEven Even Odd
Odd |
2 | | 2nn 11185 |
. . . . . . . 8
|
3 | 2 | a1i 11 |
. . . . . . 7
Odd
Odd |
4 | | oveq2 6658 |
. . . . . . . . . . 11
|
5 | | df-2 11079 |
. . . . . . . . . . . . 13
|
6 | 5 | oveq2i 6661 |
. . . . . . . . . . . 12
|
7 | | 1z 11407 |
. . . . . . . . . . . . 13
|
8 | | fzpr 12396 |
. . . . . . . . . . . . 13
|
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . . . 12
|
10 | | 1p1e2 11134 |
. . . . . . . . . . . . 13
|
11 | 10 | preq2i 4272 |
. . . . . . . . . . . 12
|
12 | 6, 9, 11 | 3eqtri 2648 |
. . . . . . . . . . 11
|
13 | 4, 12 | syl6eq 2672 |
. . . . . . . . . 10
|
14 | 13 | oveq2d 6666 |
. . . . . . . . 9
|
15 | | breq1 4656 |
. . . . . . . . . 10
|
16 | 13 | sumeq1d 14431 |
. . . . . . . . . . 11
|
17 | 16 | eqeq2d 2632 |
. . . . . . . . . 10
|
18 | 15, 17 | anbi12d 747 |
. . . . . . . . 9
|
19 | 14, 18 | rexeqbidv 3153 |
. . . . . . . 8
|
20 | 19 | adantl 482 |
. . . . . . 7
Odd
Odd
|
21 | | 1ne2 11240 |
. . . . . . . . . . . . 13
|
22 | | 1ex 10035 |
. . . . . . . . . . . . . 14
|
23 | | 2ex 11092 |
. . . . . . . . . . . . . 14
|
24 | | vex 3203 |
. . . . . . . . . . . . . 14
|
25 | | vex 3203 |
. . . . . . . . . . . . . 14
|
26 | 22, 23, 24, 25 | fpr 6421 |
. . . . . . . . . . . . 13
|
27 | 21, 26 | mp1i 13 |
. . . . . . . . . . . 12
|
28 | | prssi 4353 |
. . . . . . . . . . . 12
|
29 | 27, 28 | fssd 6057 |
. . . . . . . . . . 11
|
30 | | prmex 15391 |
. . . . . . . . . . . . 13
|
31 | | prex 4909 |
. . . . . . . . . . . . 13
|
32 | 30, 31 | pm3.2i 471 |
. . . . . . . . . . . 12
|
33 | | elmapg 7870 |
. . . . . . . . . . . 12
|
34 | 32, 33 | mp1i 13 |
. . . . . . . . . . 11
|
35 | 29, 34 | mpbird 247 |
. . . . . . . . . 10
|
36 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . 14
|
38 | 37 | sumeq2dv 14433 |
. . . . . . . . . . . . 13
|
39 | 38 | eqeq1d 2624 |
. . . . . . . . . . . 12
|
40 | 39 | anbi2d 740 |
. . . . . . . . . . 11
|
41 | 40 | adantl 482 |
. . . . . . . . . 10
|
42 | | prmz 15389 |
. . . . . . . . . . . 12
|
43 | | prmz 15389 |
. . . . . . . . . . . 12
|
44 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
45 | 22, 24 | fvpr1 6456 |
. . . . . . . . . . . . . . 15
|
46 | 21, 45 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
47 | 44, 46 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
48 | | fveq2 6191 |
. . . . . . . . . . . . . 14
|
49 | 23, 25 | fvpr2 6457 |
. . . . . . . . . . . . . . 15
|
50 | 21, 49 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
51 | 48, 50 | syl6eq 2672 |
. . . . . . . . . . . . 13
|
52 | | zcn 11382 |
. . . . . . . . . . . . . 14
|
53 | | zcn 11382 |
. . . . . . . . . . . . . 14
|
54 | 52, 53 | anim12i 590 |
. . . . . . . . . . . . 13
|
55 | 7, 2 | pm3.2i 471 |
. . . . . . . . . . . . . 14
|
56 | 55 | a1i 11 |
. . . . . . . . . . . . 13
|
57 | 21 | a1i 11 |
. . . . . . . . . . . . 13
|
58 | 47, 51, 54, 56, 57 | sumpr 14477 |
. . . . . . . . . . . 12
|
59 | 42, 43, 58 | syl2an 494 |
. . . . . . . . . . 11
|
60 | | 2re 11090 |
. . . . . . . . . . . 12
|
61 | | 3re 11094 |
. . . . . . . . . . . 12
|
62 | | 2lt3 11195 |
. . . . . . . . . . . 12
|
63 | 60, 61, 62 | ltleii 10160 |
. . . . . . . . . . 11
|
64 | 59, 63 | jctil 560 |
. . . . . . . . . 10
|
65 | 35, 41, 64 | rspcedvd 3317 |
. . . . . . . . 9
|
66 | 65 | adantr 481 |
. . . . . . . 8
Odd
Odd
|
67 | | eqeq1 2626 |
. . . . . . . . . . . . 13
|
68 | | eqcom 2629 |
. . . . . . . . . . . . 13
|
69 | 67, 68 | syl6bb 276 |
. . . . . . . . . . . 12
|
70 | 69 | anbi2d 740 |
. . . . . . . . . . 11
|
71 | 70 | rexbidv 3052 |
. . . . . . . . . 10
|
72 | 71 | 3ad2ant3 1084 |
. . . . . . . . 9
Odd Odd
|
73 | 72 | adantl 482 |
. . . . . . . 8
Odd
Odd
|
74 | 66, 73 | mpbird 247 |
. . . . . . 7
Odd
Odd
|
75 | 3, 20, 74 | rspcedvd 3317 |
. . . . . 6
Odd
Odd
|
76 | 75 | a1d 25 |
. . . . 5
Odd
Odd Even
|
77 | 76 | ex 450 |
. . . 4
Odd
Odd
Even
|
78 | 77 | rexlimivv 3036 |
. . 3
Odd
Odd Even
|
79 | 78 | impcom 446 |
. 2
Even
Odd
Odd |
80 | 1, 79 | sylbi 207 |
1
GoldbachEven |