This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑁 ∈ 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 )