sbgoldbo

Description: If the strong binary Goldbach conjecture is valid, the original formulation of the Goldbach conjecture also holds: Every integer greater than 2 can be expressed as the sum of three "primes" with regarding 1 to be a prime (as Goldbach did). Original text: "Es scheint wenigstens, dass eine jede Zahl, die groesser ist als 2, ein aggregatum trium numerorum primorum sey." (Goldbach, 1742). (Contributed by AV, 25-Dec-2021)

		Ref	Expression
	Hypothesis	sbgoldbo.p	$⊢ P = \{1\} \cup ℙ$
	Assertion	sbgoldbo	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to \forall n \in ℤ_{\geq 3} \exists p \in P \exists q \in P \exists r \in P n = p + q + r$

Proof

Step	Hyp	Ref	Expression
1		sbgoldbo.p	$⊢ P = \{1\} \cup ℙ$
2		nfra1	$⊢ Ⅎ n \forall n \in Even (4 < n \to n \in GoldbachEven)$
3		3z	$⊢ 3 \in ℤ$
4		6nn	$⊢ 6 \in ℕ$
5	4	nnzi	$⊢ 6 \in ℤ$
6		3re	$⊢ 3 \in ℝ$
7		6re	$⊢ 6 \in ℝ$
8		3lt6	$⊢ 3 < 6$
9	6 7 8	ltleii	$⊢ 3 \leq 6$
10		eluz2	$⊢ 6 \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 6 \in ℤ \land 3 \leq 6)$
11	3 5 9 10	mpbir3an	$⊢ 6 \in ℤ_{\geq 3}$
12		uzsplit	$⊢ 6 \in ℤ_{\geq 3} \to ℤ_{\geq 3} = (3 \dots 6 - 1) \cup ℤ_{\geq 6}$
13	12	eleq2d	$⊢ 6 \in ℤ_{\geq 3} \to (n \in ℤ_{\geq 3} \leftrightarrow n \in ((3 \dots 6 - 1) \cup ℤ_{\geq 6}))$
14	11 13	ax-mp	$⊢ n \in ℤ_{\geq 3} \leftrightarrow n \in ((3 \dots 6 - 1) \cup ℤ_{\geq 6})$
15		elun	$⊢ n \in ((3 \dots 6 - 1) \cup ℤ_{\geq 6}) \leftrightarrow (n \in (3 \dots 6 - 1) \lor n \in ℤ_{\geq 6})$
16		6m1e5	$⊢ 6 - 1 = 5$
17	16	oveq2i	$⊢ (3 \dots 6 - 1) = (3 \dots 5)$
18		5nn	$⊢ 5 \in ℕ$
19	18	nnzi	$⊢ 5 \in ℤ$
20		5re	$⊢ 5 \in ℝ$
21		3lt5	$⊢ 3 < 5$
22	6 20 21	ltleii	$⊢ 3 \leq 5$
23		eluz2	$⊢ 5 \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land 5 \in ℤ \land 3 \leq 5)$
24	3 19 22 23	mpbir3an	$⊢ 5 \in ℤ_{\geq 3}$
25		fzopredsuc	$⊢ 5 \in ℤ_{\geq 3} \to (3 \dots 5) = (\{3\} \cup (3 + 1 ..^5)) \cup \{5\}$
26	24 25	ax-mp	$⊢ (3 \dots 5) = (\{3\} \cup (3 + 1 ..^5)) \cup \{5\}$
27	17 26	eqtri	$⊢ (3 \dots 6 - 1) = (\{3\} \cup (3 + 1 ..^5)) \cup \{5\}$
28	27	eleq2i	$⊢ n \in (3 \dots 6 - 1) \leftrightarrow n \in ((\{3\} \cup (3 + 1 ..^5)) \cup \{5\})$
29		elun	$⊢ n \in ((\{3\} \cup (3 + 1 ..^5)) \cup \{5\}) \leftrightarrow (n \in (\{3\} \cup (3 + 1 ..^5)) \lor n \in \{5\})$
30		elun	$⊢ n \in (\{3\} \cup (3 + 1 ..^5)) \leftrightarrow (n \in \{3\} \lor n \in (3 + 1 ..^5))$
31		elsni	$⊢ n \in \{3\} \to n = 3$
32		1ex	$⊢ 1 \in V$
33	32	snid	$⊢ 1 \in \{1\}$
34	33	orci	$⊢ (1 \in \{1\} \lor 1 \in ℙ)$
35		elun	$⊢ 1 \in (\{1\} \cup ℙ) \leftrightarrow (1 \in \{1\} \lor 1 \in ℙ)$
36	34 35	mpbir	$⊢ 1 \in (\{1\} \cup ℙ)$
37	36 1	eleqtrri	$⊢ 1 \in P$
38	37	a1i	$⊢ n = 3 \to 1 \in P$
39		simpl	$⊢ (n = 3 \land p = 1) \to n = 3$
40		oveq1	$⊢ p = 1 \to p + q = 1 + q$
41	40	oveq1d	$⊢ p = 1 \to p + q + r = 1 + q + r$
42	41	adantl	$⊢ (n = 3 \land p = 1) \to p + q + r = 1 + q + r$
43	39 42	eqeq12d	$⊢ (n = 3 \land p = 1) \to (n = p + q + r \leftrightarrow 3 = 1 + q + r)$
44	43	2rexbidv	$⊢ (n = 3 \land p = 1) \to (\exists q \in P \exists r \in P n = p + q + r \leftrightarrow \exists q \in P \exists r \in P 3 = 1 + q + r)$
45		oveq2	$⊢ q = 1 \to 1 + q = 1 + 1$
46	45	oveq1d	$⊢ q = 1 \to 1 + q + r = 1 + 1 + r$
47	46	eqeq2d	$⊢ q = 1 \to (3 = 1 + q + r \leftrightarrow 3 = 1 + 1 + r)$
48	47	rexbidv	$⊢ q = 1 \to (\exists r \in P 3 = 1 + q + r \leftrightarrow \exists r \in P 3 = 1 + 1 + r)$
49	48	adantl	$⊢ (n = 3 \land q = 1) \to (\exists r \in P 3 = 1 + q + r \leftrightarrow \exists r \in P 3 = 1 + 1 + r)$
50		df-3	$⊢ 3 = 2 + 1$
51		df-2	$⊢ 2 = 1 + 1$
52	51	oveq1i	$⊢ 2 + 1 = 1 + 1 + 1$
53	50 52	eqtri	$⊢ 3 = 1 + 1 + 1$
54		oveq2	$⊢ r = 1 \to 1 + 1 + r = 1 + 1 + 1$
55	53 54	eqtr4id	$⊢ r = 1 \to 3 = 1 + 1 + r$
56	55	adantl	$⊢ (n = 3 \land r = 1) \to 3 = 1 + 1 + r$
57	38 56	rspcedeqvd	$⊢ n = 3 \to \exists r \in P 3 = 1 + 1 + r$
58	38 49 57	rspcedvd	$⊢ n = 3 \to \exists q \in P \exists r \in P 3 = 1 + q + r$
59	38 44 58	rspcedvd	$⊢ n = 3 \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
60	31 59	syl	$⊢ n \in \{3\} \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
61		3p1e4	$⊢ 3 + 1 = 4$
62		df-5	$⊢ 5 = 4 + 1$
63	61 62	oveq12i	$⊢ (3 + 1 ..^5) = (4 ..^4 + 1)$
64		4z	$⊢ 4 \in ℤ$
65		fzval3	$⊢ 4 \in ℤ \to (4 \dots 4) = (4 ..^4 + 1)$
66	64 65	ax-mp	$⊢ (4 \dots 4) = (4 ..^4 + 1)$
67	63 66	eqtr4i	$⊢ (3 + 1 ..^5) = (4 \dots 4)$
68	67	eleq2i	$⊢ n \in (3 + 1 ..^5) \leftrightarrow n \in (4 \dots 4)$
69		fzsn	$⊢ 4 \in ℤ \to (4 \dots 4) = \{4\}$
70	64 69	ax-mp	$⊢ (4 \dots 4) = \{4\}$
71	70	eleq2i	$⊢ n \in (4 \dots 4) \leftrightarrow n \in \{4\}$
72	68 71	bitri	$⊢ n \in (3 + 1 ..^5) \leftrightarrow n \in \{4\}$
73		elsni	$⊢ n \in \{4\} \to n = 4$
74		2prm	$⊢ 2 \in ℙ$
75	74	olci	$⊢ (2 \in \{1\} \lor 2 \in ℙ)$
76		elun	$⊢ 2 \in (\{1\} \cup ℙ) \leftrightarrow (2 \in \{1\} \lor 2 \in ℙ)$
77	75 76	mpbir	$⊢ 2 \in (\{1\} \cup ℙ)$
78	77 1	eleqtrri	$⊢ 2 \in P$
79	78	a1i	$⊢ n = 4 \to 2 \in P$
80		oveq1	$⊢ p = 2 \to p + q = 2 + q$
81	80	oveq1d	$⊢ p = 2 \to p + q + r = 2 + q + r$
82	81	eqeq2d	$⊢ p = 2 \to (n = p + q + r \leftrightarrow n = 2 + q + r)$
83	82	2rexbidv	$⊢ p = 2 \to (\exists q \in P \exists r \in P n = p + q + r \leftrightarrow \exists q \in P \exists r \in P n = 2 + q + r)$
84	83	adantl	$⊢ (n = 4 \land p = 2) \to (\exists q \in P \exists r \in P n = p + q + r \leftrightarrow \exists q \in P \exists r \in P n = 2 + q + r)$
85	37	a1i	$⊢ n = 4 \to 1 \in P$
86		oveq2	$⊢ q = 1 \to 2 + q = 2 + 1$
87	86	oveq1d	$⊢ q = 1 \to 2 + q + r = 2 + 1 + r$
88	87	eqeq2d	$⊢ q = 1 \to (n = 2 + q + r \leftrightarrow n = 2 + 1 + r)$
89	88	rexbidv	$⊢ q = 1 \to (\exists r \in P n = 2 + q + r \leftrightarrow \exists r \in P n = 2 + 1 + r)$
90	89	adantl	$⊢ (n = 4 \land q = 1) \to (\exists r \in P n = 2 + q + r \leftrightarrow \exists r \in P n = 2 + 1 + r)$
91		simpl	$⊢ (n = 4 \land r = 1) \to n = 4$
92		df-4	$⊢ 4 = 3 + 1$
93	50	oveq1i	$⊢ 3 + 1 = 2 + 1 + 1$
94	92 93	eqtri	$⊢ 4 = 2 + 1 + 1$
95	94	a1i	$⊢ (n = 4 \land r = 1) \to 4 = 2 + 1 + 1$
96		oveq2	$⊢ r = 1 \to 2 + 1 + r = 2 + 1 + 1$
97	96	eqcomd	$⊢ r = 1 \to 2 + 1 + 1 = 2 + 1 + r$
98	97	adantl	$⊢ (n = 4 \land r = 1) \to 2 + 1 + 1 = 2 + 1 + r$
99	95 98	eqtrd	$⊢ (n = 4 \land r = 1) \to 4 = 2 + 1 + r$
100	91 99	eqtrd	$⊢ (n = 4 \land r = 1) \to n = 2 + 1 + r$
101	85 100	rspcedeqvd	$⊢ n = 4 \to \exists r \in P n = 2 + 1 + r$
102	85 90 101	rspcedvd	$⊢ n = 4 \to \exists q \in P \exists r \in P n = 2 + q + r$
103	79 84 102	rspcedvd	$⊢ n = 4 \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
104	73 103	syl	$⊢ n \in \{4\} \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
105	72 104	sylbi	$⊢ n \in (3 + 1 ..^5) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
106	60 105	jaoi	$⊢ (n \in \{3\} \lor n \in (3 + 1 ..^5)) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
107	30 106	sylbi	$⊢ n \in (\{3\} \cup (3 + 1 ..^5)) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
108		elsni	$⊢ n \in \{5\} \to n = 5$
109		3prm	$⊢ 3 \in ℙ$
110	109	olci	$⊢ (3 \in \{1\} \lor 3 \in ℙ)$
111		elun	$⊢ 3 \in (\{1\} \cup ℙ) \leftrightarrow (3 \in \{1\} \lor 3 \in ℙ)$
112	110 111	mpbir	$⊢ 3 \in (\{1\} \cup ℙ)$
113	112 1	eleqtrri	$⊢ 3 \in P$
114	113	a1i	$⊢ n = 5 \to 3 \in P$
115		oveq1	$⊢ p = 3 \to p + q = 3 + q$
116	115	oveq1d	$⊢ p = 3 \to p + q + r = 3 + q + r$
117	116	eqeq2d	$⊢ p = 3 \to (n = p + q + r \leftrightarrow n = 3 + q + r)$
118	117	2rexbidv	$⊢ p = 3 \to (\exists q \in P \exists r \in P n = p + q + r \leftrightarrow \exists q \in P \exists r \in P n = 3 + q + r)$
119	118	adantl	$⊢ (n = 5 \land p = 3) \to (\exists q \in P \exists r \in P n = p + q + r \leftrightarrow \exists q \in P \exists r \in P n = 3 + q + r)$
120	37	a1i	$⊢ n = 5 \to 1 \in P$
121		oveq2	$⊢ q = 1 \to 3 + q = 3 + 1$
122	121	oveq1d	$⊢ q = 1 \to 3 + q + r = 3 + 1 + r$
123	122	eqeq2d	$⊢ q = 1 \to (n = 3 + q + r \leftrightarrow n = 3 + 1 + r)$
124	123	rexbidv	$⊢ q = 1 \to (\exists r \in P n = 3 + q + r \leftrightarrow \exists r \in P n = 3 + 1 + r)$
125	124	adantl	$⊢ (n = 5 \land q = 1) \to (\exists r \in P n = 3 + q + r \leftrightarrow \exists r \in P n = 3 + 1 + r)$
126		simpl	$⊢ (n = 5 \land r = 1) \to n = 5$
127	92	oveq1i	$⊢ 4 + 1 = 3 + 1 + 1$
128	62 127	eqtri	$⊢ 5 = 3 + 1 + 1$
129		oveq2	$⊢ r = 1 \to 3 + 1 + r = 3 + 1 + 1$
130	128 129	eqtr4id	$⊢ r = 1 \to 5 = 3 + 1 + r$
131	130	adantl	$⊢ (n = 5 \land r = 1) \to 5 = 3 + 1 + r$
132	126 131	eqtrd	$⊢ (n = 5 \land r = 1) \to n = 3 + 1 + r$
133	120 132	rspcedeqvd	$⊢ n = 5 \to \exists r \in P n = 3 + 1 + r$
134	120 125 133	rspcedvd	$⊢ n = 5 \to \exists q \in P \exists r \in P n = 3 + q + r$
135	114 119 134	rspcedvd	$⊢ n = 5 \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
136	108 135	syl	$⊢ n \in \{5\} \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
137	107 136	jaoi	$⊢ (n \in (\{3\} \cup (3 + 1 ..^5)) \lor n \in \{5\}) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
138	29 137	sylbi	$⊢ n \in ((\{3\} \cup (3 + 1 ..^5)) \cup \{5\}) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
139	138	a1d	$⊢ n \in ((\{3\} \cup (3 + 1 ..^5)) \cup \{5\}) \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
140	28 139	sylbi	$⊢ n \in (3 \dots 6 - 1) \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
141		sbgoldbm	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r$
142		rspa	$⊢ (\forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \land n \in ℤ_{\geq 6}) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r$
143		ssun2	$⊢ ℙ \subseteq \{1\} \cup ℙ$
144	143 1	sseqtrri	$⊢ ℙ \subseteq P$
145		rexss	$⊢ ℙ \subseteq P \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \leftrightarrow \exists p \in P (p \in ℙ \land \exists q \in ℙ \exists r \in ℙ n = p + q + r))$
146	144 145	ax-mp	$⊢ \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \leftrightarrow \exists p \in P (p \in ℙ \land \exists q \in ℙ \exists r \in ℙ n = p + q + r)$
147		rexss	$⊢ ℙ \subseteq P \to (\exists q \in ℙ \exists r \in ℙ n = p + q + r \leftrightarrow \exists q \in P (q \in ℙ \land \exists r \in ℙ n = p + q + r))$
148	144 147	ax-mp	$⊢ \exists q \in ℙ \exists r \in ℙ n = p + q + r \leftrightarrow \exists q \in P (q \in ℙ \land \exists r \in ℙ n = p + q + r)$
149		rexss	$⊢ ℙ \subseteq P \to (\exists r \in ℙ n = p + q + r \leftrightarrow \exists r \in P (r \in ℙ \land n = p + q + r))$
150	144 149	ax-mp	$⊢ \exists r \in ℙ n = p + q + r \leftrightarrow \exists r \in P (r \in ℙ \land n = p + q + r)$
151		simpr	$⊢ (r \in ℙ \land n = p + q + r) \to n = p + q + r$
152	151	reximi	$⊢ \exists r \in P (r \in ℙ \land n = p + q + r) \to \exists r \in P n = p + q + r$
153	150 152	sylbi	$⊢ \exists r \in ℙ n = p + q + r \to \exists r \in P n = p + q + r$
154	153	adantl	$⊢ (q \in ℙ \land \exists r \in ℙ n = p + q + r) \to \exists r \in P n = p + q + r$
155	154	reximi	$⊢ \exists q \in P (q \in ℙ \land \exists r \in ℙ n = p + q + r) \to \exists q \in P \exists r \in P n = p + q + r$
156	148 155	sylbi	$⊢ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \exists q \in P \exists r \in P n = p + q + r$
157	156	adantl	$⊢ (p \in ℙ \land \exists q \in ℙ \exists r \in ℙ n = p + q + r) \to \exists q \in P \exists r \in P n = p + q + r$
158	157	reximi	$⊢ \exists p \in P (p \in ℙ \land \exists q \in ℙ \exists r \in ℙ n = p + q + r) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
159	146 158	sylbi	$⊢ \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
160	142 159	syl	$⊢ (\forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \land n \in ℤ_{\geq 6}) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r$
161	160	ex	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to (n \in ℤ_{\geq 6} \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
162	141 161	syl	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to (n \in ℤ_{\geq 6} \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
163	162	com12	$⊢ n \in ℤ_{\geq 6} \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
164	140 163	jaoi	$⊢ (n \in (3 \dots 6 - 1) \lor n \in ℤ_{\geq 6}) \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
165	15 164	sylbi	$⊢ n \in ((3 \dots 6 - 1) \cup ℤ_{\geq 6}) \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
166	165	com12	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to (n \in ((3 \dots 6 - 1) \cup ℤ_{\geq 6}) \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
167	14 166	biimtrid	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to (n \in ℤ_{\geq 3} \to \exists p \in P \exists q \in P \exists r \in P n = p + q + r)$
168	2 167	ralrimi	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to \forall n \in ℤ_{\geq 3} \exists p \in P \exists q \in P \exists r \in P n = p + q + r$

Metamath Proof Explorer

Theorem sbgoldbo

Proof