Axiom ax-bgbltosilva 45262

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	⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven )

Detailed syntax breakdown of Axiom ax-bgbltosilva

Step	Hyp	Ref	Expression
1		cN	. . . 4 class 𝑁
2		ceven 45076	. . . 4 class Even
3	1, 2	wcel 2106	. . 3 wff 𝑁 ∈ Even
4		c4 12030	. . . 4 class 4
5		clt 11009	. . . 4 class <
6	4, 1, 5	wbr 5074	. . 3 wff 4 < 𝑁
7		c1 10872	. . . . . . 7 class 1
8		cc0 10871	. . . . . . 7 class 0
9	7, 8	cdc 12437	. . . . . 6 class ;10
10		c8 12034	. . . . . . 7 class 8
11	7, 10	cdc 12437	. . . . . 6 class ;18
12		cexp 13782	. . . . . 6 class ↑
13	9, 11, 12	co 7275	. . . . 5 class (;10↑;18)
14		cmul 10876	. . . . 5 class ·
15	4, 13, 14	co 7275	. . . 4 class (4 · (;10↑;18))
16		cle 11010	. . . 4 class ≤
17	1, 15, 16	wbr 5074	. . 3 wff 𝑁 ≤ (4 · (;10↑;18))
18	3, 6, 17	w3a 1086	. 2 wff (𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18)))
19		cgbe 45197	. . 3 class GoldbachEven
20	1, 19	wcel 2106	. 2 wff 𝑁 ∈ GoldbachEven
21	18, 20	wi 4	1 wff ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven )

This axiom is referenced by:  bgoldbachlt  45265  tgblthelfgott  45267