sbgoldbst

Description: If the strong binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020)

		Ref	Expression
	Assertion	sbgoldbst	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to \forall m \in Odd (7 < m \to m \in GoldbachOdd)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (m \in Odd \land 7 < m) \to m \in Odd$
2		3odd	$⊢ 3 \in Odd$
3	1 2	jctir	$⊢ (m \in Odd \land 7 < m) \to (m \in Odd \land 3 \in Odd)$
4		omoeALTV	$⊢ (m \in Odd \land 3 \in Odd) \to m - 3 \in Even$
5		breq2	$⊢ n = m - 3 \to (4 < n \leftrightarrow 4 < m - 3)$
6		eleq1	$⊢ n = m - 3 \to (n \in GoldbachEven \leftrightarrow m - 3 \in GoldbachEven)$
7	5 6	imbi12d	$⊢ n = m - 3 \to ((4 < n \to n \in GoldbachEven) \leftrightarrow (4 < m - 3 \to m - 3 \in GoldbachEven))$
8	7	rspcv	$⊢ m - 3 \in Even \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to (4 < m - 3 \to m - 3 \in GoldbachEven))$
9	3 4 8	3syl	$⊢ (m \in Odd \land 7 < m) \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to (4 < m - 3 \to m - 3 \in GoldbachEven))$
10		4p3e7	$⊢ 4 + 3 = 7$
11	10	breq1i	$⊢ 4 + 3 < m \leftrightarrow 7 < m$
12		4re	$⊢ 4 \in ℝ$
13	12	a1i	$⊢ m \in Odd \to 4 \in ℝ$
14		3re	$⊢ 3 \in ℝ$
15	14	a1i	$⊢ m \in Odd \to 3 \in ℝ$
16		oddz	$⊢ m \in Odd \to m \in ℤ$
17	16	zred	$⊢ m \in Odd \to m \in ℝ$
18	13 15 17	ltaddsubd	$⊢ m \in Odd \to (4 + 3 < m \leftrightarrow 4 < m - 3)$
19	18	biimpd	$⊢ m \in Odd \to (4 + 3 < m \to 4 < m - 3)$
20	11 19	syl5bir	$⊢ m \in Odd \to (7 < m \to 4 < m - 3)$
21	20	imp	$⊢ (m \in Odd \land 7 < m) \to 4 < m - 3$
22		pm2.27	$⊢ 4 < m - 3 \to ((4 < m - 3 \to m - 3 \in GoldbachEven) \to m - 3 \in GoldbachEven)$
23	21 22	syl	$⊢ (m \in Odd \land 7 < m) \to ((4 < m - 3 \to m - 3 \in GoldbachEven) \to m - 3 \in GoldbachEven)$
24		isgbe	$⊢ m - 3 \in GoldbachEven \leftrightarrow (m - 3 \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land m - 3 = p + q))$
25		3prm	$⊢ 3 \in ℙ$
26	25	a1i	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land m - 3 = p + q)) \to 3 \in ℙ$
27		eleq1	$⊢ r = 3 \to (r \in Odd \leftrightarrow 3 \in Odd)$
28	27	3anbi3d	$⊢ r = 3 \to ((p \in Odd \land q \in Odd \land r \in Odd) \leftrightarrow (p \in Odd \land q \in Odd \land 3 \in Odd))$
29		oveq2	$⊢ r = 3 \to p + q + r = p + q + 3$
30	29	eqeq2d	$⊢ r = 3 \to (m = p + q + r \leftrightarrow m = p + q + 3)$
31	28 30	anbi12d	$⊢ r = 3 \to (((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land 3 \in Odd) \land m = p + q + 3))$
32	31	adantl	$⊢ (((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land m - 3 = p + q)) \land r = 3) \to (((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land 3 \in Odd) \land m = p + q + 3))$
33		simp1	$⊢ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to p \in Odd$
34		simp2	$⊢ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to q \in Odd$
35	2	a1i	$⊢ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to 3 \in Odd$
36	33 34 35	3jca	$⊢ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to (p \in Odd \land q \in Odd \land 3 \in Odd)$
37	36	adantl	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land m - 3 = p + q)) \to (p \in Odd \land q \in Odd \land 3 \in Odd)$
38	16	zcnd	$⊢ m \in Odd \to m \in ℂ$
39	38	ad3antrrr	$⊢ (((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \to m \in ℂ$
40		3cn	$⊢ 3 \in ℂ$
41	40	a1i	$⊢ (((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \to 3 \in ℂ$
42		prmz	$⊢ p \in ℙ \to p \in ℤ$
43		prmz	$⊢ q \in ℙ \to q \in ℤ$
44		zaddcl	$⊢ (p \in ℤ \land q \in ℤ) \to p + q \in ℤ$
45	42 43 44	syl2an	$⊢ (p \in ℙ \land q \in ℙ) \to p + q \in ℤ$
46	45	zcnd	$⊢ (p \in ℙ \land q \in ℙ) \to p + q \in ℂ$
47	46	adantll	$⊢ (((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \to p + q \in ℂ$
48	39 41 47	subadd2d	$⊢ (((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \to (m - 3 = p + q \leftrightarrow p + q + 3 = m)$
49	48	biimpa	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land m - 3 = p + q) \to p + q + 3 = m$
50	49	eqcomd	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land m - 3 = p + q) \to m = p + q + 3$
51	50	3ad2antr3	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land m - 3 = p + q)) \to m = p + q + 3$
52	37 51	jca	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land m - 3 = p + q)) \to ((p \in Odd \land q \in Odd \land 3 \in Odd) \land m = p + q + 3)$
53	26 32 52	rspcedvd	$⊢ ((((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \land (p \in Odd \land q \in Odd \land m - 3 = p + q)) \to \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r)$
54	53	ex	$⊢ (((m \in Odd \land 7 < m) \land p \in ℙ) \land q \in ℙ) \to ((p \in Odd \land q \in Odd \land m - 3 = p + q) \to \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r))$
55	54	reximdva	$⊢ ((m \in Odd \land 7 < m) \land p \in ℙ) \to (\exists q \in ℙ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r))$
56	55	reximdva	$⊢ (m \in Odd \land 7 < m) \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r))$
57	56 1	jctild	$⊢ (m \in Odd \land 7 < m) \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to (m \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r)))$
58		isgbo	$⊢ m \in GoldbachOdd \leftrightarrow (m \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land m = p + q + r))$
59	57 58	syl6ibr	$⊢ (m \in Odd \land 7 < m) \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land m - 3 = p + q) \to m \in GoldbachOdd)$
60	59	adantld	$⊢ (m \in Odd \land 7 < m) \to ((m - 3 \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land m - 3 = p + q)) \to m \in GoldbachOdd)$
61	24 60	syl5bi	$⊢ (m \in Odd \land 7 < m) \to (m - 3 \in GoldbachEven \to m \in GoldbachOdd)$
62	9 23 61	3syld	$⊢ (m \in Odd \land 7 < m) \to (\forall n \in Even (4 < n \to n \in GoldbachEven) \to m \in GoldbachOdd)$
63	62	com12	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to ((m \in Odd \land 7 < m) \to m \in GoldbachOdd)$
64	63	expd	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to (m \in Odd \to (7 < m \to m \in GoldbachOdd))$
65	64	ralrimiv	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to \forall m \in Odd (7 < m \to m \in GoldbachOdd)$

Metamath Proof Explorer

Theorem sbgoldbst

Proof