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 = { z e. ZZ | -. 2 || z }
	ax-tgoldbachgt.g	|- G = { z e. O | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. O /\ q e. O /\ r e. O ) /\ z = ( ( p + q ) + r ) ) }
Assertion	ax-tgoldbachgt	|- E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vm	|- m
1		cn	|- NN
2	0	cv	|- m
3		cle	|- <_
4		c1	|- 1
5		cc0	|- 0
6	4 5	cdc	|- ; 1 0
7		cexp	|- ^
8		c2	|- 2
9		c7	|- 7
10	8 9	cdc	|- ; 2 7
11	6 10 7	co	|- ( ; 1 0 ^ ; 2 7 )
12	2 11 3	wbr	|- m <_ ( ; 1 0 ^ ; 2 7 )
13		vn	|- n
14		cO	|- O
15		clt	|- <
16	13	cv	|- n
17	2 16 15	wbr	|- m < n
18		cG	|- G
19	16 18	wcel	|- n e. G
20	17 19	wi	|- ( m < n -> n e. G )
21	20 13 14	wral	|- A. n e. O ( m < n -> n e. G )
22	12 21	wa	|- ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )
23	22 0 1	wrex	|- E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )