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

Step	Hyp	Ref	Expression
1		vm	. . . . 5 setvar 𝑚
2	1	cv 1474	. . . 4 class 𝑚
3		c1 9816	. . . . . 6 class 1
4		cc0 9815	. . . . . 6 class 0
5	3, 4	cdc 11369	. . . . 5 class ;10
6		c2 10947	. . . . . 6 class 2
7		c7 10952	. . . . . 6 class 7
8	6, 7	cdc 11369	. . . . 5 class ;27
9		cexp 12722	. . . . 5 class ↑
10	5, 8, 9	co 6549	. . . 4 class (;10↑;27)
11		cle 9954	. . . 4 class ≤
12	2, 10, 11	wbr 4583	. . 3 wff 𝑚 ≤ (;10↑;27)
13		vn	. . . . . . 7 setvar 𝑛
14	13	cv 1474	. . . . . 6 class 𝑛
15		clt 9953	. . . . . 6 class <
16	2, 14, 15	wbr 4583	. . . . 5 wff 𝑚 < 𝑛
17		cgboa 40169	. . . . . 6 class GoldbachOddALTV
18	14, 17	wcel 1977	. . . . 5 wff 𝑛 ∈ GoldbachOddALTV
19	16, 18	wi 4	. . . 4 wff (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )
20		codd 40076	. . . 4 class Odd
21	19, 13, 20	wral 2896	. . 3 wff ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV )
22	12, 21	wa 383	. 2 wff (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ))
23		cn 10897	. 2 class ℕ
24	22, 1, 23	wrex 2897	1 wff ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ))

This axiom is referenced by:  tgoldbach  40232