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 ∃ 𝑚 ∈ ℕ ( ( 4 · ( 1 0 ↑ 1 8 ) ) ≤ 𝑚 ∧ ∀ 𝑛 ∈ Even ( ( 4 < 𝑛 ∧ 𝑛 < 𝑚 ) → 𝑛 ∈ GoldbachEven ) )

Proof

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