This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )