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 | ||
|---|---|---|---|
| Assertion | ax-bgbltosilva | |- ( ( N e. Even /\ 4 < N /\ N <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> N e. GoldbachEven ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cN | |- N |
|
| 1 | ceven | |- Even |
|
| 2 | 0 1 | wcel | |- N e. Even |
| 3 | c4 | |- 4 |
|
| 4 | clt | |- < |
|
| 5 | 3 0 4 | wbr | |- 4 < N |
| 6 | cle | |- <_ |
|
| 7 | cmul | |- x. |
|
| 8 | c1 | |- 1 |
|
| 9 | cc0 | |- 0 |
|
| 10 | 8 9 | cdc | |- ; 1 0 |
| 11 | cexp | |- ^ |
|
| 12 | c8 | |- 8 |
|
| 13 | 8 12 | cdc | |- ; 1 8 |
| 14 | 10 13 11 | co | |- ( ; 1 0 ^ ; 1 8 ) |
| 15 | 3 14 7 | co | |- ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) |
| 16 | 0 15 6 | wbr | |- N <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) |
| 17 | 2 5 16 | w3a | |- ( N e. Even /\ 4 < N /\ N <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) |
| 18 | cgbe | |- GoldbachEven |
|
| 19 | 0 18 | wcel | |- N e. GoldbachEven |
| 20 | 17 19 | wi | |- ( ( N e. Even /\ 4 < N /\ N <_ ( 4 x. ( ; 1 0 ^ ; 1 8 ) ) ) -> N e. GoldbachEven ) |