Description: Any odd Goldbach number is greater than or equal to 9. Because of 9gbo , this bound is strict. (Contributed by AV, 26-Jul-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | gboge9 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isgbo | |
|
2 | df-3an | |
|
3 | an6 | |
|
4 | oddprmuzge3 | |
|
5 | oddprmuzge3 | |
|
6 | oddprmuzge3 | |
|
7 | 6p3e9 | |
|
8 | eluzelz | |
|
9 | eluzelz | |
|
10 | zaddcl | |
|
11 | 8 9 10 | syl2an | |
12 | 11 | zred | |
13 | eluzelre | |
|
14 | 12 13 | anim12i | |
15 | 14 | 3impa | |
16 | 6re | |
|
17 | 3re | |
|
18 | 16 17 | pm3.2i | |
19 | 15 18 | jctil | |
20 | 3p3e6 | |
|
21 | eluzelre | |
|
22 | eluzelre | |
|
23 | 21 22 | anim12i | |
24 | 17 17 | pm3.2i | |
25 | 23 24 | jctil | |
26 | eluzle | |
|
27 | eluzle | |
|
28 | 26 27 | anim12i | |
29 | le2add | |
|
30 | 25 28 29 | sylc | |
31 | 20 30 | eqbrtrrid | |
32 | 31 | 3adant3 | |
33 | eluzle | |
|
34 | 33 | 3ad2ant3 | |
35 | 32 34 | jca | |
36 | le2add | |
|
37 | 19 35 36 | sylc | |
38 | 7 37 | eqbrtrrid | |
39 | 4 5 6 38 | syl3an | |
40 | 3 39 | sylbi | |
41 | 2 40 | sylanbr | |
42 | breq2 | |
|
43 | 41 42 | syl5ibrcom | |
44 | 43 | expimpd | |
45 | 44 | rexlimdva | |
46 | 45 | a1i | |
47 | 46 | rexlimdvv | |
48 | 47 | imp | |
49 | 1 48 | sylbi | |