wtgoldbnnsum4prm

Description: If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in Helfgott p. 4. (Contributed by AV, 25-Jul-2020)

		Ref	Expression
	Assertion	wtgoldbnnsum4prm	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \forall n \in ℤ_{\geq 2} \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		9nn	$⊢ 9 \in ℕ$
3	2	nnzi	$⊢ 9 \in ℤ$
4		2re	$⊢ 2 \in ℝ$
5		9re	$⊢ 9 \in ℝ$
6		2lt9	$⊢ 2 < 9$
7	4 5 6	ltleii	$⊢ 2 \leq 9$
8		eluz2	$⊢ 9 \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land 9 \in ℤ \land 2 \leq 9)$
9	1 3 7 8	mpbir3an	$⊢ 9 \in ℤ_{\geq 2}$
10		fzouzsplit	$⊢ 9 \in ℤ_{\geq 2} \to ℤ_{\geq 2} = (2 ..^9) \cup ℤ_{\geq 9}$
11	10	eleq2d	$⊢ 9 \in ℤ_{\geq 2} \to (n \in ℤ_{\geq 2} \leftrightarrow n \in ((2 ..^9) \cup ℤ_{\geq 9}))$
12	9 11	ax-mp	$⊢ n \in ℤ_{\geq 2} \leftrightarrow n \in ((2 ..^9) \cup ℤ_{\geq 9})$
13		elun	$⊢ n \in ((2 ..^9) \cup ℤ_{\geq 9}) \leftrightarrow (n \in (2 ..^9) \lor n \in ℤ_{\geq 9})$
14	12 13	bitri	$⊢ n \in ℤ_{\geq 2} \leftrightarrow (n \in (2 ..^9) \lor n \in ℤ_{\geq 9})$
15		elfzo2	$⊢ n \in (2 ..^9) \leftrightarrow (n \in ℤ_{\geq 2} \land 9 \in ℤ \land n < 9)$
16		simp1	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ \land n < 9) \to n \in ℤ_{\geq 2}$
17		df-9	$⊢ 9 = 8 + 1$
18	17	breq2i	$⊢ n < 9 \leftrightarrow n < 8 + 1$
19		eluz2nn	$⊢ n \in ℤ_{\geq 2} \to n \in ℕ$
20		8nn	$⊢ 8 \in ℕ$
21	19 20	jctir	$⊢ n \in ℤ_{\geq 2} \to (n \in ℕ \land 8 \in ℕ)$
22	21	adantr	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ) \to (n \in ℕ \land 8 \in ℕ)$
23		nnleltp1	$⊢ (n \in ℕ \land 8 \in ℕ) \to (n \leq 8 \leftrightarrow n < 8 + 1)$
24	22 23	syl	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ) \to (n \leq 8 \leftrightarrow n < 8 + 1)$
25	24	biimprd	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ) \to (n < 8 + 1 \to n \leq 8)$
26	18 25	biimtrid	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ) \to (n < 9 \to n \leq 8)$
27	26	3impia	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ \land n < 9) \to n \leq 8$
28	16 27	jca	$⊢ (n \in ℤ_{\geq 2} \land 9 \in ℤ \land n < 9) \to (n \in ℤ_{\geq 2} \land n \leq 8)$
29	15 28	sylbi	$⊢ n \in (2 ..^9) \to (n \in ℤ_{\geq 2} \land n \leq 8)$
30		nnsum4primesle9	$⊢ (n \in ℤ_{\geq 2} \land n \leq 8) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$
31	29 30	syl	$⊢ n \in (2 ..^9) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$
32	31	a1d	$⊢ n \in (2 ..^9) \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)))$
33		4nn	$⊢ 4 \in ℕ$
34	33	a1i	$⊢ ((n \in ℤ_{\geq 9} \land n \in Even) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to 4 \in ℕ$
35		oveq2	$⊢ d = 4 \to (1 \dots d) = (1 \dots 4)$
36	35	oveq2d	$⊢ d = 4 \to ℙ^{(1 \dots d)} = ℙ^{(1 \dots 4)}$
37		breq1	$⊢ d = 4 \to (d \leq 4 \leftrightarrow 4 \leq 4)$
38	35	sumeq1d	$⊢ d = 4 \to \sum_{k = 1}^{d} f (k) = \sum_{k = 1}^{4} f (k)$
39	38	eqeq2d	$⊢ d = 4 \to (n = \sum_{k = 1}^{d} f (k) \leftrightarrow n = \sum_{k = 1}^{4} f (k))$
40	37 39	anbi12d	$⊢ d = 4 \to ((d \leq 4 \land n = \sum_{k = 1}^{d} f (k)) \leftrightarrow (4 \leq 4 \land n = \sum_{k = 1}^{4} f (k)))$
41	36 40	rexeqbidv	$⊢ d = 4 \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{(1 \dots 4)}) (4 \leq 4 \land n = \sum_{k = 1}^{4} f (k)))$
42	41	adantl	$⊢ (((n \in ℤ_{\geq 9} \land n \in Even) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \land d = 4) \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{(1 \dots 4)}) (4 \leq 4 \land n = \sum_{k = 1}^{4} f (k)))$
43		4re	$⊢ 4 \in ℝ$
44	43	leidi	$⊢ 4 \leq 4$
45	44	a1i	$⊢ ((n \in ℤ_{\geq 9} \land n \in Even) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to 4 \leq 4$
46		nnsum4primeseven	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((n \in ℤ_{\geq 9} \land n \in Even) \to \exists f \in (ℙ^{(1 \dots 4)}) n = \sum_{k = 1}^{4} f (k))$
47	46	impcom	$⊢ ((n \in ℤ_{\geq 9} \land n \in Even) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to \exists f \in (ℙ^{(1 \dots 4)}) n = \sum_{k = 1}^{4} f (k)$
48		r19.42v	$⊢ \exists f \in (ℙ^{(1 \dots 4)}) (4 \leq 4 \land n = \sum_{k = 1}^{4} f (k)) \leftrightarrow (4 \leq 4 \land \exists f \in (ℙ^{(1 \dots 4)}) n = \sum_{k = 1}^{4} f (k))$
49	45 47 48	sylanbrc	$⊢ ((n \in ℤ_{\geq 9} \land n \in Even) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to \exists f \in (ℙ^{(1 \dots 4)}) (4 \leq 4 \land n = \sum_{k = 1}^{4} f (k))$
50	34 42 49	rspcedvd	$⊢ ((n \in ℤ_{\geq 9} \land n \in Even) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$
51	50	ex	$⊢ (n \in ℤ_{\geq 9} \land n \in Even) \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)))$
52		3nn	$⊢ 3 \in ℕ$
53	52	a1i	$⊢ ((n \in ℤ_{\geq 9} \land n \in Odd) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to 3 \in ℕ$
54		oveq2	$⊢ d = 3 \to (1 \dots d) = (1 \dots 3)$
55	54	oveq2d	$⊢ d = 3 \to ℙ^{(1 \dots d)} = ℙ^{(1 \dots 3)}$
56		breq1	$⊢ d = 3 \to (d \leq 4 \leftrightarrow 3 \leq 4)$
57	54	sumeq1d	$⊢ d = 3 \to \sum_{k = 1}^{d} f (k) = \sum_{k = 1}^{3} f (k)$
58	57	eqeq2d	$⊢ d = 3 \to (n = \sum_{k = 1}^{d} f (k) \leftrightarrow n = \sum_{k = 1}^{3} f (k))$
59	56 58	anbi12d	$⊢ d = 3 \to ((d \leq 4 \land n = \sum_{k = 1}^{d} f (k)) \leftrightarrow (3 \leq 4 \land n = \sum_{k = 1}^{3} f (k)))$
60	55 59	rexeqbidv	$⊢ d = 3 \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{(1 \dots 3)}) (3 \leq 4 \land n = \sum_{k = 1}^{3} f (k)))$
61	60	adantl	$⊢ (((n \in ℤ_{\geq 9} \land n \in Odd) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \land d = 3) \to (\exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)) \leftrightarrow \exists f \in (ℙ^{(1 \dots 3)}) (3 \leq 4 \land n = \sum_{k = 1}^{3} f (k)))$
62		3re	$⊢ 3 \in ℝ$
63		3lt4	$⊢ 3 < 4$
64	62 43 63	ltleii	$⊢ 3 \leq 4$
65	64	a1i	$⊢ ((n \in ℤ_{\geq 9} \land n \in Odd) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to 3 \leq 4$
66		6nn	$⊢ 6 \in ℕ$
67	66	nnzi	$⊢ 6 \in ℤ$
68		6re	$⊢ 6 \in ℝ$
69		6lt9	$⊢ 6 < 9$
70	68 5 69	ltleii	$⊢ 6 \leq 9$
71		eluzuzle	$⊢ (6 \in ℤ \land 6 \leq 9) \to (n \in ℤ_{\geq 9} \to n \in ℤ_{\geq 6})$
72	67 70 71	mp2an	$⊢ n \in ℤ_{\geq 9} \to n \in ℤ_{\geq 6}$
73	72	anim1i	$⊢ (n \in ℤ_{\geq 9} \land n \in Odd) \to (n \in ℤ_{\geq 6} \land n \in Odd)$
74		nnsum4primesodd	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to ((n \in ℤ_{\geq 6} \land n \in Odd) \to \exists f \in (ℙ^{(1 \dots 3)}) n = \sum_{k = 1}^{3} f (k))$
75	73 74	mpan9	$⊢ ((n \in ℤ_{\geq 9} \land n \in Odd) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to \exists f \in (ℙ^{(1 \dots 3)}) n = \sum_{k = 1}^{3} f (k)$
76		r19.42v	$⊢ \exists f \in (ℙ^{(1 \dots 3)}) (3 \leq 4 \land n = \sum_{k = 1}^{3} f (k)) \leftrightarrow (3 \leq 4 \land \exists f \in (ℙ^{(1 \dots 3)}) n = \sum_{k = 1}^{3} f (k))$
77	65 75 76	sylanbrc	$⊢ ((n \in ℤ_{\geq 9} \land n \in Odd) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to \exists f \in (ℙ^{(1 \dots 3)}) (3 \leq 4 \land n = \sum_{k = 1}^{3} f (k))$
78	53 61 77	rspcedvd	$⊢ ((n \in ℤ_{\geq 9} \land n \in Odd) \land \forall m \in Odd (5 < m \to m \in GoldbachOddW)) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$
79	78	ex	$⊢ (n \in ℤ_{\geq 9} \land n \in Odd) \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)))$
80		eluzelz	$⊢ n \in ℤ_{\geq 9} \to n \in ℤ$
81		zeoALTV	$⊢ n \in ℤ \to (n \in Even \lor n \in Odd)$
82	80 81	syl	$⊢ n \in ℤ_{\geq 9} \to (n \in Even \lor n \in Odd)$
83	51 79 82	mpjaodan	$⊢ n \in ℤ_{\geq 9} \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)))$
84	32 83	jaoi	$⊢ (n \in (2 ..^9) \lor n \in ℤ_{\geq 9}) \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)))$
85	14 84	sylbi	$⊢ n \in ℤ_{\geq 2} \to (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k)))$
86	85	impcom	$⊢ (\forall m \in Odd (5 < m \to m \in GoldbachOddW) \land n \in ℤ_{\geq 2}) \to \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$
87	86	ralrimiva	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \forall n \in ℤ_{\geq 2} \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$

Metamath Proof Explorer

Theorem wtgoldbnnsum4prm

Proof