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 ⊢ ∀ m ∈ Odd 7 < m → m ∈ GoldbachOdd → ∀ n ∈ ℤ ≥ 2 ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ n = ∑ k = 1 d f ⁡ k

Proof

Step Hyp Ref Expression
1 stgoldbwt ⊢ ∀ m ∈ Odd 7 < m → m ∈ GoldbachOdd → ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW
2 wtgoldbnnsum4prm ⊢ ∀ m ∈ Odd 5 < m → m ∈ GoldbachOddW → ∀ n ∈ ℤ ≥ 2 ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ n = ∑ k = 1 d f ⁡ k
3 1 2 syl ⊢ ∀ m ∈ Odd 7 < m → m ∈ GoldbachOdd → ∀ n ∈ ℤ ≥ 2 ∃ d ∈ ℕ ∃ f ∈ ℙ 1 … d d ≤ 4 ∧ n = ∑ k = 1 d f ⁡ k