9gbo

		Ref	Expression
	Assertion	9gbo	$⊢ 9 \in GoldbachOdd$

Proof

Step	Hyp	Ref	Expression
1		df-9	$⊢ 9 = 8 + 1$
2		8even	$⊢ 8 \in Even$
3		evenp1odd	$⊢ 8 \in Even \to 8 + 1 \in Odd$
4	2 3	ax-mp	$⊢ 8 + 1 \in Odd$
5	1 4	eqeltri	$⊢ 9 \in Odd$
6		3prm	$⊢ 3 \in ℙ$
7		3odd	$⊢ 3 \in Odd$
8	7 7 7	3pm3.2i	$⊢ (3 \in Odd \land 3 \in Odd \land 3 \in Odd)$
9		gbpart9	$⊢ 9 = 3 + 3 + 3$
10	8 9	pm3.2i	$⊢ ((3 \in Odd \land 3 \in Odd \land 3 \in Odd) \land 9 = 3 + 3 + 3)$
11		eleq1	$⊢ r = 3 \to (r \in Odd \leftrightarrow 3 \in Odd)$
12	11	3anbi3d	$⊢ r = 3 \to ((3 \in Odd \land 3 \in Odd \land r \in Odd) \leftrightarrow (3 \in Odd \land 3 \in Odd \land 3 \in Odd))$
13		oveq2	$⊢ r = 3 \to 3 + 3 + r = 3 + 3 + 3$
14	13	eqeq2d	$⊢ r = 3 \to (9 = 3 + 3 + r \leftrightarrow 9 = 3 + 3 + 3)$
15	12 14	anbi12d	$⊢ r = 3 \to (((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 9 = 3 + 3 + r) \leftrightarrow ((3 \in Odd \land 3 \in Odd \land 3 \in Odd) \land 9 = 3 + 3 + 3))$
16	15	rspcev	$⊢ (3 \in ℙ \land ((3 \in Odd \land 3 \in Odd \land 3 \in Odd) \land 9 = 3 + 3 + 3)) \to \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 9 = 3 + 3 + r)$
17	6 10 16	mp2an	$⊢ \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 9 = 3 + 3 + r)$
18		eleq1	$⊢ p = 3 \to (p \in Odd \leftrightarrow 3 \in Odd)$
19	18	3anbi1d	$⊢ p = 3 \to ((p \in Odd \land q \in Odd \land r \in Odd) \leftrightarrow (3 \in Odd \land q \in Odd \land r \in Odd))$
20		oveq1	$⊢ p = 3 \to p + q = 3 + q$
21	20	oveq1d	$⊢ p = 3 \to p + q + r = 3 + q + r$
22	21	eqeq2d	$⊢ p = 3 \to (9 = p + q + r \leftrightarrow 9 = 3 + q + r)$
23	19 22	anbi12d	$⊢ p = 3 \to (((p \in Odd \land q \in Odd \land r \in Odd) \land 9 = p + q + r) \leftrightarrow ((3 \in Odd \land q \in Odd \land r \in Odd) \land 9 = 3 + q + r))$
24	23	rexbidv	$⊢ p = 3 \to (\exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 9 = p + q + r) \leftrightarrow \exists r \in ℙ ((3 \in Odd \land q \in Odd \land r \in Odd) \land 9 = 3 + q + r))$
25		eleq1	$⊢ q = 3 \to (q \in Odd \leftrightarrow 3 \in Odd)$
26	25	3anbi2d	$⊢ q = 3 \to ((3 \in Odd \land q \in Odd \land r \in Odd) \leftrightarrow (3 \in Odd \land 3 \in Odd \land r \in Odd))$
27		oveq2	$⊢ q = 3 \to 3 + q = 3 + 3$
28	27	oveq1d	$⊢ q = 3 \to 3 + q + r = 3 + 3 + r$
29	28	eqeq2d	$⊢ q = 3 \to (9 = 3 + q + r \leftrightarrow 9 = 3 + 3 + r)$
30	26 29	anbi12d	$⊢ q = 3 \to (((3 \in Odd \land q \in Odd \land r \in Odd) \land 9 = 3 + q + r) \leftrightarrow ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 9 = 3 + 3 + r))$
31	30	rexbidv	$⊢ q = 3 \to (\exists r \in ℙ ((3 \in Odd \land q \in Odd \land r \in Odd) \land 9 = 3 + q + r) \leftrightarrow \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 9 = 3 + 3 + r))$
32	24 31	rspc2ev	$⊢ (3 \in ℙ \land 3 \in ℙ \land \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 9 = 3 + 3 + r)) \to \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 9 = p + q + r)$
33	6 6 17 32	mp3an	$⊢ \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 9 = p + q + r)$
34		isgbo	$⊢ 9 \in GoldbachOdd \leftrightarrow (9 \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 9 = p + q + r))$
35	5 33 34	mpbir2an	$⊢ 9 \in GoldbachOdd$

Metamath Proof Explorer

Theorem 9gbo

Proof