Proof of Theorem sbgoldbalt
Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . . . 6
|
2 | | evenz 41543 |
. . . . . 6
Even |
3 | | zltp1le 11427 |
. . . . . 6
|
4 | 1, 2, 3 | sylancr 695 |
. . . . 5
Even |
5 | | 2p1e3 11151 |
. . . . . . 7
|
6 | 5 | breq1i 4660 |
. . . . . 6
|
7 | | 3re 11094 |
. . . . . . . . 9
|
8 | 7 | a1i 11 |
. . . . . . . 8
Even |
9 | 2 | zred 11482 |
. . . . . . . 8
Even |
10 | 8, 9 | leloed 10180 |
. . . . . . 7
Even
|
11 | | 3z 11410 |
. . . . . . . . . . . 12
|
12 | | zltp1le 11427 |
. . . . . . . . . . . 12
|
13 | 11, 2, 12 | sylancr 695 |
. . . . . . . . . . 11
Even |
14 | | 3p1e4 11153 |
. . . . . . . . . . . . 13
|
15 | 14 | breq1i 4660 |
. . . . . . . . . . . 12
|
16 | | 4re 11097 |
. . . . . . . . . . . . . . 15
|
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
Even |
18 | 17, 9 | leloed 10180 |
. . . . . . . . . . . . 13
Even
|
19 | | pm3.35 611 |
. . . . . . . . . . . . . . . . . 18
GoldbachEven
GoldbachEven |
20 | | isgbe 41639 |
. . . . . . . . . . . . . . . . . . . 20
GoldbachEven Even Odd
Odd |
21 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . 24
Odd Odd
|
22 | 21 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
Even
Odd
Odd
|
23 | 22 | reximdva 3017 |
. . . . . . . . . . . . . . . . . . . . . 22
Even
Odd Odd
|
24 | 23 | reximdva 3017 |
. . . . . . . . . . . . . . . . . . . . 21
Even Odd Odd
|
25 | 24 | imp 445 |
. . . . . . . . . . . . . . . . . . . 20
Even
Odd
Odd |
26 | 20, 25 | sylbi 207 |
. . . . . . . . . . . . . . . . . . 19
GoldbachEven |
27 | 26 | a1d 25 |
. . . . . . . . . . . . . . . . . 18
GoldbachEven Even |
28 | 19, 27 | syl 17 |
. . . . . . . . . . . . . . . . 17
GoldbachEven Even |
29 | 28 | ex 450 |
. . . . . . . . . . . . . . . 16
GoldbachEven Even
|
30 | 29 | com23 86 |
. . . . . . . . . . . . . . 15
Even
GoldbachEven |
31 | | 2prm 15405 |
. . . . . . . . . . . . . . . . . . 19
|
32 | | 2p2e4 11144 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 32 | eqcomi 2631 |
. . . . . . . . . . . . . . . . . . 19
|
34 | | rspceov 6692 |
. . . . . . . . . . . . . . . . . . 19
|
35 | 31, 31, 33, 34 | mp3an 1424 |
. . . . . . . . . . . . . . . . . 18
|
36 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . 19
|
37 | 36 | 2rexbidv 3057 |
. . . . . . . . . . . . . . . . . 18
|
38 | 35, 37 | mpbii 223 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | a1d 25 |
. . . . . . . . . . . . . . . 16
GoldbachEven |
40 | 39 | a1d 25 |
. . . . . . . . . . . . . . 15
Even
GoldbachEven |
41 | 30, 40 | jaoi 394 |
. . . . . . . . . . . . . 14
Even
GoldbachEven |
42 | 41 | com12 32 |
. . . . . . . . . . . . 13
Even
GoldbachEven |
43 | 18, 42 | sylbid 230 |
. . . . . . . . . . . 12
Even GoldbachEven
|
44 | 15, 43 | syl5bi 232 |
. . . . . . . . . . 11
Even GoldbachEven
|
45 | 13, 44 | sylbid 230 |
. . . . . . . . . 10
Even
GoldbachEven
|
46 | 45 | com12 32 |
. . . . . . . . 9
Even
GoldbachEven |
47 | | 3odd 41617 |
. . . . . . . . . . . 12
Odd |
48 | | eleq1 2689 |
. . . . . . . . . . . 12
Odd
Odd |
49 | 47, 48 | mpbii 223 |
. . . . . . . . . . 11
Odd |
50 | | oddneven 41557 |
. . . . . . . . . . 11
Odd
Even |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
Even |
52 | 51 | pm2.21d 118 |
. . . . . . . . 9
Even
GoldbachEven |
53 | 46, 52 | jaoi 394 |
. . . . . . . 8
Even
GoldbachEven |
54 | 53 | com12 32 |
. . . . . . 7
Even
GoldbachEven |
55 | 10, 54 | sylbid 230 |
. . . . . 6
Even GoldbachEven
|
56 | 6, 55 | syl5bi 232 |
. . . . 5
Even GoldbachEven
|
57 | 4, 56 | sylbid 230 |
. . . 4
Even
GoldbachEven
|
58 | 57 | com23 86 |
. . 3
Even GoldbachEven
|
59 | | 2lt4 11198 |
. . . . . . . 8
|
60 | | 2re 11090 |
. . . . . . . . . 10
|
61 | 60 | a1i 11 |
. . . . . . . . 9
Even |
62 | | lttr 10114 |
. . . . . . . . 9
|
63 | 61, 17, 9, 62 | syl3anc 1326 |
. . . . . . . 8
Even |
64 | 59, 63 | mpani 712 |
. . . . . . 7
Even
|
65 | 64 | imp 445 |
. . . . . 6
Even |
66 | | simpll 790 |
. . . . . . . . 9
Even
Even |
67 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
Even
|
68 | 67 | anim1i 592 |
. . . . . . . . . . . . . . . 16
Even
|
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . 15
Even
|
70 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
Even
Even
|
71 | 70 | anim1i 592 |
. . . . . . . . . . . . . . . 16
Even
Even
|
72 | | df-3an 1039 |
. . . . . . . . . . . . . . . 16
Even
Even
|
73 | 71, 72 | sylibr 224 |
. . . . . . . . . . . . . . 15
Even
Even |
74 | | sbgoldbaltlem2 41668 |
. . . . . . . . . . . . . . 15
Even Odd
Odd |
75 | 69, 73, 74 | sylc 65 |
. . . . . . . . . . . . . 14
Even
Odd
Odd |
76 | | simpr 477 |
. . . . . . . . . . . . . 14
Even
|
77 | | df-3an 1039 |
. . . . . . . . . . . . . 14
Odd Odd Odd
Odd |
78 | 75, 76, 77 | sylanbrc 698 |
. . . . . . . . . . . . 13
Even
Odd
Odd |
79 | 78 | ex 450 |
. . . . . . . . . . . 12
Even
Odd Odd
|
80 | 79 | reximdva 3017 |
. . . . . . . . . . 11
Even
Odd Odd |
81 | 80 | reximdva 3017 |
. . . . . . . . . 10
Even
Odd Odd |
82 | 81 | imp 445 |
. . . . . . . . 9
Even
Odd Odd |
83 | 66, 82 | jca 554 |
. . . . . . . 8
Even
Even Odd Odd |
84 | 83 | ex 450 |
. . . . . . 7
Even
Even
Odd Odd |
85 | 84, 20 | syl6ibr 242 |
. . . . . 6
Even
GoldbachEven |
86 | 65, 85 | embantd 59 |
. . . . 5
Even
GoldbachEven |
87 | 86 | ex 450 |
. . . 4
Even
GoldbachEven |
88 | 87 | com23 86 |
. . 3
Even
GoldbachEven |
89 | 58, 88 | impbid 202 |
. 2
Even GoldbachEven
|
90 | 89 | ralbiia 2979 |
1
Even
GoldbachEven
Even |