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 44121
 Description: Temporary duplicate of tgoldbachgt 31942, provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than (;10↑;27) 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 𝐺 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 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
ax-tgoldbachgt.g 𝐺 = {𝑧𝑂 ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝𝑂𝑞𝑂𝑟𝑂) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))}
Assertion
Ref Expression
ax-tgoldbachgt 𝑚 ∈ ℕ (𝑚 ≤ (10↑27) ∧ ∀𝑛𝑂 (𝑚 < 𝑛𝑛𝐺))
Distinct variable groups:   𝑚,𝐺   𝑚,𝑂,𝑝,𝑞,𝑟,𝑧   𝑚,𝑛,𝑝,𝑞,𝑟,𝑧
Allowed substitution hints:   𝐺(𝑧,𝑛,𝑟,𝑞,𝑝)   𝑂(𝑛)

Detailed syntax breakdown of Axiom ax-tgoldbachgt
StepHypRef Expression
1 vm . . . . 5 setvar 𝑚
21cv 1536 . . . 4 class 𝑚
3 c1 10516 . . . . . 6 class 1
4 cc0 10515 . . . . . 6 class 0
53, 4cdc 12077 . . . . 5 class 10
6 c2 11671 . . . . . 6 class 2
7 c7 11676 . . . . . 6 class 7
86, 7cdc 12077 . . . . 5 class 27
9 cexp 13414 . . . . 5 class
105, 8, 9co 7133 . . . 4 class (10↑27)
11 cle 10654 . . . 4 class
122, 10, 11wbr 5042 . . 3 wff 𝑚 ≤ (10↑27)
13 vn . . . . . . 7 setvar 𝑛
1413cv 1536 . . . . . 6 class 𝑛
15 clt 10653 . . . . . 6 class <
162, 14, 15wbr 5042 . . . . 5 wff 𝑚 < 𝑛
17 cG . . . . . 6 class 𝐺
1814, 17wcel 2114 . . . . 5 wff 𝑛𝐺
1916, 18wi 4 . . . 4 wff (𝑚 < 𝑛𝑛𝐺)
20 cO . . . 4 class 𝑂
2119, 13, 20wral 3125 . . 3 wff 𝑛𝑂 (𝑚 < 𝑛𝑛𝐺)
2212, 21wa 398 . 2 wff (𝑚 ≤ (10↑27) ∧ ∀𝑛𝑂 (𝑚 < 𝑛𝑛𝐺))
23 cn 11616 . 2 class
2422, 1, 23wrex 3126 1 wff 𝑚 ∈ ℕ (𝑚 ≤ (10↑27) ∧ ∀𝑛𝑂 (𝑚 < 𝑛𝑛𝐺))
 Colors of variables: wff setvar class This axiom is referenced by:  tgoldbachgtALTV  44122
 Copyright terms: Public domain W3C validator