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	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \leftrightarrow \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r$

Proof

Step	Hyp	Ref	Expression
1		sbgoldbm	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \to \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r$
2		mogoldbb	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \forall n \in Even (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
3		sbgoldbalt	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \leftrightarrow \forall n \in Even (2 < n \to \exists p \in ℙ \exists q \in ℙ n = p + q)$
4	2 3	sylibr	$⊢ \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r \to \forall n \in Even (4 < n \to n \in GoldbachEven)$
5	1 4	impbii	$⊢ \forall n \in Even (4 < n \to n \in GoldbachEven) \leftrightarrow \forall n \in ℤ_{\geq 6} \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ n = p + q + r$