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	⊢ ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )

Proof

Step	Hyp	Ref	Expression
1		stgoldbwt	⊢ ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) )
2		wtgoldbnnsum4prm	⊢ ( ∀ 𝑚 ∈ Odd ( 5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )
3	1 2	syl	⊢ ( ∀ 𝑚 ∈ Odd ( 7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 2 ) ∃ 𝑑 ∈ ℕ ∃ 𝑓 ∈ ( ℙ ↑m ( 1 ... 𝑑 ) ) ( 𝑑 ≤ 4 ∧ 𝑛 = Σ 𝑘 ∈ ( 1 ... 𝑑 ) ( 𝑓 ‘ 𝑘 ) ) )