Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-tgoldbachgt Structured version   Visualization version   GIF version

Axiom ax-tgoldbachgt 40231
 Description: The ternary Goldbach conjecture is valid for big odd numbers (i.e. for all odd numbers greater than a fixed 𝑚). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for m = 10^27. Temporarily provided as "axiom". (Contributed by AV, 2-Aug-2020.) (Revised by AV, 9-Sep-2021.)
Assertion
Ref Expression
ax-tgoldbachgt 𝑚 ∈ ℕ (𝑚 ≤ (10↑27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛𝑛 ∈ GoldbachOddALTV ))
Distinct variable group:   𝑚,𝑛

Detailed syntax breakdown of Axiom ax-tgoldbachgt
StepHypRef Expression
1 vm . . . . 5 setvar 𝑚
21cv 1474 . . . 4 class 𝑚
3 c1 9816 . . . . . 6 class 1
4 cc0 9815 . . . . . 6 class 0
53, 4cdc 11369 . . . . 5 class 10
6 c2 10947 . . . . . 6 class 2
7 c7 10952 . . . . . 6 class 7
86, 7cdc 11369 . . . . 5 class 27
9 cexp 12722 . . . . 5 class
105, 8, 9co 6549 . . . 4 class (10↑27)
11 cle 9954 . . . 4 class
122, 10, 11wbr 4583 . . 3 wff 𝑚 ≤ (10↑27)
13 vn . . . . . . 7 setvar 𝑛
1413cv 1474 . . . . . 6 class 𝑛
15 clt 9953 . . . . . 6 class <
162, 14, 15wbr 4583 . . . . 5 wff 𝑚 < 𝑛
17 cgboa 40169 . . . . . 6 class GoldbachOddALTV
1814, 17wcel 1977 . . . . 5 wff 𝑛 ∈ GoldbachOddALTV
1916, 18wi 4 . . . 4 wff (𝑚 < 𝑛𝑛 ∈ GoldbachOddALTV )
20 codd 40076 . . . 4 class Odd
2119, 13, 20wral 2896 . . 3 wff 𝑛 ∈ Odd (𝑚 < 𝑛𝑛 ∈ GoldbachOddALTV )
2212, 21wa 383 . 2 wff (𝑚 ≤ (10↑27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛𝑛 ∈ GoldbachOddALTV ))
23 cn 10897 . 2 class
2422, 1, 23wrex 2897 1 wff 𝑚 ∈ ℕ (𝑚 ≤ (10↑27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛𝑛 ∈ GoldbachOddALTV ))
 Colors of variables: wff setvar class This axiom is referenced by:  tgoldbach  40232
 Copyright terms: Public domain W3C validator