Metamath Proof Explorer

Theorem nnsum4primesle9

Description: Every integer greater than 1 and less than or equal to 8 is the sum of at most 4 primes. (Contributed by AV, 24-Jul-2020) (Proof shortened by AV, 2-Aug-2020)

		Ref	Expression
	Assertion	nnsum4primesle9	$⊢ (N \in ℤ_{\geq 2} \land N \leq 8) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land N = \sum_{k = 1}^{d} f (k))$

Proof

Step	Hyp	Ref	Expression
1		nnsum3primesle9	$⊢ (N \in ℤ_{\geq 2} \land N \leq 8) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k))$
2		3lt4	$⊢ 3 < 4$
3		nnre	$⊢ d \in ℕ \to d \in ℝ$
4		3re	$⊢ 3 \in ℝ$
5	4	a1i	$⊢ d \in ℕ \to 3 \in ℝ$
6		4re	$⊢ 4 \in ℝ$
7	6	a1i	$⊢ d \in ℕ \to 4 \in ℝ$
8		leltletr	$⊢ (d \in ℝ \land 3 \in ℝ \land 4 \in ℝ) \to ((d \leq 3 \land 3 < 4) \to d \leq 4)$
9	3 5 7 8	syl3anc	$⊢ d \in ℕ \to ((d \leq 3 \land 3 < 4) \to d \leq 4)$
10	2 9	mpan2i	$⊢ d \in ℕ \to (d \leq 3 \to d \leq 4)$
11	10	anim1d	$⊢ d \in ℕ \to ((d \leq 3 \land N = \sum_{k = 1}^{d} f (k)) \to (d \leq 4 \land N = \sum_{k = 1}^{d} f (k)))$
12	11	reximdv	$⊢ d \in ℕ \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k)) \to \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land N = \sum_{k = 1}^{d} f (k)))$
13	12	reximia	$⊢ \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k)) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land N = \sum_{k = 1}^{d} f (k))$
14	1 13	syl	$⊢ (N \in ℤ_{\geq 2} \land N \leq 8) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land N = \sum_{k = 1}^{d} f (k))$