Metamath Proof Explorer

Theorem stgoldbnnsum4prm

Description: If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020)

		Ref	Expression
	Assertion	stgoldbnnsum4prm	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to \forall n \in ℤ_{\geq 2} \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$

Proof

Step	Hyp	Ref	Expression
1		stgoldbwt	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to \forall m \in Odd (5 < m \to m \in GoldbachOddW)$
2		wtgoldbnnsum4prm	$⊢ \forall m \in Odd (5 < m \to m \in GoldbachOddW) \to \forall n \in ℤ_{\geq 2} \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$
3	1 2	syl	$⊢ \forall m \in Odd (7 < m \to m \in GoldbachOdd) \to \forall n \in ℤ_{\geq 2} \exists d \in ℕ \exists f \in (ℙ^{(1 \dots d)}) (d \leq 4 \land n = \sum_{k = 1}^{d} f (k))$