Axiom ax-tgoldbachgt 45263

Description: Temporary duplicate of tgoldbachgt 32643, 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 10872	. . . . . 6 class 1
4		cc0 10871	. . . . . 6 class 0
5	3, 4	cdc 12437	. . . . 5 class ;10
6		c2 12028	. . . . . 6 class 2
7		c7 12033	. . . . . 6 class 7
8	6, 7	cdc 12437	. . . . 5 class ;27
9		cexp 13782	. . . . 5 class ↑
10	5, 8, 9	co 7275	. . . 4 class (;10↑;27)
11		cle 11010	. . . 4 class ≤
12	2, 10, 11	wbr 5074	. . 3 wff 𝑚 ≤ (;10↑;27)
13		vn	. . . . . . 7 setvar 𝑛
14	13	cv 1538	. . . . . 6 class 𝑛
15		clt 11009	. . . . . 6 class <
16	2, 14, 15	wbr 5074	. . . . 5 wff 𝑚 < 𝑛
17		cG	. . . . . 6 class 𝐺
18	14, 17	wcel 2106	. . . . 5 wff 𝑛 ∈ 𝐺
19	16, 18	wi 4	. . . 4 wff (𝑚 < 𝑛 → 𝑛 ∈ 𝐺)
20		cO	. . . 4 class 𝑂
21	19, 13, 20	wral 3064	. . 3 wff ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺)
22	12, 21	wa 396	. 2 wff (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))
23		cn 11973	. 2 class ℕ
24	22, 1, 23	wrex 3065	1 wff ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺))

This axiom is referenced by:  tgoldbachgtALTV  45264