Description: Variant of Thierry Arnoux's tgoldbachgt using the symbols Odd and GoldbachOdd : The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed m ). This is proven by Helfgott (see section 7.4 in Helfgott p. 70) for m = 10^27. (Contributed by AV, 2-Aug-2020) (Revised by AV, 15-Jan-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | tgoldbachgtALTV | |- E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. Odd ( m < n -> n e. GoldbachOdd ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfodd3 | |- Odd = { z e. ZZ | -. 2 || z } |
|
| 2 | df-gbo | |- GoldbachOdd = { z e. Odd | E. p e. Prime E. q e. Prime E. r e. Prime ( ( p e. Odd /\ q e. Odd /\ r e. Odd ) /\ z = ( ( p + q ) + r ) ) } |
|
| 3 | 1 2 | ax-tgoldbachgt | |- E. m e. NN ( m <_ ( ; 1 0 ^ ; 2 7 ) /\ A. n e. Odd ( m < n -> n e. GoldbachOdd ) ) |