![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-bgbltosilva | Structured version Visualization version GIF version |
Description: The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) |
Ref | Expression |
---|---|
ax-bgbltosilva | โข ((๐ โ Even โง 4 < ๐ โง ๐ โค (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cN | . . . 4 class ๐ | |
2 | ceven 45902 | . . . 4 class Even | |
3 | 1, 2 | wcel 2107 | . . 3 wff ๐ โ Even |
4 | c4 12215 | . . . 4 class 4 | |
5 | clt 11194 | . . . 4 class < | |
6 | 4, 1, 5 | wbr 5106 | . . 3 wff 4 < ๐ |
7 | c1 11057 | . . . . . . 7 class 1 | |
8 | cc0 11056 | . . . . . . 7 class 0 | |
9 | 7, 8 | cdc 12623 | . . . . . 6 class ;10 |
10 | c8 12219 | . . . . . . 7 class 8 | |
11 | 7, 10 | cdc 12623 | . . . . . 6 class ;18 |
12 | cexp 13973 | . . . . . 6 class โ | |
13 | 9, 11, 12 | co 7358 | . . . . 5 class (;10โ;18) |
14 | cmul 11061 | . . . . 5 class ยท | |
15 | 4, 13, 14 | co 7358 | . . . 4 class (4 ยท (;10โ;18)) |
16 | cle 11195 | . . . 4 class โค | |
17 | 1, 15, 16 | wbr 5106 | . . 3 wff ๐ โค (4 ยท (;10โ;18)) |
18 | 3, 6, 17 | w3a 1088 | . 2 wff (๐ โ Even โง 4 < ๐ โง ๐ โค (4 ยท (;10โ;18))) |
19 | cgbe 46023 | . . 3 class GoldbachEven | |
20 | 1, 19 | wcel 2107 | . 2 wff ๐ โ GoldbachEven |
21 | 18, 20 | wi 4 | 1 wff ((๐ โ Even โง 4 < ๐ โง ๐ โค (4 ยท (;10โ;18))) โ ๐ โ GoldbachEven ) |
Colors of variables: wff setvar class |
This axiom is referenced by: bgoldbachlt 46091 tgblthelfgott 46093 |
Copyright terms: Public domain | W3C validator |