Axiom ax-tgoldbachgt 41699

Description: Temporary duplicate of tgoldbachgt 30741, 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
ax-tgoldbachgt	|- E. m e. NN ( m <_ (; 1 0 ^; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )

Distinct variable groups:   m, G   m, O, p, q, r, z   m, n, p, q, r, z

Allowed substitution hints:   G( z, n, r, q, p)   O( n)

Detailed syntax breakdown of Axiom ax-tgoldbachgt

Step	Hyp	Ref	Expression
1		vm	. . . . 5 setvar m
2	1	cv 1482	. . . 4 class m
3		c1 9937	. . . . . 6 class 1
4		cc0 9936	. . . . . 6 class 0
5	3, 4	cdc 11493	. . . . 5 class ; 1 0
6		c2 11070	. . . . . 6 class 2
7		c7 11075	. . . . . 6 class 7
8	6, 7	cdc 11493	. . . . 5 class ; 2 7
9		cexp 12860	. . . . 5 class ^
10	5, 8, 9	co 6650	. . . 4 class (; 1 0 ^; 2 7 )
11		cle 10075	. . . 4 class <_
12	2, 10, 11	wbr 4653	. . 3 wff m <_ (; 1 0 ^; 2 7 )
13		vn	. . . . . . 7 setvar n
14	13	cv 1482	. . . . . 6 class n
15		clt 10074	. . . . . 6 class <
16	2, 14, 15	wbr 4653	. . . . 5 wff m < n
17		cG	. . . . . 6 class G
18	14, 17	wcel 1990	. . . . 5 wff n e. G
19	16, 18	wi 4	. . . 4 wff ( m < n -> n e. G )
20		cO	. . . 4 class O
21	19, 13, 20	wral 2912	. . 3 wff A. n e. O ( m < n -> n e. G )
22	12, 21	wa 384	. 2 wff ( m <_ (; 1 0 ^; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )
23		cn 11020	. 2 class NN
24	22, 1, 23	wrex 2913	1 wff E. m e. NN ( m <_ (; 1 0 ^; 2 7 ) /\ A. n e. O ( m < n -> n e. G ) )

This axiom is referenced by:  tgoldbachgtALTV  41700