mogoldbb

Description: If the modern version of the original formulation of the Goldbach conjecture is valid, the (weak) binary Goldbach conjecture also holds. (Contributed by AV, 26-Dec-2021)

		Ref	Expression
	Assertion	mogoldbb	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \forall n \in Even (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q)$

Proof

Step	Hyp	Ref	Expression
1		nfra1	$⊢ Ⅎ n \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r$
2		eqeq1	$⊢ n = m \to (n = p + q + r \leftrightarrow m = p + q + r)$
3	2	rexbidv	$⊢ n = m \to (\exists r \in ℙ n = p + q + r \leftrightarrow \exists r \in ℙ m = p + q + r)$
4	3	2rexbidv	$⊢ n = m \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \leftrightarrow \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ m = p + q + r)$
5	4	cbvralvw	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \leftrightarrow \forall m \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ m = p + q + r$
6		6nn	$⊢ 6 \in ℕ$
7	6	nnzi	$⊢ 6 \in ℤ$
8	7	a1i	$⊢ (n \in Even \land 2 < n) \to 6 \in ℤ$
9		evenz	$⊢ n \in Even \to n \in ℤ$
10		2z	$⊢ 2 \in ℤ$
11	10	a1i	$⊢ n \in Even \to 2 \in ℤ$
12	9 11	zaddcld	$⊢ n \in Even \to n + 2 \in ℤ$
13	12	adantr	$⊢ (n \in Even \land 2 < n) \to n + 2 \in ℤ$
14		4cn	$⊢ 4 \in ℂ$
15		2cn	$⊢ 2 \in ℂ$
16		4p2e6	$⊢ 4 + 2 = 6$
17	16	eqcomi	$⊢ 6 = 4 + 2$
18	14 15 17	mvrraddi	$⊢ 6 - 2 = 4$
19		2p2e4	$⊢ 2 + 2 = 4$
20		2evenALTV	$⊢ 2 \in Even$
21		evenltle	$⊢ (n \in Even \land 2 \in Even \land 2 < n) \to 2 + 2 \leq n$
22	20 21	mp3an2	$⊢ (n \in Even \land 2 < n) \to 2 + 2 \leq n$
23	19 22	eqbrtrrid	$⊢ (n \in Even \land 2 < n) \to 4 \leq n$
24	18 23	eqbrtrid	$⊢ (n \in Even \land 2 < n) \to 6 - 2 \leq n$
25		6re	$⊢ 6 \in ℝ$
26	25	a1i	$⊢ n \in Even \to 6 \in ℝ$
27		2re	$⊢ 2 \in ℝ$
28	27	a1i	$⊢ n \in Even \to 2 \in ℝ$
29	9	zred	$⊢ n \in Even \to n \in ℝ$
30	26 28 29	3jca	$⊢ n \in Even \to (6 \in ℝ \land 2 \in ℝ \land n \in ℝ)$
31	30	adantr	$⊢ (n \in Even \land 2 < n) \to (6 \in ℝ \land 2 \in ℝ \land n \in ℝ)$
32		lesubadd	$⊢ (6 \in ℝ \land 2 \in ℝ \land n \in ℝ) \to (6 - 2 \leq n \leftrightarrow 6 \leq n + 2)$
33	31 32	syl	$⊢ (n \in Even \land 2 < n) \to (6 - 2 \leq n \leftrightarrow 6 \leq n + 2)$
34	24 33	mpbid	$⊢ (n \in Even \land 2 < n) \to 6 \leq n + 2$
35		eluz2	$⊢ n + 2 \in ℤ_{\geq 6} \leftrightarrow (6 \in ℤ \land n + 2 \in ℤ \land 6 \leq n + 2)$
36	8 13 34 35	syl3anbrc	$⊢ (n \in Even \land 2 < n) \to n + 2 \in ℤ_{\geq 6}$
37		eqeq1	$⊢ m = n + 2 \to (m = p + q + r \leftrightarrow n + 2 = p + q + r)$
38	37	rexbidv	$⊢ m = n + 2 \to (\exists r \in ℙ m = p + q + r \leftrightarrow \exists r \in ℙ n + 2 = p + q + r)$
39	38	2rexbidv	$⊢ m = n + 2 \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ m = p + q + r \leftrightarrow \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r)$
40	39	rspcv	$⊢ n + 2 \in ℤ_{\geq 6} \to (\forall m \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ m = p + q + r \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r)$
41	36 40	syl	$⊢ (n \in Even \land 2 < n) \to (\forall m \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ m = p + q + r \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r)$
42	5 41	syl5bi	$⊢ (n \in Even \land 2 < n) \to (\forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r)$
43		nfv	$⊢ Ⅎ p (n \in Even \land 2 < n)$
44		nfre1	$⊢ Ⅎ p \exists p \in ℙ \exists q \in ℙ n = p + q$
45		nfv	$⊢ Ⅎ q ((n \in Even \land 2 < n) \land p \in ℙ)$
46		nfcv	$⊢ \underline{Ⅎ} q ℙ$
47		nfre1	$⊢ Ⅎ q \exists q \in ℙ n = p + q$
48	46 47	nfrex	$⊢ Ⅎ q \exists p \in ℙ \exists q \in ℙ n = p + q$
49		simplrl	$⊢ (((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \to p \in ℙ$
50		simplrr	$⊢ (((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \to q \in ℙ$
51		simpr	$⊢ (((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \to r \in ℙ$
52	49 50 51	3jca	$⊢ (((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \to (p \in ℙ \land q \in ℙ \land r \in ℙ)$
53	52	adantr	$⊢ ((((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \land n + 2 = p + q + r) \to (p \in ℙ \land q \in ℙ \land r \in ℙ)$
54		simp-4l	$⊢ ((((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \land n + 2 = p + q + r) \to n \in Even$
55		simpr	$⊢ ((((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \land n + 2 = p + q + r) \to n + 2 = p + q + r$
56		mogoldbblem	$⊢ ((p \in ℙ \land q \in ℙ \land r \in ℙ) \land n \in Even \land n + 2 = p + q + r) \to \exists y \in ℙ \exists x \in ℙ n = y + x$
57		oveq1	$⊢ p = y \to p + q = y + q$
58	57	eqeq2d	$⊢ p = y \to (n = p + q \leftrightarrow n = y + q)$
59		oveq2	$⊢ q = x \to y + q = y + x$
60	59	eqeq2d	$⊢ q = x \to (n = y + q \leftrightarrow n = y + x)$
61	58 60	cbvrex2vw	$⊢ \exists p \in ℙ \exists q \in ℙ n = p + q \leftrightarrow \exists y \in ℙ \exists x \in ℙ n = y + x$
62	56 61	sylibr	$⊢ ((p \in ℙ \land q \in ℙ \land r \in ℙ) \land n \in Even \land n + 2 = p + q + r) \to \exists p \in ℙ \exists q \in ℙ n = p + q$
63	53 54 55 62	syl3anc	$⊢ ((((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \land r \in ℙ) \land n + 2 = p + q + r) \to \exists p \in ℙ \exists q \in ℙ n = p + q$
64	63	rexlimdva2	$⊢ ((n \in Even \land 2 < n) \land (p \in ℙ \land q \in ℙ)) \to (\exists r \in ℙ n + 2 = p + q + r \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
65	64	expr	$⊢ ((n \in Even \land 2 < n) \land p \in ℙ) \to (q \in ℙ \to (\exists r \in ℙ n + 2 = p + q + r \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
66	45 48 65	rexlimd	$⊢ ((n \in Even \land 2 < n) \land p \in ℙ) \to (\exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
67	66	ex	$⊢ (n \in Even \land 2 < n) \to (p \in ℙ \to (\exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
68	43 44 67	rexlimd	$⊢ (n \in Even \land 2 < n) \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n + 2 = p + q + r \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
69	42 68	syldc	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to ((n \in Even \land 2 < n) \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
70	69	expd	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to (n \in Even \to (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q))$
71	1 70	ralrimi	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \forall n \in Even (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q)$

Metamath Proof Explorer

Theorem mogoldbb

Proof