Metamath Proof Explorer

Theorem sbgoldbb

Description: If the strong binary Goldbach conjecture is valid, the binary Goldbach conjecture is valid. (Contributed by AV, 23-Dec-2021)

Ref Expression
Assertion sbgoldbb ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ n ∈ Even 2 < n → ∃ p ∈ ℙ ∃ q ∈ ℙ n = p + q

Proof

Step Hyp Ref Expression
1 sbgoldbalt ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven ↔ ∀ n ∈ Even 2 < n → ∃ p ∈ ℙ ∃ q ∈ ℙ n = p + q
2 1 biimpi ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ n ∈ Even 2 < n → ∃ p ∈ ℙ ∃ q ∈ ℙ n = p + q