Metamath Proof Explorer

Theorem nnsum4primesgbe

Description: Any even Goldbach number is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020) (Proof shortened by AV, 2-Aug-2020)

Ref Expression
Assertion nnsum4primesgbe ⊢ N ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ N = ∑ k = 1 d f ⁡ k

Proof

Step Hyp Ref Expression
1 nnsum3primesgbe ⊢ N ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ N = ∑ k = 1 d f ⁡ k
2 3lt4 ⊢ 3 < 4
3 nnre ⊢ d ∈ ℕ → d ∈ ℝ
4 3re ⊢ 3 ∈ ℝ
5 4 a1i ⊢ d ∈ ℕ → 3 ∈ ℝ
6 4re ⊢ 4 ∈ ℝ
7 6 a1i ⊢ d ∈ ℕ → 4 ∈ ℝ
8 leltletr ⊢ d ∈ ℝ ∧ 3 ∈ ℝ ∧ 4 ∈ ℝ → d ≤ 3 ∧ 3 < 4 → d ≤ 4
9 3 5 7 8 syl3anc ⊢ d ∈ ℕ → d ≤ 3 ∧ 3 < 4 → d ≤ 4
10 2 9 mpan2i ⊢ d ∈ ℕ → d ≤ 3 → d ≤ 4
11 10 anim1d ⊢ d ∈ ℕ → d ≤ 3 ∧ N = ∑ k = 1 d f ⁡ k → d ≤ 4 ∧ N = ∑ k = 1 d f ⁡ k
12 11 reximdv ⊢ d ∈ ℕ → ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ N = ∑ k = 1 d f ⁡ k → ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ N = ∑ k = 1 d f ⁡ k
13 12 reximia ⊢ ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ N = ∑ k = 1 d f ⁡ k → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ N = ∑ k = 1 d f ⁡ k
14 1 13 syl ⊢ N ∈ GoldbachEven → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ N = ∑ k = 1 d f ⁡ k