Theorem nnsum3primes4

Description: 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		1ne2	$$⊢1\ne 2$$
3		1ex	$$⊢1\in \mathrm{V}$$
4		2ex	$$⊢2\in \mathrm{V}$$
5	3 4 4 4	fpr	$$⊢1\ne 2\to \left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\left\{2,2\right\}$$
6		2prm	$$⊢2\in \mathbb{P}$$
7	6 6	pm3.2i	$$⊢\left(2\in \mathbb{P}\wedge 2\in \mathbb{P}\right)$$
8	4 4	prss	$$⊢\left(2\in \mathbb{P}\wedge 2\in \mathbb{P}\right)\leftrightarrow \left\{2,2\right\}\subseteq \mathbb{P}$$
9	7 8	mpbi	$$⊢\left\{2,2\right\}\subseteq \mathbb{P}$$
10		fss	$$⊢\left(\left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\left\{2,2\right\}\wedge \left\{2,2\right\}\subseteq \mathbb{P}\right)\to \left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\mathbb{P}$$
11	9 10	mpan2	$$⊢\left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\left\{2,2\right\}\to \left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\mathbb{P}$$
12	2 5 11	mp2b	$$⊢\left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\mathbb{P}$$
13		prmex	$$⊢\mathbb{P}\in \mathrm{V}$$
14		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
15	13 14	elmap	$$⊢\left\{⟨1,2⟩,⟨2,2⟩\right\}\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)\leftrightarrow \left\{⟨1,2⟩,⟨2,2⟩\right\}:\left\{1,2\right\}⟶\mathbb{P}$$
16	12 15	mpbir	$$⊢\left\{⟨1,2⟩,⟨2,2⟩\right\}\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)$$
17		2re	$$⊢2\in ℝ$$
18		3re	$$⊢3\in ℝ$$
19		2lt3	$$⊢2<3$$
20	17 18 19	ltleii	$$⊢2\le 3$$
21		2cn	$$⊢2\in ℂ$$
22		fveq2	$$⊢k=1\to \left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)=\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(1\right)$$
23	3 4	fvpr1	$$⊢1\ne 2\to \left\{⟨1,2⟩,⟨2,2⟩\right\}\left(1\right)=2$$
24	2 23	ax-mp	$$⊢\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(1\right)=2$$
25	22 24	eqtrdi	$$⊢k=1\to \left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)=2$$
26		fveq2	$$⊢k=2\to \left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)=\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(2\right)$$
27	4 4	fvpr2	$$⊢1\ne 2\to \left\{⟨1,2⟩,⟨2,2⟩\right\}\left(2\right)=2$$
28	2 27	ax-mp	$$⊢\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(2\right)=2$$
29	26 28	eqtrdi	$$⊢k=2\to \left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)=2$$
30		id	$$⊢2\in ℂ\to 2\in ℂ$$
31	30	ancri	$$⊢2\in ℂ\to \left(2\in ℂ\wedge 2\in ℂ\right)$$
32	3	jctl	$$⊢2\in ℂ\to \left(1\in \mathrm{V}\wedge 2\in ℂ\right)$$
33	2	a1i	$$⊢2\in ℂ\to 1\ne 2$$
34	25 29 31 32 33	sumpr	$$⊢2\in ℂ\to \sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)=2+2$$
35	21 34	ax-mp	$$⊢\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)=2+2$$
36		2p2e4	$$⊢2+2=4$$
37	35 36	eqtr2i	$$⊢4=\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)$$
38	20 37	pm3.2i	$$⊢\left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)\right)$$
39		fveq1	$$⊢f=\left\{⟨1,2⟩,⟨2,2⟩\right\}\to f\left(k\right)=\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)$$
40	39	sumeq2sdv	$$⊢f=\left\{⟨1,2⟩,⟨2,2⟩\right\}\to \sum _{k\in \left\{1,2\right\}}f\left(k\right)=\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)$$
41	40	eqeq2d	$$⊢f=\left\{⟨1,2⟩,⟨2,2⟩\right\}\to \left(4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\leftrightarrow 4=\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)\right)$$
42	41	anbi2d	$$⊢f=\left\{⟨1,2⟩,⟨2,2⟩\right\}\to \left(\left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)\leftrightarrow \left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)\right)\right)$$
43	42	rspcev	$$⊢\left(\left\{⟨1,2⟩,⟨2,2⟩\right\}\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)\wedge \left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}\left\{⟨1,2⟩,⟨2,2⟩\right\}\left(k\right)\right)\right)\to \exists f\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)\left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)$$
44	16 38 43	mp2an	$$⊢\exists f\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)\left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)$$
45		oveq2	$$⊢d=2\to \left(1\dots d\right)=\left(1\dots 2\right)$$
46		df-2	$$⊢2=1+1$$
47	46	oveq2i	$$⊢\left(1\dots 2\right)=\left(1\dots 1+1\right)$$
48		1z	$$⊢1\in \mathbb{Z}$$
49		fzpr	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+1\right)=\left\{1,1+1\right\}$$
50	48 49	ax-mp	$$⊢\left(1\dots 1+1\right)=\left\{1,1+1\right\}$$
51		1p1e2	$$⊢1+1=2$$
52	51	preq2i	$$⊢\left\{1,1+1\right\}=\left\{1,2\right\}$$
53	50 52	eqtri	$$⊢\left(1\dots 1+1\right)=\left\{1,2\right\}$$
54	47 53	eqtri	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$
55	45 54	eqtrdi	$$⊢d=2\to \left(1\dots d\right)=\left\{1,2\right\}$$
56	55	oveq2d	$$⊢d=2\to {\mathbb{P}}^{\left(1\dots d\right)}={\mathbb{P}}^{\left\{1,2\right\}}$$
57		breq1	$$⊢d=2\to \left(d\le 3\leftrightarrow 2\le 3\right)$$
58	55	sumeq1d	$$⊢d=2\to \sum _{k=1}^{d}f\left(k\right)=\sum _{k\in \left\{1,2\right\}}f\left(k\right)$$
59	58	eqeq2d	$$⊢d=2\to \left(4=\sum _{k=1}^{d}f\left(k\right)\leftrightarrow 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)$$
60	57 59	anbi12d	$$⊢d=2\to \left(\left(d\le 3\wedge 4=\sum _{k=1}^{d}f\left(k\right)\right)\leftrightarrow \left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)\right)$$
61	56 60	rexeqbidv	$$⊢d=2\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)\leftrightarrow \exists f\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)\left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)\right)$$
62	61	rspcev	$$⊢\left(2\in \mathbb{N}\wedge \exists f\in \left({\mathbb{P}}^{\left\{1,2\right\}}\right)\left(2\le 3\wedge 4=\sum _{k\in \left\{1,2\right\}}f\left(k\right)\right)\right)\to \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)$$
63	1 44 62	mp2an	$$⊢\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)$$