Axiom ax-tgoldbachgt

Description: Temporary duplicate of tgoldbachgt , provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: 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	ax-tgoldbachgt.o	$$⊢O=\left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}$$
	ax-tgoldbachgt.g	$$⊢G=\left\{z\in O|\exists p\in \mathbb{P}\exists q\in \mathbb{P}\exists r\in \mathbb{P}\left(\left(p\in O\wedge q\in O\wedge r\in O\right)\wedge z=p+q+r\right)\right\}$$
Assertion	ax-tgoldbachgt	$$⊢\exists m\in \mathbb{N}\left(m\le {10}^{27}\wedge \forall n\in O\left(m<n\to n\in G\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vm	$$setvarm$$
1		cn	$$class\mathbb{N}$$
2	0	cv	$$setvarm$$
3		cle	$$class\le$$
4		c1	$$class1$$
5		cc0	$$class0$$
6	4 5	cdc	$$class10$$
7		cexp	$$class^$$
8		c2	$$class2$$
9		c7	$$class7$$
10	8 9	cdc	$$class27$$
11	6 10 7	co	$$class{10}^{27}$$
12	2 11 3	wbr	$$wffm\le {10}^{27}$$
13		vn	$$setvarn$$
14		cO	$$classO$$
15		clt	$$class<$$
16	13	cv	$$setvarn$$
17	2 16 15	wbr	$$wffm<n$$
18		cG	$$classG$$
19	16 18	wcel	$$wffn\in G$$
20	17 19	wi	$$wff\left(m<n\to n\in G\right)$$
21	20 13 14	wral	$$wff\forall n\in O\left(m<n\to n\in G\right)$$
22	12 21	wa	$$wff\left(m\le {10}^{27}\wedge \forall n\in O\left(m<n\to n\in G\right)\right)$$
23	22 0 1	wrex	$$wff\exists m\in \mathbb{N}\left(m\le {10}^{27}\wedge \forall n\in O\left(m<n\to n\in G\right)\right)$$