Metamath Proof Explorer

Theorem bgoldbachlt

Description: The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big m ). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva . (Contributed by AV, 3-Aug-2020) (Revised by AV, 9-Sep-2021)

Ref Expression
Assertion bgoldbachlt ⊢ ∃ m ∈ ℕ 4 ⁢ 10 18 ≤ m ∧ ∀ n ∈ Even 4 < n ∧ n < m → n ∈ GoldbachEven

Proof

Step Hyp Ref Expression
1 4nn ⊢ 4 ∈ ℕ
2 10nn ⊢ 10 ∈ ℕ
3 1nn0 ⊢ 1 ∈ ℕ 0
4 8nn0 ⊢ 8 ∈ ℕ 0
5 3 4 deccl ⊢ 18 ∈ ℕ 0
6 nnexpcl ⊢ 10 ∈ ℕ ∧ 18 ∈ ℕ 0 → 10 18 ∈ ℕ
7 2 5 6 mp2an ⊢ 10 18 ∈ ℕ
8 1 7 nnmulcli ⊢ 4 ⁢ 10 18 ∈ ℕ
9 id ⊢ 4 ⁢ 10 18 ∈ ℕ → 4 ⁢ 10 18 ∈ ℕ
10 breq2 ⊢ m = 4 ⁢ 10 18 → 4 ⁢ 10 18 ≤ m ↔ 4 ⁢ 10 18 ≤ 4 ⁢ 10 18
11 breq2 ⊢ m = 4 ⁢ 10 18 → n < m ↔ n < 4 ⁢ 10 18
12 11 anbi2d ⊢ m = 4 ⁢ 10 18 → 4 < n ∧ n < m ↔ 4 < n ∧ n < 4 ⁢ 10 18
13 12 imbi1d ⊢ m = 4 ⁢ 10 18 → 4 < n ∧ n < m → n ∈ GoldbachEven ↔ 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
14 13 ralbidv ⊢ m = 4 ⁢ 10 18 → ∀ n ∈ Even 4 < n ∧ n < m → n ∈ GoldbachEven ↔ ∀ n ∈ Even 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
15 10 14 anbi12d ⊢ m = 4 ⁢ 10 18 → 4 ⁢ 10 18 ≤ m ∧ ∀ n ∈ Even 4 < n ∧ n < m → n ∈ GoldbachEven ↔ 4 ⁢ 10 18 ≤ 4 ⁢ 10 18 ∧ ∀ n ∈ Even 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
16 15 adantl ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ m = 4 ⁢ 10 18 → 4 ⁢ 10 18 ≤ m ∧ ∀ n ∈ Even 4 < n ∧ n < m → n ∈ GoldbachEven ↔ 4 ⁢ 10 18 ≤ 4 ⁢ 10 18 ∧ ∀ n ∈ Even 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
17 nnre ⊢ 4 ⁢ 10 18 ∈ ℕ → 4 ⁢ 10 18 ∈ ℝ
18 17 leidd ⊢ 4 ⁢ 10 18 ∈ ℕ → 4 ⁢ 10 18 ≤ 4 ⁢ 10 18
19 simplr ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even ∧ 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ Even
20 simprl ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even ∧ 4 < n ∧ n < 4 ⁢ 10 18 → 4 < n
21 evenz ⊢ n ∈ Even → n ∈ ℤ
22 21 zred ⊢ n ∈ Even → n ∈ ℝ
23 ltle ⊢ n ∈ ℝ ∧ 4 ⁢ 10 18 ∈ ℝ → n < 4 ⁢ 10 18 → n ≤ 4 ⁢ 10 18
24 22 17 23 syl2anr ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even → n < 4 ⁢ 10 18 → n ≤ 4 ⁢ 10 18
25 24 a1d ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even → 4 < n → n < 4 ⁢ 10 18 → n ≤ 4 ⁢ 10 18
26 25 imp32 ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even ∧ 4 < n ∧ n < 4 ⁢ 10 18 → n ≤ 4 ⁢ 10 18
27 ax-bgbltosilva ⊢ n ∈ Even ∧ 4 < n ∧ n ≤ 4 ⁢ 10 18 → n ∈ GoldbachEven
28 19 20 26 27 syl3anc ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even ∧ 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
29 28 ex ⊢ 4 ⁢ 10 18 ∈ ℕ ∧ n ∈ Even → 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
30 29 ralrimiva ⊢ 4 ⁢ 10 18 ∈ ℕ → ∀ n ∈ Even 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
31 18 30 jca ⊢ 4 ⁢ 10 18 ∈ ℕ → 4 ⁢ 10 18 ≤ 4 ⁢ 10 18 ∧ ∀ n ∈ Even 4 < n ∧ n < 4 ⁢ 10 18 → n ∈ GoldbachEven
32 9 16 31 rspcedvd ⊢ 4 ⁢ 10 18 ∈ ℕ → ∃ m ∈ ℕ 4 ⁢ 10 18 ≤ m ∧ ∀ n ∈ Even 4 < n ∧ n < m → n ∈ GoldbachEven
33 8 32 ax-mp ⊢ ∃ m ∈ ℕ 4 ⁢ 10 18 ≤ m ∧ ∀ n ∈ Even 4 < n ∧ n < m → n ∈ GoldbachEven