Axiom ax-tgoldbachgt

Description: Temporary duplicate of tgoldbachgt , provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than ( ; 1 0 ^ ; 2 7 ) 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 G of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021)

	Ref	Expression
Hypotheses	ax-tgoldbachgt.o	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
	ax-tgoldbachgt.g	⊢ 𝐺 = { 𝑧 ∈ 𝑂 ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂 ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }
Assertion	ax-tgoldbachgt	⊢ ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( ; 1 0 ↑ ; 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vm	⊢ 𝑚
1		cn	⊢ ℕ
2	0	cv	⊢ 𝑚
3		cle	⊢ ≤
4		c1	⊢ 1
5		cc0	⊢ 0
6	4 5	cdc	⊢ ; 1 0
7		cexp	⊢ ↑
8		c2	⊢ 2
9		c7	⊢ 7
10	8 9	cdc	⊢ ; 2 7
11	6 10 7	co	⊢ ( ; 1 0 ↑ ; 2 7 )
12	2 11 3	wbr	⊢ 𝑚 ≤ ( ; 1 0 ↑ ; 2 7 )
13		vn	⊢ 𝑛
14		cO	⊢ 𝑂
15		clt	⊢ <
16	13	cv	⊢ 𝑛
17	2 16 15	wbr	⊢ 𝑚 < 𝑛
18		cG	⊢ 𝐺
19	16 18	wcel	⊢ 𝑛 ∈ 𝐺
20	17 19	wi	⊢ ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 )
21	20 13 14	wral	⊢ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 )
22	12 21	wa	⊢ ( 𝑚 ≤ ( ; 1 0 ↑ ; 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) )
23	22 0 1	wrex	⊢ ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( ; 1 0 ↑ ; 2 7 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) )