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

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 ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ Odd ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) )

Proof

Step Hyp Ref Expression
1 dfodd3 ⊢ Odd = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2 df-gbo ⊢ GoldbachOdd = { 𝑧 ∈ Odd ∣ ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ ( ( 𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) ) }
3 1 2 ax-tgoldbachgt ⊢ ∃ 𝑚 ∈ ℕ ( 𝑚 ≤ ( 1 0 ↑ 2 7 ) ∧ ∀ 𝑛 ∈ Odd ( 𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd ) )