tgoldbachgt

Description: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of Helfgott p. 70 , expressed using the set G of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021)

	Ref	Expression
Hypotheses	tgoldbachgt.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
	tgoldbachgt.g	$⊢ G = \{z \in O \| \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r)\}$
Assertion	tgoldbachgt	$⊢ \exists m \in ℕ (m \leq 10^{27} \land \forall n \in O (m < n \to n \in G))$

Proof

Step	Hyp	Ref	Expression
1		tgoldbachgt.o	$⊢ O = \{z \in ℤ \| \neg 2 ∥ z\}$
2		tgoldbachgt.g	$⊢ G = \{z \in O \| \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r)\}$
3		10nn	$⊢ 10 \in ℕ$
4		2nn0	$⊢ 2 \in ℕ_{0}$
5		7nn0	$⊢ 7 \in ℕ_{0}$
6	4 5	deccl	$⊢ 27 \in ℕ_{0}$
7		nnexpcl	$⊢ (10 \in ℕ \land 27 \in ℕ_{0}) \to 10^{27} \in ℕ$
8	3 6 7	mp2an	$⊢ 10^{27} \in ℕ$
9	8	nnrei	$⊢ 10^{27} \in ℝ$
10	9	leidi	$⊢ 10^{27} \leq 10^{27}$
11		simpl	$⊢ (n \in O \land 10^{27} < n) \to n \in O$
12		inss2	$⊢ O \cap ℙ \subseteq ℙ$
13		prmssnn	$⊢ ℙ \subseteq ℕ$
14	12 13	sstri	$⊢ O \cap ℙ \subseteq ℕ$
15	14	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to O \cap ℙ \subseteq ℕ$
16	1	eleq2i	$⊢ n \in O \leftrightarrow n \in \{z \in ℤ \| \neg 2 ∥ z\}$
17		elrabi	$⊢ n \in \{z \in ℤ \| \neg 2 ∥ z\} \to n \in ℤ$
18	16 17	sylbi	$⊢ n \in O \to n \in ℤ$
19	18	ad2antrr	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to n \in ℤ$
20		3nn0	$⊢ 3 \in ℕ_{0}$
21	20	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 3 \in ℕ_{0}$
22		simpr	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c \in ((O \cap ℙ) repr (3) n)$
23	15 19 21 22	reprf	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c : (0 ..^3) ⟶ O \cap ℙ$
24		c0ex	$⊢ 0 \in V$
25	24	tpid1	$⊢ 0 \in \{0, 1, 2\}$
26		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
27	25 26	eleqtrri	$⊢ 0 \in (0 ..^3)$
28	27	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 0 \in (0 ..^3)$
29	23 28	ffvelcdmd	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (0) \in (O \cap ℙ)$
30	29	elin2d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (0) \in ℙ$
31		1eltp012	$⊢ 1 \in \{0, 1, 2\}$
32	31 26	eleqtrri	$⊢ 1 \in (0 ..^3)$
33	32	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 1 \in (0 ..^3)$
34	23 33	ffvelcdmd	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (1) \in (O \cap ℙ)$
35	34	elin2d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (1) \in ℙ$
36		2ex	$⊢ 2 \in V$
37	36	tpid3	$⊢ 2 \in \{0, 1, 2\}$
38	37 26	eleqtrri	$⊢ 2 \in (0 ..^3)$
39	38	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 2 \in (0 ..^3)$
40	23 39	ffvelcdmd	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (2) \in (O \cap ℙ)$
41	40	elin2d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (2) \in ℙ$
42	29	elin1d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (0) \in O$
43	34	elin1d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (1) \in O$
44	40	elin1d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (2) \in O$
45	42 43 44	3jca	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to (c (0) \in O \land c (1) \in O \land c (2) \in O)$
46	26	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to (0 ..^3) = \{0, 1, 2\}$
47	46	sumeq1d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to \sum_{i \in (0 ..^3)} c (i) = \sum_{i \in \{0, 1, 2\}} c (i)$
48	15 19 21 22	reprsum	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to \sum_{i \in (0 ..^3)} c (i) = n$
49		fveq2	$⊢ i = 0 \to c (i) = c (0)$
50		fveq2	$⊢ i = 1 \to c (i) = c (1)$
51		fveq2	$⊢ i = 2 \to c (i) = c (2)$
52	14 29	sselid	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (0) \in ℕ$
53	52	nncnd	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (0) \in ℂ$
54	14 34	sselid	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (1) \in ℕ$
55	54	nncnd	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (1) \in ℂ$
56	14 40	sselid	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (2) \in ℕ$
57	56	nncnd	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to c (2) \in ℂ$
58	53 55 57	3jca	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to (c (0) \in ℂ \land c (1) \in ℂ \land c (2) \in ℂ)$
59	24	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 0 \in V$
60		1ex	$⊢ 1 \in V$
61	60	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 1 \in V$
62	36	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 2 \in V$
63	59 61 62	3jca	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to (0 \in V \land 1 \in V \land 2 \in V)$
64		0ne1	$⊢ 0 \neq 1$
65	64	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 0 \neq 1$
66		0ne2	$⊢ 0 \neq 2$
67	66	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 0 \neq 2$
68		1ne2	$⊢ 1 \neq 2$
69	68	a1i	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to 1 \neq 2$
70	49 50 51 58 63 65 67 69	sumtp	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to \sum_{i \in \{0, 1, 2\}} c (i) = c (0) + c (1) + c (2)$
71	47 48 70	3eqtr3d	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to n = c (0) + c (1) + c (2)$
72	45 71	jca	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to ((c (0) \in O \land c (1) \in O \land c (2) \in O) \land n = c (0) + c (1) + c (2))$
73		eleq1	$⊢ p = c (0) \to (p \in O \leftrightarrow c (0) \in O)$
74	73	3anbi1d	$⊢ p = c (0) \to ((p \in O \land q \in O \land r \in O) \leftrightarrow (c (0) \in O \land q \in O \land r \in O))$
75		oveq1	$⊢ p = c (0) \to p + q = c (0) + q$
76	75	oveq1d	$⊢ p = c (0) \to p + q + r = c (0) + q + r$
77	76	eqeq2d	$⊢ p = c (0) \to (n = p + q + r \leftrightarrow n = c (0) + q + r)$
78	74 77	anbi12d	$⊢ p = c (0) \to (((p \in O \land q \in O \land r \in O) \land n = p + q + r) \leftrightarrow ((c (0) \in O \land q \in O \land r \in O) \land n = c (0) + q + r))$
79		eleq1	$⊢ q = c (1) \to (q \in O \leftrightarrow c (1) \in O)$
80	79	3anbi2d	$⊢ q = c (1) \to ((c (0) \in O \land q \in O \land r \in O) \leftrightarrow (c (0) \in O \land c (1) \in O \land r \in O))$
81		oveq2	$⊢ q = c (1) \to c (0) + q = c (0) + c (1)$
82	81	oveq1d	$⊢ q = c (1) \to c (0) + q + r = c (0) + c (1) + r$
83	82	eqeq2d	$⊢ q = c (1) \to (n = c (0) + q + r \leftrightarrow n = c (0) + c (1) + r)$
84	80 83	anbi12d	$⊢ q = c (1) \to (((c (0) \in O \land q \in O \land r \in O) \land n = c (0) + q + r) \leftrightarrow ((c (0) \in O \land c (1) \in O \land r \in O) \land n = c (0) + c (1) + r))$
85		eleq1	$⊢ r = c (2) \to (r \in O \leftrightarrow c (2) \in O)$
86	85	3anbi3d	$⊢ r = c (2) \to ((c (0) \in O \land c (1) \in O \land r \in O) \leftrightarrow (c (0) \in O \land c (1) \in O \land c (2) \in O))$
87		oveq2	$⊢ r = c (2) \to c (0) + c (1) + r = c (0) + c (1) + c (2)$
88	87	eqeq2d	$⊢ r = c (2) \to (n = c (0) + c (1) + r \leftrightarrow n = c (0) + c (1) + c (2))$
89	86 88	anbi12d	$⊢ r = c (2) \to (((c (0) \in O \land c (1) \in O \land r \in O) \land n = c (0) + c (1) + r) \leftrightarrow ((c (0) \in O \land c (1) \in O \land c (2) \in O) \land n = c (0) + c (1) + c (2)))$
90	78 84 89	rspc3ev	$⊢ ((c (0) \in ℙ \land c (1) \in ℙ \land c (2) \in ℙ) \land ((c (0) \in O \land c (1) \in O \land c (2) \in O) \land n = c (0) + c (1) + c (2))) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r)$
91	30 35 41 72 90	syl31anc	$⊢ ((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r)$
92	91	adantr	$⊢ (((n \in O \land 10^{27} < n) \land c \in ((O \cap ℙ) repr (3) n)) \land ⊤) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r)$
93	8	a1i	$⊢ (n \in O \land 10^{27} < n) \to 10^{27} \in ℕ$
94	93	nnred	$⊢ (n \in O \land 10^{27} < n) \to 10^{27} \in ℝ$
95	18	zred	$⊢ n \in O \to n \in ℝ$
96	95	adantr	$⊢ (n \in O \land 10^{27} < n) \to n \in ℝ$
97		simpr	$⊢ (n \in O \land 10^{27} < n) \to 10^{27} < n$
98	94 96 97	ltled	$⊢ (n \in O \land 10^{27} < n) \to 10^{27} \leq n$
99	1 11 98	tgoldbachgtd	$⊢ (n \in O \land 10^{27} < n) \to 0 < \|(O \cap ℙ) repr (3) n\|$
100		ovex	$⊢ (O \cap ℙ) repr (3) n \in V$
101		hashneq0	$⊢ (O \cap ℙ) repr (3) n \in V \to (0 < \|(O \cap ℙ) repr (3) n\| \leftrightarrow (O \cap ℙ) repr (3) n \neq \emptyset)$
102	100 101	ax-mp	$⊢ 0 < \|(O \cap ℙ) repr (3) n\| \leftrightarrow (O \cap ℙ) repr (3) n \neq \emptyset$
103	99 102	sylib	$⊢ (n \in O \land 10^{27} < n) \to (O \cap ℙ) repr (3) n \neq \emptyset$
104	103	neneqd	$⊢ (n \in O \land 10^{27} < n) \to \neg (O \cap ℙ) repr (3) n = \emptyset$
105		neq0	$⊢ \neg (O \cap ℙ) repr (3) n = \emptyset \leftrightarrow \exists c c \in ((O \cap ℙ) repr (3) n)$
106	104 105	sylib	$⊢ (n \in O \land 10^{27} < n) \to \exists c c \in ((O \cap ℙ) repr (3) n)$
107		tru	$⊢ ⊤$
108	106 107	jctil	$⊢ (n \in O \land 10^{27} < n) \to (⊤ \land \exists c c \in ((O \cap ℙ) repr (3) n))$
109		19.42v	$⊢ \exists c (⊤ \land c \in ((O \cap ℙ) repr (3) n)) \leftrightarrow (⊤ \land \exists c c \in ((O \cap ℙ) repr (3) n))$
110	108 109	sylibr	$⊢ (n \in O \land 10^{27} < n) \to \exists c (⊤ \land c \in ((O \cap ℙ) repr (3) n))$
111		exancom	$⊢ \exists c (⊤ \land c \in ((O \cap ℙ) repr (3) n)) \leftrightarrow \exists c (c \in ((O \cap ℙ) repr (3) n) \land ⊤)$
112	110 111	sylib	$⊢ (n \in O \land 10^{27} < n) \to \exists c (c \in ((O \cap ℙ) repr (3) n) \land ⊤)$
113		df-rex	$⊢ \exists c \in ((O \cap ℙ) repr (3) n) ⊤ \leftrightarrow \exists c (c \in ((O \cap ℙ) repr (3) n) \land ⊤)$
114	112 113	sylibr	$⊢ (n \in O \land 10^{27} < n) \to \exists c \in ((O \cap ℙ) repr (3) n) ⊤$
115	92 114	r19.29a	$⊢ (n \in O \land 10^{27} < n) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r)$
116	2	eleq2i	$⊢ n \in G \leftrightarrow n \in \{z \in O \| \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r)\}$
117		eqeq1	$⊢ z = n \to (z = p + q + r \leftrightarrow n = p + q + r)$
118	117	anbi2d	$⊢ z = n \to (((p \in O \land q \in O \land r \in O) \land z = p + q + r) \leftrightarrow ((p \in O \land q \in O \land r \in O) \land n = p + q + r))$
119	118	rexbidv	$⊢ z = n \to (\exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r) \leftrightarrow \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r))$
120	119	rexbidv	$⊢ z = n \to (\exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r) \leftrightarrow \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r))$
121	120	rexbidv	$⊢ z = n \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r) \leftrightarrow \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r))$
122	121	elrab3	$⊢ n \in O \to (n \in \{z \in O \| \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land z = p + q + r)\} \leftrightarrow \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r))$
123	116 122	bitrid	$⊢ n \in O \to (n \in G \leftrightarrow \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r))$
124	123	biimpar	$⊢ (n \in O \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in O \land q \in O \land r \in O) \land n = p + q + r)) \to n \in G$
125	11 115 124	syl2anc	$⊢ (n \in O \land 10^{27} < n) \to n \in G$
126	125	ex	$⊢ n \in O \to (10^{27} < n \to n \in G)$
127	126	rgen	$⊢ \forall n \in O (10^{27} < n \to n \in G)$
128	10 127	pm3.2i	$⊢ (10^{27} \leq 10^{27} \land \forall n \in O (10^{27} < n \to n \in G))$
129		breq1	$⊢ m = 10^{27} \to (m \leq 10^{27} \leftrightarrow 10^{27} \leq 10^{27})$
130		breq1	$⊢ m = 10^{27} \to (m < n \leftrightarrow 10^{27} < n)$
131	130	imbi1d	$⊢ m = 10^{27} \to ((m < n \to n \in G) \leftrightarrow (10^{27} < n \to n \in G))$
132	131	ralbidv	$⊢ m = 10^{27} \to (\forall n \in O (m < n \to n \in G) \leftrightarrow \forall n \in O (10^{27} < n \to n \in G))$
133	129 132	anbi12d	$⊢ m = 10^{27} \to ((m \leq 10^{27} \land \forall n \in O (m < n \to n \in G)) \leftrightarrow (10^{27} \leq 10^{27} \land \forall n \in O (10^{27} < n \to n \in G)))$
134	133	rspcev	$⊢ (10^{27} \in ℕ \land (10^{27} \leq 10^{27} \land \forall n \in O (10^{27} < n \to n \in G))) \to \exists m \in ℕ (m \leq 10^{27} \land \forall n \in O (m < n \to n \in G))$
135	8 128 134	mp2an	$⊢ \exists m \in ℕ (m \leq 10^{27} \land \forall n \in O (m < n \to n \in G))$

Metamath Proof Explorer

Theorem tgoldbachgt

Proof