This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ∧ ∀ 𝑛 ∈ 𝑂 ( 𝑚 < 𝑛 → 𝑛 ∈ 𝐺 ) )