gbogbow

Description: A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020)

		Ref	Expression
	Assertion	gbogbow	$⊢ Z \in GoldbachOdd \to Z \in GoldbachOddW$

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to Z = p + q + r$
2	1	reximi	$⊢ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to \exists r \in ℙ Z = p + q + r$
3	2	reximi	$⊢ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land Z = p + q + r) \to \exists q \in ℙ \exists r \in ℙ Z = p + q + r$
4	3	reximi	$⊢ \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) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r$
5	4	anim2i	$⊢ (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)) \to (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r)$
6		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))$
7		isgbow	$⊢ Z \in GoldbachOddW \leftrightarrow (Z \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ Z = p + q + r)$
8	5 6 7	3imtr4i	$⊢ Z \in GoldbachOdd \to Z \in GoldbachOddW$

Metamath Proof Explorer