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	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sbgoldbalt	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
2	1	biimpi	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )