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 ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 nnsum3primesgbe ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
2 3lt4 3 < 4
3 nnre ( 𝑑 ∈ ℕ → 𝑑 ∈ ℝ )
4 3re 3 ∈ ℝ
5 4 a1i ( 𝑑 ∈ ℕ → 3 ∈ ℝ )
6 4re 4 ∈ ℝ
7 6 a1i ( 𝑑 ∈ ℕ → 4 ∈ ℝ )
8 leltletr ( ( 𝑑 ∈ ℝ ∧ 3 ∈ ℝ ∧ 4 ∈ ℝ ) → ( ( 𝑑 ≤ 3 ∧ 3 < 4 ) → 𝑑 ≤ 4 ) )
9 3 5 7 8 syl3anc ( 𝑑 ∈ ℕ → ( ( 𝑑 ≤ 3 ∧ 3 < 4 ) → 𝑑 ≤ 4 ) )
10 2 9 mpan2i ( 𝑑 ∈ ℕ → ( 𝑑 ≤ 3 → 𝑑 ≤ 4 ) )
11 10 anim1d ( 𝑑 ∈ ℕ → ( ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) → ( 𝑑 ≤ 4 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
12 11 reximdv ( 𝑑 ∈ ℕ → ( ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) → ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) ) )
13 12 reximia ( ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 3 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )
14 1 13 syl ( 𝑁 ∈ GoldbachEven → ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑁 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓𝑘 ) ) )