Metamath Proof Explorer

Theorem sbgoldbmb

Description: The strong binary Goldbach conjecture and the modern version of the original formulation of the Goldbach conjecture are equivalent. (Contributed by AV, 26-Dec-2021)

Ref Expression
Assertion sbgoldbmb ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven ↔ ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r

Proof

Step Hyp Ref Expression
1 sbgoldbm ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven → ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r
2 mogoldbb ⊢ ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r → ∀ n ∈ Even 2 < n → ∃ p ∈ ℙ ∃ q ∈ ℙ n = p + q
3 sbgoldbalt ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven ↔ ∀ n ∈ Even 2 < n → ∃ p ∈ ℙ ∃ q ∈ ℙ n = p + q
4 2 3 sylibr ⊢ ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r → ∀ n ∈ Even 4 < n → n ∈ GoldbachEven
5 1 4 impbii ⊢ ∀ n ∈ Even 4 < n → n ∈ GoldbachEven ↔ ∀ n ∈ ℤ ≥ 6 ∃ p ∈ ℙ ∃ q ∈ ℙ ∃ r ∈ ℙ n = p + q + r