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	$⊢ \exists m \in ℕ (m \leq 10^{27} \land \forall n \in Odd (m < n \to n \in GoldbachOdd))$

Proof

Step	Hyp	Ref	Expression
1		dfodd3	$⊢ Odd = \{z \in ℤ \| \neg 2 ∥ z\}$
2		df-gbo	$⊢ GoldbachOdd = \{z \in Odd \| \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r)\}$
3	1 2	ax-tgoldbachgt	$⊢ \exists m \in ℕ (m \leq 10^{27} \land \forall n \in Odd (m < n \to n \in GoldbachOdd))$