nnsum3primesprm

Description: Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020) (Proof shortened by AV, 17-Apr-2021)

		Ref	Expression
	Assertion	nnsum3primesprm	$⊢ P \in ℙ \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land P = \sum_{k = 1}^{d} f (k))$

Proof

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2		1zzd	$⊢ P \in ℙ \to 1 \in ℤ$
3		id	$⊢ P \in ℙ \to P \in ℙ$
4	2 3	fsnd	$⊢ P \in ℙ \to \{⟨1, P⟩\} : \{1\} ⟶ ℙ$
5		prmex	$⊢ ℙ \in V$
6		snex	$⊢ \{1\} \in V$
7	5 6	elmap	$⊢ \{⟨1, P⟩\} \in (ℙ^{\{1\}}) \leftrightarrow \{⟨1, P⟩\} : \{1\} ⟶ ℙ$
8	4 7	sylibr	$⊢ P \in ℙ \to \{⟨1, P⟩\} \in (ℙ^{\{1\}})$
9		1re	$⊢ 1 \in ℝ$
10		simpl	$⊢ (P \in ℙ \land k \in \{1\}) \to P \in ℙ$
11		fvsng	$⊢ (1 \in ℝ \land P \in ℙ) \to \{⟨1, P⟩\} (1) = P$
12	9 10 11	sylancr	$⊢ (P \in ℙ \land k \in \{1\}) \to \{⟨1, P⟩\} (1) = P$
13	12	sumeq2dv	$⊢ P \in ℙ \to \sum_{k \in \{1\}} \{⟨1, P⟩\} (1) = \sum_{k \in \{1\}} P$
14		prmz	$⊢ P \in ℙ \to P \in ℤ$
15	14	zcnd	$⊢ P \in ℙ \to P \in ℂ$
16		eqidd	$⊢ k = 1 \to P = P$
17	16	sumsn	$⊢ (1 \in ℝ \land P \in ℂ) \to \sum_{k \in \{1\}} P = P$
18	9 15 17	sylancr	$⊢ P \in ℙ \to \sum_{k \in \{1\}} P = P$
19	13 18	eqtr2d	$⊢ P \in ℙ \to P = \sum_{k \in \{1\}} \{⟨1, P⟩\} (1)$
20		1le3	$⊢ 1 \leq 3$
21	19 20	jctil	$⊢ P \in ℙ \to (1 \leq 3 \land P = \sum_{k \in \{1\}} \{⟨1, P⟩\} (1))$
22		simpl	$⊢ (f = \{⟨1, P⟩\} \land k \in \{1\}) \to f = \{⟨1, P⟩\}$
23		elsni	$⊢ k \in \{1\} \to k = 1$
24	23	adantl	$⊢ (f = \{⟨1, P⟩\} \land k \in \{1\}) \to k = 1$
25	22 24	fveq12d	$⊢ (f = \{⟨1, P⟩\} \land k \in \{1\}) \to f (k) = \{⟨1, P⟩\} (1)$
26	25	sumeq2dv	$⊢ f = \{⟨1, P⟩\} \to \sum_{k \in \{1\}} f (k) = \sum_{k \in \{1\}} \{⟨1, P⟩\} (1)$
27	26	eqeq2d	$⊢ f = \{⟨1, P⟩\} \to (P = \sum_{k \in \{1\}} f (k) \leftrightarrow P = \sum_{k \in \{1\}} \{⟨1, P⟩\} (1))$
28	27	anbi2d	$⊢ f = \{⟨1, P⟩\} \to ((1 \leq 3 \land P = \sum_{k \in \{1\}} f (k)) \leftrightarrow (1 \leq 3 \land P = \sum_{k \in \{1\}} \{⟨1, P⟩\} (1)))$
29	28	rspcev	$⊢ (\{⟨1, P⟩\} \in (ℙ^{\{1\}}) \land (1 \leq 3 \land P = \sum_{k \in \{1\}} \{⟨1, P⟩\} (1))) \to \exists f \in (ℙ^{\{1\}}) (1 \leq 3 \land P = \sum_{k \in \{1\}} f (k))$
30	8 21 29	syl2anc	$⊢ P \in ℙ \to \exists f \in (ℙ^{\{1\}}) (1 \leq 3 \land P = \sum_{k \in \{1\}} f (k))$
31		oveq2	$⊢ d = 1 \to (1 \dots d) = (1 \dots 1)$
32		1z	$⊢ 1 \in ℤ$
33		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
34	32 33	ax-mp	$⊢ (1 \dots 1) = \{1\}$
35	31 34	eqtrdi	$⊢ d = 1 \to (1 \dots d) = \{1\}$
36	35	oveq2d	$⊢ d = 1 \to ℙ^{(1 \dots d)} = ℙ^{\{1\}}$
37		breq1	$⊢ d = 1 \to (d \leq 3 \leftrightarrow 1 \leq 3)$
38	35	sumeq1d	$⊢ d = 1 \to \sum_{k = 1}^{d} f (k) = \sum_{k \in \{1\}} f (k)$
39	38	eqeq2d	$⊢ d = 1 \to (P = \sum_{k = 1}^{d} f (k) \leftrightarrow P = \sum_{k \in \{1\}} f (k))$
40	37 39	anbi12d	$⊢ d = 1 \to ((d \leq 3 \land P = \sum_{k = 1}^{d} f (k)) \leftrightarrow (1 \leq 3 \land P = \sum_{k \in \{1\}} f (k)))$
41	36 40	rexeqbidv	$⊢ d = 1 \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land P = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{\{1\}}) (1 \leq 3 \land P = \sum_{k \in \{1\}} f (k)))$
42	41	rspcev	$⊢ (1 \in ℕ \land \exists f \in (ℙ^{\{1\}}) (1 \leq 3 \land P = \sum_{k \in \{1\}} f (k))) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land P = \sum_{k = 1}^{d} f (k))$
43	1 30 42	sylancr	$⊢ P \in ℙ \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land P = \sum_{k = 1}^{d} f (k))$

Metamath Proof Explorer

Theorem nnsum3primesprm

Proof