Metamath Proof Explorer

Theorem isgbe

Description: The predicate "is an even Goldbach number". An even Goldbach number is an even integer having a Goldbach partition, i.e. which can be written as a sum of two odd primes. (Contributed by AV, 20-Jul-2020)

		Ref	Expression
	Assertion	isgbe	$⊢ Z \in GoldbachEven \leftrightarrow (Z \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q))$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ z = Z \to (z = p + q \leftrightarrow Z = p + q)$
2	1	3anbi3d	$⊢ z = Z \to ((p \in Odd \land q \in Odd \land z = p + q) \leftrightarrow (p \in Odd \land q \in Odd \land Z = p + q))$
3	2	2rexbidv	$⊢ z = Z \to (\exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land z = p + q) \leftrightarrow \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q))$
4		df-gbe	$⊢ GoldbachEven = \{z \in Even \| \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land z = p + q)\}$
5	3 4	elrab2	$⊢ Z \in GoldbachEven \leftrightarrow (Z \in Even \land \exists p \in ℙ \exists q \in ℙ (p \in Odd \land q \in Odd \land Z = p + q))$