nnsum4primesoddALTV

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

		Ref	Expression
	Assertion	nnsum4primesoddALTV	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to ((N \in ℤ_{\geq 8} \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 (7 < m \leftrightarrow 7 < N)$
2		eleq1	$⊢ m = N \to (m \in GoldbachOdd \leftrightarrow N \in GoldbachOdd)$
3	1 2	imbi12d	$⊢ m = N \to ((7 < m \to m \in GoldbachOdd) \leftrightarrow (7 < N \to N \in GoldbachOdd))$
4	3	rspcv	$⊢ N \in Odd \to (\forall m \in Odd (7 < m \to m \in GoldbachOdd) \to (7 < N \to N \in GoldbachOdd))$
5	4	adantl	$⊢ (N \in ℤ_{\geq 8} \land N \in Odd) \to (\forall m \in Odd (7 < m \to m \in GoldbachOdd) \to (7 < N \to N \in GoldbachOdd))$
6		eluz2	$⊢ N \in ℤ_{\geq 8} \leftrightarrow (8 \in ℤ \land N \in ℤ \land 8 \leq N)$
7		7lt8	$⊢ 7 < 8$
8		7re	$⊢ 7 \in ℝ$
9	8	a1i	$⊢ N \in ℤ \to 7 \in ℝ$
10		8re	$⊢ 8 \in ℝ$
11	10	a1i	$⊢ N \in ℤ \to 8 \in ℝ$
12		zre	$⊢ N \in ℤ \to N \in ℝ$
13		ltletr	$⊢ (7 \in ℝ \land 8 \in ℝ \land N \in ℝ) \to ((7 < 8 \land 8 \leq N) \to 7 < N)$
14	9 11 12 13	syl3anc	$⊢ N \in ℤ \to ((7 < 8 \land 8 \leq N) \to 7 < N)$
15	7 14	mpani	$⊢ N \in ℤ \to (8 \leq N \to 7 < N)$
16	15	imp	$⊢ (N \in ℤ \land 8 \leq N) \to 7 < N$
17	16	3adant1	$⊢ (8 \in ℤ \land N \in ℤ \land 8 \leq N) \to 7 < N$
18	6 17	sylbi	$⊢ N \in ℤ_{\geq 8} \to 7 < N$
19	18	adantr	$⊢ (N \in ℤ_{\geq 8} \land N \in Odd) \to 7 < N$
20		pm2.27	$⊢ 7 < N \to ((7 < N \to N \in GoldbachOdd) \to N \in GoldbachOdd)$
21	19 20	syl	$⊢ (N \in ℤ_{\geq 8} \land N \in Odd) \to ((7 < N \to N \in GoldbachOdd) \to N \in GoldbachOdd)$
22		isgbo	$⊢ N \in GoldbachOdd \leftrightarrow (N \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 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	adantld	$⊢ ((p \in ℙ \land q \in ℙ) \land r \in ℙ) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land N = p + q + r) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
104	103	rexlimdva	$⊢ (p \in ℙ \land q \in ℙ) \to (\exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land N = p + q + r) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
105	104	rexlimivv	$⊢ \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land N = p + q + r) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k)$
106	105	adantl	$⊢ (N \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land N = p + q + r)) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k)$
107	22 106	sylbi	$⊢ N \in GoldbachOdd \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k)$
108	107	a1i	$⊢ (N \in ℤ_{\geq 8} \land N \in Odd) \to (N \in GoldbachOdd \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
109	5 21 108	3syld	$⊢ (N \in ℤ_{\geq 8} \land N \in Odd) \to (\forall m \in Odd (7 < m \to m \in GoldbachOdd) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$
110	109	com12	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to ((N \in ℤ_{\geq 8} \land N \in Odd) \to \exists f \in (ℙ^{(1 \dots 3)}) N = \sum_{k = 1}^{3} f (k))$

Metamath Proof Explorer

Theorem nnsum4primesoddALTV

Proof