Proof of Theorem sbgoldbo
Step | Hyp | Ref
| Expression |
1 | | nfra1 2941 |
. 2
Even GoldbachEven |
2 | | 3z 11410 |
. . . . 5
|
3 | | 6nn 11189 |
. . . . . 6
|
4 | 3 | nnzi 11401 |
. . . . 5
|
5 | | 3re 11094 |
. . . . . 6
|
6 | | 6re 11101 |
. . . . . 6
|
7 | | 3lt6 11206 |
. . . . . 6
|
8 | 5, 6, 7 | ltleii 10160 |
. . . . 5
|
9 | | eluz2 11693 |
. . . . 5
|
10 | 2, 4, 8, 9 | mpbir3an 1244 |
. . . 4
|
11 | | uzsplit 12412 |
. . . . 5
|
12 | 11 | eleq2d 2687 |
. . . 4
|
13 | 10, 12 | ax-mp 5 |
. . 3
|
14 | | elun 3753 |
. . . . 5
|
15 | | 6m1e5 11140 |
. . . . . . . . . 10
|
16 | 15 | oveq2i 6661 |
. . . . . . . . 9
|
17 | | 5nn 11188 |
. . . . . . . . . . . 12
|
18 | 17 | nnzi 11401 |
. . . . . . . . . . 11
|
19 | | 5re 11099 |
. . . . . . . . . . . 12
|
20 | | 3lt5 11201 |
. . . . . . . . . . . 12
|
21 | 5, 19, 20 | ltleii 10160 |
. . . . . . . . . . 11
|
22 | | eluz2 11693 |
. . . . . . . . . . 11
|
23 | 2, 18, 21, 22 | mpbir3an 1244 |
. . . . . . . . . 10
|
24 | | fzopredsuc 41333 |
. . . . . . . . . 10
..^ |
25 | 23, 24 | ax-mp 5 |
. . . . . . . . 9
..^ |
26 | 16, 25 | eqtri 2644 |
. . . . . . . 8
..^ |
27 | 26 | eleq2i 2693 |
. . . . . . 7
..^ |
28 | | elun 3753 |
. . . . . . . . 9
..^ ..^ |
29 | | elun 3753 |
. . . . . . . . . . 11
..^
..^ |
30 | | elsni 4194 |
. . . . . . . . . . . . 13
|
31 | | 1ex 10035 |
. . . . . . . . . . . . . . . . . . 19
|
32 | 31 | snid 4208 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32 | orci 405 |
. . . . . . . . . . . . . . . . 17
|
34 | | elun 3753 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | mpbir 221 |
. . . . . . . . . . . . . . . 16
|
36 | | sbgoldbo.p |
. . . . . . . . . . . . . . . 16
|
37 | 35, 36 | eleqtrri 2700 |
. . . . . . . . . . . . . . 15
|
38 | 37 | a1i 11 |
. . . . . . . . . . . . . 14
|
39 | | simpl 473 |
. . . . . . . . . . . . . . . 16
|
40 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
|
41 | 40 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
|
42 | 41 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
43 | 39, 42 | eqeq12d 2637 |
. . . . . . . . . . . . . . 15
|
44 | 43 | 2rexbidv 3057 |
. . . . . . . . . . . . . 14
|
45 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
46 | 45 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
47 | 46 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
48 | 47 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | adantl 482 |
. . . . . . . . . . . . . . 15
|
50 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
|
51 | | df-3 11080 |
. . . . . . . . . . . . . . . . . . 19
|
52 | | df-2 11079 |
. . . . . . . . . . . . . . . . . . . 20
|
53 | 52 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
|
54 | 51, 53 | eqtri 2644 |
. . . . . . . . . . . . . . . . . 18
|
55 | 50, 54 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . 17
|
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
57 | 38, 56 | rspcedeq2vd 3319 |
. . . . . . . . . . . . . . 15
|
58 | 38, 49, 57 | rspcedvd 3317 |
. . . . . . . . . . . . . 14
|
59 | 38, 44, 58 | rspcedvd 3317 |
. . . . . . . . . . . . 13
|
60 | 30, 59 | syl 17 |
. . . . . . . . . . . 12
|
61 | | 3p1e4 11153 |
. . . . . . . . . . . . . . . . 17
|
62 | | df-5 11082 |
. . . . . . . . . . . . . . . . 17
|
63 | 61, 62 | oveq12i 6662 |
. . . . . . . . . . . . . . . 16
..^ ..^ |
64 | | 4z 11411 |
. . . . . . . . . . . . . . . . 17
|
65 | | fzval3 12536 |
. . . . . . . . . . . . . . . . 17
..^ |
66 | 64, 65 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
..^ |
67 | 63, 66 | eqtr4i 2647 |
. . . . . . . . . . . . . . 15
..^ |
68 | 67 | eleq2i 2693 |
. . . . . . . . . . . . . 14
..^
|
69 | | fzsn 12383 |
. . . . . . . . . . . . . . . 16
|
70 | 64, 69 | ax-mp 5 |
. . . . . . . . . . . . . . 15
|
71 | 70 | eleq2i 2693 |
. . . . . . . . . . . . . 14
|
72 | 68, 71 | bitri 264 |
. . . . . . . . . . . . 13
..^
|
73 | | elsni 4194 |
. . . . . . . . . . . . . 14
|
74 | | 2prm 15405 |
. . . . . . . . . . . . . . . . . . 19
|
75 | 74 | olci 406 |
. . . . . . . . . . . . . . . . . 18
|
76 | | elun 3753 |
. . . . . . . . . . . . . . . . . 18
|
77 | 75, 76 | mpbir 221 |
. . . . . . . . . . . . . . . . 17
|
78 | 77, 36 | eleqtrri 2700 |
. . . . . . . . . . . . . . . 16
|
79 | 78 | a1i 11 |
. . . . . . . . . . . . . . 15
|
80 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 80 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
|
82 | 81 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
|
83 | 82 | 2rexbidv 3057 |
. . . . . . . . . . . . . . . 16
|
84 | 83 | adantl 482 |
. . . . . . . . . . . . . . 15
|
85 | 37 | a1i 11 |
. . . . . . . . . . . . . . . 16
|
86 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
87 | 86 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
|
88 | 87 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . . 18
|
89 | 88 | rexbidv 3052 |
. . . . . . . . . . . . . . . . 17
|
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
91 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
|
92 | | df-4 11081 |
. . . . . . . . . . . . . . . . . . . . 21
|
93 | 51 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | 92, 93 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
96 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . 21
|
97 | 96 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 97 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 95, 98 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
|
100 | 91, 99 | eqtrd 2656 |
. . . . . . . . . . . . . . . . 17
|
101 | 85, 100 | rspcedeq2vd 3319 |
. . . . . . . . . . . . . . . 16
|
102 | 85, 90, 101 | rspcedvd 3317 |
. . . . . . . . . . . . . . 15
|
103 | 79, 84, 102 | rspcedvd 3317 |
. . . . . . . . . . . . . 14
|
104 | 73, 103 | syl 17 |
. . . . . . . . . . . . 13
|
105 | 72, 104 | sylbi 207 |
. . . . . . . . . . . 12
..^
|
106 | 60, 105 | jaoi 394 |
. . . . . . . . . . 11
..^
|
107 | 29, 106 | sylbi 207 |
. . . . . . . . . 10
..^
|
108 | | elsni 4194 |
. . . . . . . . . . 11
|
109 | | 3prm 15406 |
. . . . . . . . . . . . . . . 16
|
110 | 109 | olci 406 |
. . . . . . . . . . . . . . 15
|
111 | | elun 3753 |
. . . . . . . . . . . . . . 15
|
112 | 110, 111 | mpbir 221 |
. . . . . . . . . . . . . 14
|
113 | 112, 36 | eleqtrri 2700 |
. . . . . . . . . . . . 13
|
114 | 113 | a1i 11 |
. . . . . . . . . . . 12
|
115 | | oveq1 6657 |
. . . . . . . . . . . . . . . 16
|
116 | 115 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
|
117 | 116 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
|
118 | 117 | 2rexbidv 3057 |
. . . . . . . . . . . . 13
|
119 | 118 | adantl 482 |
. . . . . . . . . . . 12
|
120 | 37 | a1i 11 |
. . . . . . . . . . . . 13
|
121 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
122 | 121 | oveq1d 6665 |
. . . . . . . . . . . . . . . 16
|
123 | 122 | eqeq2d 2632 |
. . . . . . . . . . . . . . 15
|
124 | 123 | rexbidv 3052 |
. . . . . . . . . . . . . 14
|
125 | 124 | adantl 482 |
. . . . . . . . . . . . 13
|
126 | | simpl 473 |
. . . . . . . . . . . . . . 15
|
127 | | oveq2 6658 |
. . . . . . . . . . . . . . . . 17
|
128 | 92 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . 18
|
129 | 62, 128 | eqtri 2644 |
. . . . . . . . . . . . . . . . 17
|
130 | 127, 129 | syl6reqr 2675 |
. . . . . . . . . . . . . . . 16
|
131 | 130 | adantl 482 |
. . . . . . . . . . . . . . 15
|
132 | 126, 131 | eqtrd 2656 |
. . . . . . . . . . . . . 14
|
133 | 120, 132 | rspcedeq2vd 3319 |
. . . . . . . . . . . . 13
|
134 | 120, 125,
133 | rspcedvd 3317 |
. . . . . . . . . . . 12
|
135 | 114, 119,
134 | rspcedvd 3317 |
. . . . . . . . . . 11
|
136 | 108, 135 | syl 17 |
. . . . . . . . . 10
|
137 | 107, 136 | jaoi 394 |
. . . . . . . . 9
..^
|
138 | 28, 137 | sylbi 207 |
. . . . . . . 8
..^
|
139 | 138 | a1d 25 |
. . . . . . 7
..^
Even
GoldbachEven
|
140 | 27, 139 | sylbi 207 |
. . . . . 6
Even GoldbachEven
|
141 | | sbgoldbm 41672 |
. . . . . . . 8
Even
GoldbachEven |
142 | | rspa 2930 |
. . . . . . . . . 10
|
143 | | ssun2 3777 |
. . . . . . . . . . . . 13
|
144 | 143, 36 | sseqtr4i 3638 |
. . . . . . . . . . . 12
|
145 | | rexss 3669 |
. . . . . . . . . . . 12
|
146 | 144, 145 | ax-mp 5 |
. . . . . . . . . . 11
|
147 | | rexss 3669 |
. . . . . . . . . . . . . . 15
|
148 | 144, 147 | ax-mp 5 |
. . . . . . . . . . . . . 14
|
149 | | rexss 3669 |
. . . . . . . . . . . . . . . . . 18
|
150 | 144, 149 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
|
151 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
|
152 | 151 | reximi 3011 |
. . . . . . . . . . . . . . . . 17
|
153 | 150, 152 | sylbi 207 |
. . . . . . . . . . . . . . . 16
|
154 | 153 | adantl 482 |
. . . . . . . . . . . . . . 15
|
155 | 154 | reximi 3011 |
. . . . . . . . . . . . . 14
|
156 | 148, 155 | sylbi 207 |
. . . . . . . . . . . . 13
|
157 | 156 | adantl 482 |
. . . . . . . . . . . 12
|
158 | 157 | reximi 3011 |
. . . . . . . . . . 11
|
159 | 146, 158 | sylbi 207 |
. . . . . . . . . 10
|
160 | 142, 159 | syl 17 |
. . . . . . . . 9
|
161 | 160 | ex 450 |
. . . . . . . 8
|
162 | 141, 161 | syl 17 |
. . . . . . 7
Even
GoldbachEven
|
163 | 162 | com12 32 |
. . . . . 6
Even
GoldbachEven
|
164 | 140, 163 | jaoi 394 |
. . . . 5
Even
GoldbachEven
|
165 | 14, 164 | sylbi 207 |
. . . 4
Even
GoldbachEven
|
166 | 165 | com12 32 |
. . 3
Even
GoldbachEven
|
167 | 13, 166 | syl5bi 232 |
. 2
Even
GoldbachEven
|
168 | 1, 167 | ralrimi 2957 |
1
Even
GoldbachEven
|