Metamath Proof Explorer

Theorem nnsum4primesprm

Description: Every prime is "the sum of at most 4" (actually one - the prime itself) primes. (Contributed by AV, 23-Jul-2020) (Proof shortened by AV, 2-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 nnsum3primesprm ⊢ P ∈ ℙ → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ P = ∑ 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 ∧ P = ∑ k = 1 d f ⁡ k → d ≤ 4 ∧ P = ∑ k = 1 d f ⁡ k
12 11 reximdv ⊢ d ∈ ℕ → ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ P = ∑ k = 1 d f ⁡ k → ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ P = ∑ k = 1 d f ⁡ k
13 12 reximia ⊢ ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 3 ∧ P = ∑ k = 1 d f ⁡ k → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ P = ∑ k = 1 d f ⁡ k
14 1 13 syl ⊢ P ∈ ℙ → ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ P = ∑ k = 1 d f ⁡ k