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 ) ) }