Metamath Proof Explorer

Theorem tgoldbachgtALTV

Description: Variant of Thierry Arnoux's tgoldbachgt using the symbols Odd and GoldbachOdd : The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed m ). This is proven by Helfgott (see section 7.4 in Helfgott p. 70) for m = 10^27. (Contributed by AV, 2-Aug-2020) (Revised by AV, 15-Jan-2022)

Ref Expression
Assertion tgoldbachgtALTV ⊢ ∃ m ∈ ℕ m ≤ 10 27 ∧ ∀ n ∈ Odd m < n → n ∈ GoldbachOdd

Proof

Step Hyp Ref Expression
1 dfodd3 ⊢ Odd = z ∈ ℤ | ¬ 2 ∥ z
2 df-gbo ⊢ GoldbachOdd = z ∈ Odd | ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ p ∈ Odd ∧ q ∈ Odd ∧ r ∈ Odd ∧ z = p + q + r
3 1 2 ax-tgoldbachgt ⊢ ∃ m ∈ ℕ m ≤ 10 27 ∧ ∀ n ∈ Odd m < n → n ∈ GoldbachOdd