This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isgbo

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

		Ref	Expression
	Assertion	isgbo	$⊢ Z \in GoldbachOdd \leftrightarrow (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r))$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$⊢ z = Z \to (z = p + q + r \leftrightarrow Z = p + q + r)$
2	1	anbi2d	$⊢ z = Z \to (((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r) \leftrightarrow ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r))$
3	2	rexbidv	$⊢ z = Z \to (\exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r) \leftrightarrow \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r))$
4	3	2rexbidv	$⊢ z = Z \to (\exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r) \leftrightarrow \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r))$
5		df-gbo	$⊢ GoldbachOdd = \{z \in Odd \| \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r)\}$
6	4 5	elrab2	$⊢ Z \in GoldbachOdd \leftrightarrow (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r))$