Theorem nnsum4primes4

Description: 4 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	nnsum4primes4	$$⊢\exists d\in \mathbb{N}\exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 4\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnsum3primes4	$$⊢\exists d\in \mathbb{N}\exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 3\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)$$
2		3lt4	$$⊢3<4$$
3		nnre	$$⊢d\in \mathbb{N}\to d\in ℝ$$
4		3re	$$⊢3\in ℝ$$
5	4	a1i	$$⊢d\in \mathbb{N}\to 3\in ℝ$$
6		4re	$$⊢4\in ℝ$$
7	6	a1i	$$⊢d\in \mathbb{N}\to 4\in ℝ$$
8		leltletr	$$⊢\left(d\in ℝ\wedge 3\in ℝ\wedge 4\in ℝ\right)\to \left(\left(d\le 3\wedge 3<4\right)\to d\le 4\right)$$
9	3 5 7 8	syl3anc	$$⊢d\in \mathbb{N}\to \left(\left(d\le 3\wedge 3<4\right)\to d\le 4\right)$$
10	2 9	mpan2i	$$⊢d\in \mathbb{N}\to \left(d\le 3\to d\le 4\right)$$
11	10	anim1d	$$⊢d\in \mathbb{N}\to \left(\left(d\le 3\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)\to \left(d\le 4\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)\right)$$
12	11	reximdv	$$⊢d\in \mathbb{N}\to \left(\exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 3\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)\to \exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 4\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)\right)$$
13	12	reximia	$$⊢\exists d\in \mathbb{N}\exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 3\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)\to \exists d\in \mathbb{N}\exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 4\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)$$
14	1 13	ax-mp	$$⊢\exists d\in \mathbb{N}\exists f\in \left({\mathbb{P}}^{\left(1\dots d\right)}\right)\left(d\le 4\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)$$