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 ⊢ O = z ∈ ℤ | ¬ 2 ∥ z
ax-tgoldbachgt.g ⊢ G = z ∈ O | ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ O ∧ q ∈ O ∧ r ∈ O ∧ z = p + q + r
Assertion ax-tgoldbachgt ⊢ ∃ m ∈ ℕ m ≤ 10 27 ∧ ∀ n ∈ O m < n → n ∈ G

Detailed syntax breakdown

Step Hyp Ref Expression
0 vm setvar m
1 cn class ℕ
2 0 cv setvar m
3 cle class ≤
4 c1 class 1
5 cc0 class 0
6 4 5 cdc class 10
7 cexp class ^
8 c2 class 2
9 c7 class 7
10 8 9 cdc class 27
11 6 10 7 co class 10 27
12 2 11 3 wbr wff m ≤ 10 27
13 vn setvar n
14 cO class O
15 clt class <
16 13 cv setvar n
17 2 16 15 wbr wff m < n
18 cG class G
19 16 18 wcel wff n ∈ G
20 17 19 wi wff m < n → n ∈ G
21 20 13 14 wral wff ∀ n ∈ O m < n → n ∈ G
22 12 21 wa wff m ≤ 10 27 ∧ ∀ n ∈ O m < n → n ∈ G
23 22 0 1 wrex wff ∃ m ∈ ℕ m ≤ 10 27 ∧ ∀ n ∈ O m < n → n ∈ G