stgoldbwt

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

		Ref	Expression
	Assertion	stgoldbwt	$⊢ \forall n \in Odd (7 < n \to n \in GoldbachOdd) \to \forall n \in Odd (5 < n \to n \in GoldbachOddW)$

Proof

Step	Hyp	Ref	Expression
1		pm3.35	$⊢ (7 < n \land (7 < n \to n \in GoldbachOdd)) \to n \in GoldbachOdd$
2		gbogbow	$⊢ n \in GoldbachOdd \to n \in GoldbachOddW$
3	2	a1d	$⊢ n \in GoldbachOdd \to (5 < n \to n \in GoldbachOddW)$
4	1 3	syl	$⊢ (7 < n \land (7 < n \to n \in GoldbachOdd)) \to (5 < n \to n \in GoldbachOddW)$
5	4	ex	$⊢ 7 < n \to ((7 < n \to n \in GoldbachOdd) \to (5 < n \to n \in GoldbachOddW))$
6	5	a1d	$⊢ 7 < n \to (n \in Odd \to ((7 < n \to n \in GoldbachOdd) \to (5 < n \to n \in GoldbachOddW)))$
7		oddz	$⊢ n \in Odd \to n \in ℤ$
8	7	zred	$⊢ n \in Odd \to n \in ℝ$
9		7re	$⊢ 7 \in ℝ$
10	9	a1i	$⊢ n \in Odd \to 7 \in ℝ$
11	8 10	lenltd	$⊢ n \in Odd \to (n \leq 7 \leftrightarrow \neg 7 < n)$
12	8 10	leloed	$⊢ n \in Odd \to (n \leq 7 \leftrightarrow (n < 7 \lor n = 7))$
13	7	adantr	$⊢ (n \in Odd \land 5 < n) \to n \in ℤ$
14		6nn	$⊢ 6 \in ℕ$
15	14	nnzi	$⊢ 6 \in ℤ$
16	13 15	jctir	$⊢ (n \in Odd \land 5 < n) \to (n \in ℤ \land 6 \in ℤ)$
17	16	adantl	$⊢ (n < 7 \land (n \in Odd \land 5 < n)) \to (n \in ℤ \land 6 \in ℤ)$
18		df-7	$⊢ 7 = 6 + 1$
19	18	breq2i	$⊢ n < 7 \leftrightarrow n < 6 + 1$
20	19	biimpi	$⊢ n < 7 \to n < 6 + 1$
21		df-6	$⊢ 6 = 5 + 1$
22		5nn	$⊢ 5 \in ℕ$
23	22	nnzi	$⊢ 5 \in ℤ$
24		zltp1le	$⊢ (5 \in ℤ \land n \in ℤ) \to (5 < n \leftrightarrow 5 + 1 \leq n)$
25	23 7 24	sylancr	$⊢ n \in Odd \to (5 < n \leftrightarrow 5 + 1 \leq n)$
26	25	biimpa	$⊢ (n \in Odd \land 5 < n) \to 5 + 1 \leq n$
27	21 26	eqbrtrid	$⊢ (n \in Odd \land 5 < n) \to 6 \leq n$
28	20 27	anim12ci	$⊢ (n < 7 \land (n \in Odd \land 5 < n)) \to (6 \leq n \land n < 6 + 1)$
29		zgeltp1eq	$⊢ (n \in ℤ \land 6 \in ℤ) \to ((6 \leq n \land n < 6 + 1) \to n = 6)$
30	17 28 29	sylc	$⊢ (n < 7 \land (n \in Odd \land 5 < n)) \to n = 6$
31	30	orcd	$⊢ (n < 7 \land (n \in Odd \land 5 < n)) \to (n = 6 \lor n = 7)$
32	31	ex	$⊢ n < 7 \to ((n \in Odd \land 5 < n) \to (n = 6 \lor n = 7))$
33		olc	$⊢ n = 7 \to (n = 6 \lor n = 7)$
34	33	a1d	$⊢ n = 7 \to ((n \in Odd \land 5 < n) \to (n = 6 \lor n = 7))$
35	32 34	jaoi	$⊢ (n < 7 \lor n = 7) \to ((n \in Odd \land 5 < n) \to (n = 6 \lor n = 7))$
36	35	expd	$⊢ (n < 7 \lor n = 7) \to (n \in Odd \to (5 < n \to (n = 6 \lor n = 7)))$
37	36	com12	$⊢ n \in Odd \to ((n < 7 \lor n = 7) \to (5 < n \to (n = 6 \lor n = 7)))$
38	12 37	sylbid	$⊢ n \in Odd \to (n \leq 7 \to (5 < n \to (n = 6 \lor n = 7)))$
39		eleq1	$⊢ n = 6 \to (n \in Odd \leftrightarrow 6 \in Odd)$
40		6even	$⊢ 6 \in Even$
41		evennodd	$⊢ 6 \in Even \to \neg 6 \in Odd$
42	41	pm2.21d	$⊢ 6 \in Even \to (6 \in Odd \to n \in GoldbachOddW)$
43	40 42	mp1i	$⊢ n = 6 \to (6 \in Odd \to n \in GoldbachOddW)$
44	39 43	sylbid	$⊢ n = 6 \to (n \in Odd \to n \in GoldbachOddW)$
45		7gbow	$⊢ 7 \in GoldbachOddW$
46		eleq1	$⊢ n = 7 \to (n \in GoldbachOddW \leftrightarrow 7 \in GoldbachOddW)$
47	45 46	mpbiri	$⊢ n = 7 \to n \in GoldbachOddW$
48	47	a1d	$⊢ n = 7 \to (n \in Odd \to n \in GoldbachOddW)$
49	44 48	jaoi	$⊢ (n = 6 \lor n = 7) \to (n \in Odd \to n \in GoldbachOddW)$
50	49	com12	$⊢ n \in Odd \to ((n = 6 \lor n = 7) \to n \in GoldbachOddW)$
51	38 50	syl6d	$⊢ n \in Odd \to (n \leq 7 \to (5 < n \to n \in GoldbachOddW))$
52	11 51	sylbird	$⊢ n \in Odd \to (\neg 7 < n \to (5 < n \to n \in GoldbachOddW))$
53	52	com12	$⊢ \neg 7 < n \to (n \in Odd \to (5 < n \to n \in GoldbachOddW))$
54	53	a1dd	$⊢ \neg 7 < n \to (n \in Odd \to ((7 < n \to n \in GoldbachOdd) \to (5 < n \to n \in GoldbachOddW)))$
55	6 54	pm2.61i	$⊢ n \in Odd \to ((7 < n \to n \in GoldbachOdd) \to (5 < n \to n \in GoldbachOddW))$
56	55	ralimia	$⊢ \forall n \in Odd (7 < n \to n \in GoldbachOdd) \to \forall n \in Odd (5 < n \to n \in GoldbachOddW)$

Metamath Proof Explorer

Theorem stgoldbwt

Proof