nnsum3primesgbe

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

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

Proof

Step	Hyp	Ref	Expression
1		isgbe	$⊢ N \in GoldbachEven \leftrightarrow (N \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land N = p + q))$
2		2nn	$⊢ 2 \in ℕ$
3	2	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \to 2 \in ℕ$
4		oveq2	$⊢ d = 2 \to (1 \dots d) = (1 \dots 2)$
5		df-2	$⊢ 2 = 1 + 1$
6	5	oveq2i	$⊢ (1 \dots 2) = (1 \dots 1 + 1)$
7		1z	$⊢ 1 \in ℤ$
8		fzpr	$⊢ 1 \in ℤ \to (1 \dots 1 + 1) = \{1, 1 + 1\}$
9	7 8	ax-mp	$⊢ (1 \dots 1 + 1) = \{1, 1 + 1\}$
10		1p1e2	$⊢ 1 + 1 = 2$
11	10	preq2i	$⊢ \{1, 1 + 1\} = \{1, 2\}$
12	6 9 11	3eqtri	$⊢ (1 \dots 2) = \{1, 2\}$
13	4 12	eqtrdi	$⊢ d = 2 \to (1 \dots d) = \{1, 2\}$
14	13	oveq2d	$⊢ d = 2 \to ℙ^{(1 \dots d)} = ℙ^{\{1, 2\}}$
15		breq1	$⊢ d = 2 \to (d \leq 3 \leftrightarrow 2 \leq 3)$
16	13	sumeq1d	$⊢ d = 2 \to \sum_{k = 1}^{d} f (k) = \sum_{k \in \{1, 2\}} f (k)$
17	16	eqeq2d	$⊢ d = 2 \to (N = \sum_{k = 1}^{d} f (k) \leftrightarrow N = \sum_{k \in \{1, 2\}} f (k))$
18	15 17	anbi12d	$⊢ d = 2 \to ((d \leq 3 \land N = \sum_{k = 1}^{d} f (k)) \leftrightarrow (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)))$
19	14 18	rexeqbidv	$⊢ d = 2 \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)))$
20	19	adantl	$⊢ (((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \land d = 2) \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)))$
21		1ne2	$⊢ 1 \neq 2$
22		1ex	$⊢ 1 \in V$
23		2ex	$⊢ 2 \in V$
24		vex	$⊢ p \in V$
25		vex	$⊢ q \in V$
26	22 23 24 25	fpr	$⊢ 1 \neq 2 \to \{⟨1, p⟩, ⟨2, q⟩\} : \{1, 2\} ⟶ \{p, q\}$
27	21 26	mp1i	$⊢ (p \in ℙ \land q \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩\} : \{1, 2\} ⟶ \{p, q\}$
28		prssi	$⊢ (p \in ℙ \land q \in ℙ) \to \{p, q\} \subseteq ℙ$
29	27 28	fssd	$⊢ (p \in ℙ \land q \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩\} : \{1, 2\} ⟶ ℙ$
30		prmex	$⊢ ℙ \in V$
31		prex	$⊢ \{1, 2\} \in V$
32	30 31	pm3.2i	$⊢ (ℙ \in V \land \{1, 2\} \in V)$
33		elmapg	$⊢ (ℙ \in V \land \{1, 2\} \in V) \to (\{⟨1, p⟩, ⟨2, q⟩\} \in (ℙ^{\{1, 2\}}) \leftrightarrow \{⟨1, p⟩, ⟨2, q⟩\} : \{1, 2\} ⟶ ℙ)$
34	32 33	mp1i	$⊢ (p \in ℙ \land q \in ℙ) \to (\{⟨1, p⟩, ⟨2, q⟩\} \in (ℙ^{\{1, 2\}}) \leftrightarrow \{⟨1, p⟩, ⟨2, q⟩\} : \{1, 2\} ⟶ ℙ)$
35	29 34	mpbird	$⊢ (p \in ℙ \land q \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩\} \in (ℙ^{\{1, 2\}})$
36		fveq1	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩\} \to f (k) = \{⟨1, p⟩, ⟨2, q⟩\} (k)$
37	36	adantr	$⊢ (f = \{⟨1, p⟩, ⟨2, q⟩\} \land k \in \{1, 2\}) \to f (k) = \{⟨1, p⟩, ⟨2, q⟩\} (k)$
38	37	sumeq2dv	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩\} \to \sum_{k \in \{1, 2\}} f (k) = \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k)$
39	38	eqeq1d	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩\} \to (\sum_{k \in \{1, 2\}} f (k) = p + q \leftrightarrow \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k) = p + q)$
40	39	anbi2d	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩\} \to ((2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q) \leftrightarrow (2 \leq 3 \land \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k) = p + q))$
41	40	adantl	$⊢ ((p \in ℙ \land q \in ℙ) \land f = \{⟨1, p⟩, ⟨2, q⟩\}) \to ((2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q) \leftrightarrow (2 \leq 3 \land \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k) = p + q))$
42		prmz	$⊢ p \in ℙ \to p \in ℤ$
43		prmz	$⊢ q \in ℙ \to q \in ℤ$
44		fveq2	$⊢ k = 1 \to \{⟨1, p⟩, ⟨2, q⟩\} (k) = \{⟨1, p⟩, ⟨2, q⟩\} (1)$
45	22 24	fvpr1	$⊢ 1 \neq 2 \to \{⟨1, p⟩, ⟨2, q⟩\} (1) = p$
46	21 45	ax-mp	$⊢ \{⟨1, p⟩, ⟨2, q⟩\} (1) = p$
47	44 46	eqtrdi	$⊢ k = 1 \to \{⟨1, p⟩, ⟨2, q⟩\} (k) = p$
48		fveq2	$⊢ k = 2 \to \{⟨1, p⟩, ⟨2, q⟩\} (k) = \{⟨1, p⟩, ⟨2, q⟩\} (2)$
49	23 25	fvpr2	$⊢ 1 \neq 2 \to \{⟨1, p⟩, ⟨2, q⟩\} (2) = q$
50	21 49	ax-mp	$⊢ \{⟨1, p⟩, ⟨2, q⟩\} (2) = q$
51	48 50	eqtrdi	$⊢ k = 2 \to \{⟨1, p⟩, ⟨2, q⟩\} (k) = q$
52		zcn	$⊢ p \in ℤ \to p \in ℂ$
53		zcn	$⊢ q \in ℤ \to q \in ℂ$
54	52 53	anim12i	$⊢ (p \in ℤ \land q \in ℤ) \to (p \in ℂ \land q \in ℂ)$
55	7 2	pm3.2i	$⊢ (1 \in ℤ \land 2 \in ℕ)$
56	55	a1i	$⊢ (p \in ℤ \land q \in ℤ) \to (1 \in ℤ \land 2 \in ℕ)$
57	21	a1i	$⊢ (p \in ℤ \land q \in ℤ) \to 1 \neq 2$
58	47 51 54 56 57	sumpr	$⊢ (p \in ℤ \land q \in ℤ) \to \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k) = p + q$
59	42 43 58	syl2an	$⊢ (p \in ℙ \land q \in ℙ) \to \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k) = p + q$
60		2re	$⊢ 2 \in ℝ$
61		3re	$⊢ 3 \in ℝ$
62		2lt3	$⊢ 2 < 3$
63	60 61 62	ltleii	$⊢ 2 \leq 3$
64	59 63	jctil	$⊢ (p \in ℙ \land q \in ℙ) \to (2 \leq 3 \land \sum_{k \in \{1, 2\}} \{⟨1, p⟩, ⟨2, q⟩\} (k) = p + q)$
65	35 41 64	rspcedvd	$⊢ (p \in ℙ \land q \in ℙ) \to \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q)$
66	65	adantr	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \to \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q)$
67		eqeq1	$⊢ N = p + q \to (N = \sum_{k \in \{1, 2\}} f (k) \leftrightarrow p + q = \sum_{k \in \{1, 2\}} f (k))$
68		eqcom	$⊢ p + q = \sum_{k \in \{1, 2\}} f (k) \leftrightarrow \sum_{k \in \{1, 2\}} f (k) = p + q$
69	67 68	bitrdi	$⊢ N = p + q \to (N = \sum_{k \in \{1, 2\}} f (k) \leftrightarrow \sum_{k \in \{1, 2\}} f (k) = p + q)$
70	69	anbi2d	$⊢ N = p + q \to ((2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)) \leftrightarrow (2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q))$
71	70	rexbidv	$⊢ N = p + q \to (\exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)) \leftrightarrow \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q))$
72	71	3ad2ant3	$⊢ (p \in Odd \land q \in Odd \land N = p + q) \to (\exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)) \leftrightarrow \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q))$
73	72	adantl	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \to (\exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k)) \leftrightarrow \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land \sum_{k \in \{1, 2\}} f (k) = p + q))$
74	66 73	mpbird	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \to \exists f \in (ℙ^{\{1, 2\}}) (2 \leq 3 \land N = \sum_{k \in \{1, 2\}} f (k))$
75	3 20 74	rspcedvd	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k))$
76	75	a1d	$⊢ ((p \in ℙ \land q \in ℙ) \land (p \in Odd \land q \in Odd \land N = p + q)) \to (N \in Even \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k)))$
77	76	ex	$⊢ (p \in ℙ \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land N = p + q) \to (N \in Even \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k))))$
78	77	rexlimivv	$⊢ \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land N = p + q) \to (N \in Even \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k)))$
79	78	impcom	$⊢ (N \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land N = p + q)) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k))$
80	1 79	sylbi	$⊢ N \in GoldbachEven \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 3 \land N = \sum_{k = 1}^{d} f (k))$

Metamath Proof Explorer

Theorem nnsum3primesgbe

Proof