Axiom ax-tgoldbachgt 45151

Description: Temporary duplicate of tgoldbachgt 32543, 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

Step	Hyp	Ref	Expression
1		vm	. . . . 5 setvar 𝑚
2	1	cv 1538	. . . 4 class 𝑚
3		c1 10803	. . . . . 6 class 1
4		cc0 10802	. . . . . 6 class 0
5	3, 4	cdc 12366	. . . . 5 class ;10
6		c2 11958	. . . . . 6 class 2
7		c7 11963	. . . . . 6 class 7
8	6, 7	cdc 12366	. . . . 5 class ;27
9		cexp 13710	. . . . 5 class ↑
10	5, 8, 9	co 7255	. . . 4 class (;10↑;27)
11		cle 10941	. . . 4 class ≤
12	2, 10, 11	wbr 5070	. . 3 wff 𝑚 ≤ (;10↑;27)
13		vn	. . . . . . 7 setvar 𝑛
14	13	cv 1538	. . . . . 6 class 𝑛
15		clt 10940	. . . . . 6 class <
16	2, 14, 15	wbr 5070	. . . . 5 wff 𝑚 < 𝑛
17		cG	. . . . . 6 class 𝐺
18	14, 17	wcel 2108	. . . . 5 wff 𝑛 ∈ 𝐺
19	16, 18	wi 4	. . . 4 wff (𝑚 < 𝑛 → 𝑛 ∈ 𝐺)
20		cO	. . . 4 class 𝑂
21	19, 13, 20	wral 3063	. . 3 wff ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺)
22	12, 21	wa 395	. 2 wff (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))
23		cn 11903	. 2 class ℕ
24	22, 1, 23	wrex 3064	1 wff ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))

This axiom is referenced by:  tgoldbachgtALTV  45152