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	$$classN$$
1		ceven	$$class\mathrm{Even}$$
2	0 1	wcel	$$wffN\in \mathrm{Even}$$
3		c4	$$class4$$
4		clt	$$class<$$
5	3 0 4	wbr	$$wff4<N$$
6		cle	$$class\le$$
7		cmul	$$class\times$$
8		c1	$$class1$$
9		cc0	$$class0$$
10	8 9	cdc	$$class10$$
11		cexp	$$class^$$
12		c8	$$class8$$
13	8 12	cdc	$$class18$$
14	10 13 11	co	$$class{10}^{18}$$
15	3 14 7	co	$$class4{10}^{18}$$
16	0 15 6	wbr	$$wffN\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	$$wffN\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)$$