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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cN	⊢ 𝑁
1		ceven	⊢ Even
2	0 1	wcel	⊢ 𝑁 ∈ Even
3		c4	⊢ 4
4		clt	⊢ <
5	3 0 4	wbr	⊢ 4 < 𝑁
6		cle	⊢ ≤
7		cmul	⊢ ·
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 · ( ; 1 0 ↑ ; 1 8 ) )
16	0 15 6	wbr	⊢ 𝑁 ≤ ( 4 · ( ; 1 0 ↑ ; 1 8 ) )
17	2 5 16	w3a	⊢ ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) )
18		cgbe	⊢ GoldbachEven
19	0 18	wcel	⊢ 𝑁 ∈ GoldbachEven
20	17 19	wi	⊢ ( ( 𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ ( 4 · ( ; 1 0 ↑ ; 1 8 ) ) ) → 𝑁 ∈ GoldbachEven )