Metamath Proof Explorer

Theorem bgoldbnnsum3prm

Description: If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020)

Ref Expression
Assertion bgoldbnnsum3prm ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∀ n ∈ ℤ ≥ 2 ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 9nn ⊢ 9 ∈ ℕ
3 2 nnzi ⊢ 9 ∈ ℤ
4 2re ⊢ 2 ∈ ℝ
5 9re ⊢ 9 ∈ ℝ
6 2lt9 ⊢ 2 < 9
7 4 5 6 ltleii ⊢ 2 ≤ 9
8 eluz2 ⊢ 9 ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ 9 ∈ ℤ ∧ 2 ≤ 9
9 1 3 7 8 mpbir3an ⊢ 9 ∈ ℤ ≥ 2
10 fzouzsplit ⊢ 9 ∈ ℤ ≥ 2 → ℤ ≥ 2 = 2 ..^ 9 ∪ ℤ ≥ 9
11 10 eleq2d ⊢ 9 ∈ ℤ ≥ 2 → n ∈ ℤ ≥ 2 ↔ n ∈ 2 ..^ 9 ∪ ℤ ≥ 9
12 9 11 ax-mp ⊢ n ∈ ℤ ≥ 2 ↔ n ∈ 2 ..^ 9 ∪ ℤ ≥ 9
13 elun ⊢ n ∈ 2 ..^ 9 ∪ ℤ ≥ 9 ↔ n ∈ 2 ..^ 9 ∨ n ∈ ℤ ≥ 9
14 12 13 bitri ⊢ n ∈ ℤ ≥ 2 ↔ n ∈ 2 ..^ 9 ∨ n ∈ ℤ ≥ 9
15 elfzo2 ⊢ n ∈ 2 ..^ 9 ↔ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ ∧ n < 9
16 simp1 ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ ∧ n < 9 → n ∈ ℤ ≥ 2
17 df-9 ⊢ 9 = 8 + 1
18 17 breq2i ⊢ n < 9 ↔ n < 8 + 1
19 eluz2nn ⊢ n ∈ ℤ ≥ 2 → n ∈ ℕ
20 8nn ⊢ 8 ∈ ℕ
21 19 20 jctir ⊢ n ∈ ℤ ≥ 2 → n ∈ ℕ ∧ 8 ∈ ℕ
22 21 adantr ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ → n ∈ ℕ ∧ 8 ∈ ℕ
23 nnleltp1 ⊢ n ∈ ℕ ∧ 8 ∈ ℕ → n ≤ 8 ↔ n < 8 + 1
24 22 23 syl ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ → n ≤ 8 ↔ n < 8 + 1
25 24 biimprd ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ → n < 8 + 1 → n ≤ 8
26 18 25 biimtrid ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ → n < 9 → n ≤ 8
27 26 3impia ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ ∧ n < 9 → n ≤ 8
28 16 27 jca ⊢ n ∈ ℤ ≥ 2 ∧ 9 ∈ ℤ ∧ n < 9 → n ∈ ℤ ≥ 2 ∧ n ≤ 8
29 15 28 sylbi ⊢ n ∈ 2 ..^ 9 → n ∈ ℤ ≥ 2 ∧ n ≤ 8
30 nnsum3primesle9 ⊢ n ∈ ℤ ≥ 2 ∧ n ≤ 8 → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
31 29 30 syl ⊢ n ∈ 2 ..^ 9 → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
32 31 a1d ⊢ n ∈ 2 ..^ 9 → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
33 breq2 ⊢ m = n → 4 < m ↔ 4 < n
34 eleq1w ⊢ m = n → m ∈ GoldbachEven ↔ n ∈ GoldbachEven
35 33 34 imbi12d ⊢ m = n → 4 < m → m ∈ GoldbachEven ↔ 4 < n → n ∈ GoldbachEven
36 35 rspcv ⊢ n ∈ Even → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → 4 < n → n ∈ GoldbachEven
37 4re ⊢ 4 ∈ ℝ
38 37 a1i ⊢ n ∈ ℤ ≥ 9 → 4 ∈ ℝ
39 5 a1i ⊢ n ∈ ℤ ≥ 9 → 9 ∈ ℝ
40 eluzelre ⊢ n ∈ ℤ ≥ 9 → n ∈ ℝ
41 38 39 40 3jca ⊢ n ∈ ℤ ≥ 9 → 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ n ∈ ℝ
42 41 adantl ⊢ n ∈ Even ∧ n ∈ ℤ ≥ 9 → 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ n ∈ ℝ
43 eluzle ⊢ n ∈ ℤ ≥ 9 → 9 ≤ n
44 43 adantl ⊢ n ∈ Even ∧ n ∈ ℤ ≥ 9 → 9 ≤ n
45 4lt9 ⊢ 4 < 9
46 44 45 jctil ⊢ n ∈ Even ∧ n ∈ ℤ ≥ 9 → 4 < 9 ∧ 9 ≤ n
47 ltletr ⊢ 4 ∈ ℝ ∧ 9 ∈ ℝ ∧ n ∈ ℝ → 4 < 9 ∧ 9 ≤ n → 4 < n
48 42 46 47 sylc ⊢ n ∈ Even ∧ n ∈ ℤ ≥ 9 → 4 < n
49 pm2.27 ⊢ 4 < n → 4 < n → n ∈ GoldbachEven → n ∈ GoldbachEven
50 48 49 syl ⊢ n ∈ Even ∧ n ∈ ℤ ≥ 9 → 4 < n → n ∈ GoldbachEven → n ∈ GoldbachEven
51 50 ex ⊢ n ∈ Even → n ∈ ℤ ≥ 9 → 4 < n → n ∈ GoldbachEven → n ∈ GoldbachEven
52 36 51 syl5d ⊢ n ∈ Even → n ∈ ℤ ≥ 9 → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → n ∈ GoldbachEven
53 52 impcom ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Even → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → n ∈ GoldbachEven
54 nnsum3primesgbe ⊢ n ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
55 53 54 syl6 ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Even → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
56 3nn ⊢ 3 ∈ ℕ
57 56 a1i ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd ∧ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → 3 ∈ ℕ
58 oveq2 ⊢ d = 3 → 1 … d = 1 … 3
59 58 oveq2d ⊢ d = 3 → ℙ 1 … d = ℙ 1 … 3
60 breq1 ⊢ d = 3 → d ≤ 3 ↔ 3 ≤ 3
61 58 sumeq1d ⊢ d = 3 → ∑ k = 1 d f ⁡ k = ∑ k = 1 3 f ⁡ k
62 61 eqeq2d ⊢ d = 3 → n = ∑ k = 1 d f ⁡ k ↔ n = ∑ k = 1 3 f ⁡ k
63 60 62 anbi12d ⊢ d = 3 → d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k ↔ 3 ≤ 3 ∧ n = ∑ k = 1 3 f ⁡ k
64 59 63 rexeqbidv ⊢ d = 3 → ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k ↔ ∃ f ∈ ℙ 1 … 3 3 ≤ 3 ∧ n = ∑ k = 1 3 f ⁡ k
65 64 adantl ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd ∧ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW ∧ d = 3 → ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k ↔ ∃ f ∈ ℙ 1 … 3 3 ≤ 3 ∧ n = ∑ k = 1 3 f ⁡ k
66 3re ⊢ 3 ∈ ℝ
67 66 leidi ⊢ 3 ≤ 3
68 67 a1i ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd ∧ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → 3 ≤ 3
69 6nn ⊢ 6 ∈ ℕ
70 69 nnzi ⊢ 6 ∈ ℤ
71 6re ⊢ 6 ∈ ℝ
72 6lt9 ⊢ 6 < 9
73 71 5 72 ltleii ⊢ 6 ≤ 9
74 eluzuzle ⊢ 6 ∈ ℤ ∧ 6 ≤ 9 → n ∈ ℤ ≥ 9 → n ∈ ℤ ≥ 6
75 70 73 74 mp2an ⊢ n ∈ ℤ ≥ 9 → n ∈ ℤ ≥ 6
76 75 anim1i ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd → n ∈ ℤ ≥ 6 ∧ n ∈ Odd
77 nnsum4primesodd ⊢ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → n ∈ ℤ ≥ 6 ∧ n ∈ Odd → ∃ f ∈ ℙ 1 … 3 n = ∑ k = 1 3 f ⁡ k
78 76 77 mpan9 ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd ∧ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → ∃ f ∈ ℙ 1 … 3 n = ∑ k = 1 3 f ⁡ k
79 r19.42v ⊢ ∃ f ∈ ℙ 1 … 3 3 ≤ 3 ∧ n = ∑ k = 1 3 f ⁡ k ↔ 3 ≤ 3 ∧ ∃ f ∈ ℙ 1 … 3 n = ∑ k = 1 3 f ⁡ k
80 68 78 79 sylanbrc ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd ∧ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → ∃ f ∈ ℙ 1 … 3 3 ≤ 3 ∧ n = ∑ k = 1 3 f ⁡ k
81 57 65 80 rspcedvd ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd ∧ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
82 81 expcom ⊢ ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW → n ∈ ℤ ≥ 9 ∧ n ∈ Odd → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
83 sbgoldbwt ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∀ o ∈ Odd 5 < o → o ∈ GoldbachOddW
84 82 83 syl11 ⊢ n ∈ ℤ ≥ 9 ∧ n ∈ Odd → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
85 eluzelz ⊢ n ∈ ℤ ≥ 9 → n ∈ ℤ
86 zeoALTV ⊢ n ∈ ℤ → n ∈ Even ∨ n ∈ Odd
87 85 86 syl ⊢ n ∈ ℤ ≥ 9 → n ∈ Even ∨ n ∈ Odd
88 55 84 87 mpjaodan ⊢ n ∈ ℤ ≥ 9 → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
89 32 88 jaoi ⊢ n ∈ 2 ..^ 9 ∨ n ∈ ℤ ≥ 9 → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
90 14 89 sylbi ⊢ n ∈ ℤ ≥ 2 → ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
91 90 impcom ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven ∧ n ∈ ℤ ≥ 2 → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k
92 91 ralrimiva ⊢ ∀ m ∈ Even 4 < m → m ∈ GoldbachEven → ∀ n ∈ ℤ ≥ 2 ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ n = ∑ k = 1 d f ⁡ k