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	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )

Proof

Step	Hyp	Ref	Expression
1		sbgoldbm	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )
2		mogoldbb	⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
3		sbgoldbalt	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ Even ( 2 < 𝑛 → ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ 𝑛 = ( 𝑝 + 𝑞 ) ) )
4	2 3	sylibr	⊢ ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) → ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) )
5	1 4	impbii	⊢ ( ∀ 𝑛 ∈ Even ( 4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ 6 ) ∃ 𝑝 ∈ ℙ ∃ 𝑞 ∈ ℙ ∃ 𝑟 ∈ ℙ 𝑛 = ( ( 𝑝 + 𝑞 ) + 𝑟 ) )