Axiom ax-bgbltosilva 41698

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.)

Assertion

Ref	Expression
ax-bgbltosilva	|- ( ( N e. Even /\ 4 < N /\ N <_ ( 4 x. (; 1 0 ^; 1 8 ) ) ) -> N e. GoldbachEven )

Detailed syntax breakdown of Axiom ax-bgbltosilva

Step	Hyp	Ref	Expression
1		cN	. . . 4 class N
2		ceven 41537	. . . 4 class Even
3	1, 2	wcel 1990	. . 3 wff N e. Even
4		c4 11072	. . . 4 class 4
5		clt 10074	. . . 4 class <
6	4, 1, 5	wbr 4653	. . 3 wff 4 < N
7		c1 9937	. . . . . . 7 class 1
8		cc0 9936	. . . . . . 7 class 0
9	7, 8	cdc 11493	. . . . . 6 class ; 1 0
10		c8 11076	. . . . . . 7 class 8
11	7, 10	cdc 11493	. . . . . 6 class ; 1 8
12		cexp 12860	. . . . . 6 class ^
13	9, 11, 12	co 6650	. . . . 5 class (; 1 0 ^; 1 8 )
14		cmul 9941	. . . . 5 class x.
15	4, 13, 14	co 6650	. . . 4 class ( 4 x. (; 1 0 ^; 1 8 ) )
16		cle 10075	. . . 4 class <_
17	1, 15, 16	wbr 4653	. . 3 wff N <_ ( 4 x. (; 1 0 ^; 1 8 ) )
18	3, 6, 17	w3a 1037	. 2 wff ( N e. Even /\ 4 < N /\ N <_ ( 4 x. (; 1 0 ^; 1 8 ) ) )
19		cgbe 41633	. . 3 class GoldbachEven
20	1, 19	wcel 1990	. 2 wff N e. GoldbachEven
21	18, 20	wi 4	1 wff ( ( N e. Even /\ 4 < N /\ N <_ ( 4 x. (; 1 0 ^; 1 8 ) ) ) -> N e. GoldbachEven )

This axiom is referenced by:  bgoldbachlt  41701  tgblthelfgott  41703