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 ) )