# Metamath Proof Explorer

## Axiom ax-bgbltosilva

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 ${⊢}\left({N}\in \mathrm{Even}\wedge 4<{N}\wedge {N}\le 4{10}^{18}\right)\to {N}\in \mathrm{GoldbachEven}$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cN ${class}{N}$
1 ceven ${class}\mathrm{Even}$
2 0 1 wcel ${wff}{N}\in \mathrm{Even}$
3 c4 ${class}4$
4 clt ${class}<$
5 3 0 4 wbr ${wff}4<{N}$
6 cle ${class}\le$
7 cmul ${class}×$
8 c1 ${class}1$
9 cc0 ${class}0$
10 8 9 cdc ${class}10$
11 cexp ${class}^$
12 c8 ${class}8$
13 8 12 cdc ${class}18$
14 10 13 11 co ${class}{10}^{18}$
15 3 14 7 co ${class}4{10}^{18}$
16 0 15 6 wbr ${wff}{N}\le 4{10}^{18}$
17 2 5 16 w3a ${wff}\left({N}\in \mathrm{Even}\wedge 4<{N}\wedge {N}\le 4{10}^{18}\right)$
18 cgbe ${class}\mathrm{GoldbachEven}$
19 0 18 wcel ${wff}{N}\in \mathrm{GoldbachEven}$
20 17 19 wi ${wff}\left(\left({N}\in \mathrm{Even}\wedge 4<{N}\wedge {N}\le 4{10}^{18}\right)\to {N}\in \mathrm{GoldbachEven}\right)$