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