nnsum4primesodd

Description: If the (weak) ternary Goldbach conjecture is valid, then every odd integer greater than 5 is the sum of 3 primes. (Contributed by AV, 2-Jul-2020)

		Ref	Expression
	Assertion	nnsum4primesodd	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((N \in ℤ_{\geq 6} \land N \in Odd) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$

Proof

Step	Hyp	Ref	Expression
1		breq2	$⊢ m = N \to (5 < m \leftrightarrow 5 < N)$
2		eleq1	$⊢ m = N \to (m \in GoldbachOddW \leftrightarrow N \in GoldbachOddW)$
3	1 2	imbi12d	$⊢ m = N \to ((5 < m \to m \in GoldbachOddW) \leftrightarrow (5 < N \to N \in GoldbachOddW))$
4	3	rspcv	$⊢ N \in Odd \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to (5 < N \to N \in GoldbachOddW))$
5	4	adantl	$⊢ (N \in ℤ_{\geq 6} \land N \in Odd) \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to (5 < N \to N \in GoldbachOddW))$
6		eluz2	$⊢ N \in ℤ_{\geq 6} \leftrightarrow (6 \in ℤ \land N \in ℤ \land 6 \leq N)$
7		5lt6	$⊢ 5 < 6$
8		5re	$⊢ 5 \in ℝ$
9	8	a1i	$⊢ N \in ℤ \to 5 \in ℝ$
10		6re	$⊢ 6 \in ℝ$
11	10	a1i	$⊢ N \in ℤ \to 6 \in ℝ$
12		zre	$⊢ N \in ℤ \to N \in ℝ$
13		ltletr	$⊢ (5 \in ℝ \land 6 \in ℝ \land N \in ℝ) \to ((5 < 6 \land 6 \leq N) \to 5 < N)$
14	9 11 12 13	syl3anc	$⊢ N \in ℤ \to ((5 < 6 \land 6 \leq N) \to 5 < N)$
15	7 14	mpani	$⊢ N \in ℤ \to (6 \leq N \to 5 < N)$
16	15	imp	$⊢ (N \in ℤ \land 6 \leq N) \to 5 < N$
17	16	3adant1	$⊢ (6 \in ℤ \land N \in ℤ \land 6 \leq N) \to 5 < N$
18	6 17	sylbi	$⊢ N \in ℤ_{\geq 6} \to 5 < N$
19	18	adantr	$⊢ (N \in ℤ_{\geq 6} \land N \in Odd) \to 5 < N$
20		pm2.27	$⊢ 5 < N \to ((5 < N \to N \in GoldbachOddW) \to N \in GoldbachOddW)$
21	19 20	syl	$⊢ (N \in ℤ_{\geq 6} \land N \in Odd) \to ((5 < N \to N \in GoldbachOddW) \to N \in GoldbachOddW)$
22		isgbow	$⊢ N \in GoldbachOddW \leftrightarrow (N \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ N = p + q + r)$
23		1ex	$⊢ 1 \in V$
24		2ex	$⊢ 2 \in V$
25		3ex	$⊢ 3 \in V$
26		vex	$⊢ p \in V$
27		vex	$⊢ q \in V$
28		vex	$⊢ r \in V$
29		1ne2	$⊢ 1 \neq 2$
30		1re	$⊢ 1 \in ℝ$
31		1lt3	$⊢ 1 < 3$
32	30 31	ltneii	$⊢ 1 \neq 3$
33		2re	$⊢ 2 \in ℝ$
34		2lt3	$⊢ 2 < 3$
35	33 34	ltneii	$⊢ 2 \neq 3$
36	23 24 25 26 27 28 29 32 35	ftp	$⊢ \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : \{1, 2, 3\} ⟶ \{p, q, r\}$
37	36	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : \{1, 2, 3\} ⟶ \{p, q, r\}$
38		1p2e3	$⊢ 1 + 2 = 3$
39	38	eqcomi	$⊢ 3 = 1 + 2$
40	39	oveq2i	$⊢ (1 \dots 3) = (1 \dots 1 + 2)$
41		1z	$⊢ 1 \in ℤ$
42		fztp	$⊢ 1 \in ℤ \to (1 \dots 1 + 2) = \{1, 1 + 1, 1 + 2\}$
43	41 42	ax-mp	$⊢ (1 \dots 1 + 2) = \{1, 1 + 1, 1 + 2\}$
44		eqid	$⊢ 1 = 1$
45		id	$⊢ 1 = 1 \to 1 = 1$
46		1p1e2	$⊢ 1 + 1 = 2$
47	46	a1i	$⊢ 1 = 1 \to 1 + 1 = 2$
48	38	a1i	$⊢ 1 = 1 \to 1 + 2 = 3$
49	45 47 48	tpeq123d	$⊢ 1 = 1 \to \{1, 1 + 1, 1 + 2\} = \{1, 2, 3\}$
50	44 49	ax-mp	$⊢ \{1, 1 + 1, 1 + 2\} = \{1, 2, 3\}$
51	40 43 50	3eqtri	$⊢ (1 \dots 3) = \{1, 2, 3\}$
52	51	feq2i	$⊢ \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : (1 \dots 3) ⟶ \{p, q, r\} \leftrightarrow \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : \{1, 2, 3\} ⟶ \{p, q, r\}$
53	37 52	sylibr	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : (1 \dots 3) ⟶ \{p, q, r\}$
54		df-3an	$⊢ (p \in ℙ \land q \in ℙ \land r \in ℙ) \leftrightarrow ((p \in ℙ \land q \in ℙ) \land r \in ℙ)$
55	26 27 28	tpss	$⊢ (p \in ℙ \land q \in ℙ \land r \in ℙ) \leftrightarrow \{p, q, r\} \subseteq ℙ$
56	54 55	sylbb1	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \{p, q, r\} \subseteq ℙ$
57	53 56	fssd	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : (1 \dots 3) ⟶ ℙ$
58		prmex	$⊢ ℙ \in V$
59		ovex	$⊢ (1 \dots 3) \in V$
60	58 59	pm3.2i	$⊢ (ℙ \in V \land (1 \dots 3) \in V)$
61		elmapg	$⊢ (ℙ \in V \land (1 \dots 3) \in V) \to (\{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} \in (ℙ^{(1 \dots 3)}) \leftrightarrow \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : (1 \dots 3) ⟶ ℙ)$
62	60 61	mp1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (\{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} \in (ℙ^{(1 \dots 3)}) \leftrightarrow \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} : (1 \dots 3) ⟶ ℙ)$
63	57 62	mpbird	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} \in (ℙ^{(1 \dots 3)})$
64		fveq1	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} \to f (k) = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k)$
65	64	sumeq2sdv	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} \to \sum_{k = 1}^{3} f (k) = \sum_{k = 1}^{3} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k)$
66	65	eqeq2d	$⊢ f = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} \to (p + q + r = \sum_{k = 1}^{3} f (k) \leftrightarrow p + q + r = \sum_{k = 1}^{3} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k))$
67	66	adantl	$⊢ (((p \in ℙ \land q \in ℙ) \land r \in ℙ) \land f = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\}) \to (p + q + r = \sum_{k = 1}^{3} f (k) \leftrightarrow p + q + r = \sum_{k = 1}^{3} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k))$
68	51	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (1 \dots 3) = \{1, 2, 3\}$
69	68	sumeq1d	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \sum_{k = 1}^{3} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = \sum_{k \in \{1, 2, 3\}} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k)$
70		fveq2	$⊢ k = 1 \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (1)$
71	23 26	fvtp1	$⊢ (1 \neq 2 \land 1 \neq 3) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (1) = p$
72	29 32 71	mp2an	$⊢ \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (1) = p$
73	70 72	eqtrdi	$⊢ k = 1 \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = p$
74		fveq2	$⊢ k = 2 \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (2)$
75	24 27	fvtp2	$⊢ (1 \neq 2 \land 2 \neq 3) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (2) = q$
76	29 35 75	mp2an	$⊢ \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (2) = q$
77	74 76	eqtrdi	$⊢ k = 2 \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = q$
78		fveq2	$⊢ k = 3 \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (3)$
79	25 28	fvtp3	$⊢ (1 \neq 3 \land 2 \neq 3) \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (3) = r$
80	32 35 79	mp2an	$⊢ \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (3) = r$
81	78 80	eqtrdi	$⊢ k = 3 \to \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = r$
82		prmz	$⊢ p \in ℙ \to p \in ℤ$
83	82	zcnd	$⊢ p \in ℙ \to p \in ℂ$
84		prmz	$⊢ q \in ℙ \to q \in ℤ$
85	84	zcnd	$⊢ q \in ℙ \to q \in ℂ$
86		prmz	$⊢ r \in ℙ \to r \in ℤ$
87	86	zcnd	$⊢ r \in ℙ \to r \in ℂ$
88	83 85 87	3anim123i	$⊢ (p \in ℙ \land q \in ℙ \land r \in ℙ) \to (p \in ℂ \land q \in ℂ \land r \in ℂ)$
89	88	3expa	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (p \in ℂ \land q \in ℂ \land r \in ℂ)$
90		2z	$⊢ 2 \in ℤ$
91		3z	$⊢ 3 \in ℤ$
92	41 90 91	3pm3.2i	$⊢ (1 \in ℤ \land 2 \in ℤ \land 3 \in ℤ)$
93	92	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (1 \in ℤ \land 2 \in ℤ \land 3 \in ℤ)$
94	29	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to 1 \neq 2$
95	32	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to 1 \neq 3$
96	35	a1i	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to 2 \neq 3$
97	73 77 81 89 93 94 95 96	sumtp	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \sum_{k \in \{1, 2, 3\}} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k) = p + q + r$
98	69 97	eqtr2d	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to p + q + r = \sum_{k = 1}^{3} \{⟨1, p⟩, ⟨2, q⟩, ⟨3, r⟩\} (k)$
99	63 67 98	rspcedvd	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to \exists f \in (ℙ^{(1 \dots 3)}) p + q + r = \sum_{k = 1}^{3} f (k)$
100		eqeq1	$⊢ N = p + q + r \to (N = \sum_{k = 1}^{3} f (k) \leftrightarrow p + q + r = \sum_{k = 1}^{3} f (k))$
101	100	rexbidv	$⊢ N = p + q + r \to (\exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k) \leftrightarrow \exists f \in (ℙ^{(1 \dots 3)}) p + q + r = \sum_{k = 1}^{3} f (k))$
102	99 101	syl5ibrcom	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (N = p + q + r \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
103	102	rexlimdva	$⊢ (p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ N = p + q + r \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
104	103	rexlimivv	$⊢ \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ N = p + q + r \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k)$
105	104	adantl	$⊢ (N \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ N = p + q + r) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k)$
106	22 105	sylbi	$⊢ N \in GoldbachOddW \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k)$
107	106	a1i	$⊢ (N \in ℤ_{\geq 6} \land N \in Odd) \to (N \in GoldbachOddW \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
108	5 21 107	3syld	$⊢ (N \in ℤ_{\geq 6} \land N \in Odd) \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
109	108	com12	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((N \in ℤ_{\geq 6} \land N \in Odd) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$

Metamath Proof Explorer

Theorem nnsum4primesodd

Proof