Metamath Proof Explorer


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