11gbo

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

Proof

Step	Hyp	Ref	Expression
1		6p5e11	$⊢ 6 + 5 = 11$
2		6even	$⊢ 6 \in Even$
3		5odd	$⊢ 5 \in Odd$
4		epoo	$⊢ (6 \in Even \land 5 \in Odd) \to 6 + 5 \in Odd$
5	2 3 4	mp2an	$⊢ 6 + 5 \in Odd$
6	1 5	eqeltrri	$⊢ 11 \in Odd$
7		3prm	$⊢ 3 \in ℙ$
8		5prm	$⊢ 5 \in ℙ$
9		3odd	$⊢ 3 \in Odd$
10	9 9 3	3pm3.2i	$⊢ (3 \in Odd \land 3 \in Odd \land 5 \in Odd)$
11		gbpart11	$⊢ 11 = 3 + 3 + 5$
12	10 11	pm3.2i	$⊢ ((3 \in Odd \land 3 \in Odd \land 5 \in Odd) \land 11 = 3 + 3 + 5)$
13		eleq1	$⊢ r = 5 \to (r \in Odd \leftrightarrow 5 \in Odd)$
14	13	3anbi3d	$⊢ r = 5 \to ((3 \in Odd \land 3 \in Odd \land r \in Odd) \leftrightarrow (3 \in Odd \land 3 \in Odd \land 5 \in Odd))$
15		oveq2	$⊢ r = 5 \to 3 + 3 + r = 3 + 3 + 5$
16	15	eqeq2d	$⊢ r = 5 \to (11 = 3 + 3 + r \leftrightarrow 11 = 3 + 3 + 5)$
17	14 16	anbi12d	$⊢ r = 5 \to (((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 11 = 3 + 3 + r) \leftrightarrow ((3 \in Odd \land 3 \in Odd \land 5 \in Odd) \land 11 = 3 + 3 + 5))$
18	17	rspcev	$⊢ (5 \in ℙ \land ((3 \in Odd \land 3 \in Odd \land 5 \in Odd) \land 11 = 3 + 3 + 5)) \to \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 11 = 3 + 3 + r)$
19	8 12 18	mp2an	$⊢ \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 11 = 3 + 3 + r)$
20		eleq1	$⊢ p = 3 \to (p \in Odd \leftrightarrow 3 \in Odd)$
21	20	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))$
22		oveq1	$⊢ p = 3 \to p + q = 3 + q$
23	22	oveq1d	$⊢ p = 3 \to p + q + r = 3 + q + r$
24	23	eqeq2d	$⊢ p = 3 \to (11 = p + q + r \leftrightarrow 11 = 3 + q + r)$
25	21 24	anbi12d	$⊢ p = 3 \to (((p \in Odd \land q \in Odd \land r \in Odd) \land 11 = p + q + r) \leftrightarrow ((3 \in Odd \land q \in Odd \land r \in Odd) \land 11 = 3 + q + r))$
26	25	rexbidv	$⊢ p = 3 \to (\exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 11 = p + q + r) \leftrightarrow \exists r \in ℙ ((3 \in Odd \land q \in Odd \land r \in Odd) \land 11 = 3 + q + r))$
27		eleq1	$⊢ q = 3 \to (q \in Odd \leftrightarrow 3 \in Odd)$
28	27	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))$
29		oveq2	$⊢ q = 3 \to 3 + q = 3 + 3$
30	29	oveq1d	$⊢ q = 3 \to 3 + q + r = 3 + 3 + r$
31	30	eqeq2d	$⊢ q = 3 \to (11 = 3 + q + r \leftrightarrow 11 = 3 + 3 + r)$
32	28 31	anbi12d	$⊢ q = 3 \to (((3 \in Odd \land q \in Odd \land r \in Odd) \land 11 = 3 + q + r) \leftrightarrow ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 11 = 3 + 3 + r))$
33	32	rexbidv	$⊢ q = 3 \to (\exists r \in ℙ ((3 \in Odd \land q \in Odd \land r \in Odd) \land 11 = 3 + q + r) \leftrightarrow \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 11 = 3 + 3 + r))$
34	26 33	rspc2ev	$⊢ (3 \in ℙ \land 3 \in ℙ \land \exists r \in ℙ ((3 \in Odd \land 3 \in Odd \land r \in Odd) \land 11 = 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 11 = p + q + r)$
35	7 7 19 34	mp3an	$⊢ \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 11 = p + q + r)$
36		isgbo	$⊢ 11 \in GoldbachOdd \leftrightarrow (11 \in Odd \land \exists p \in ℙ \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land 11 = p + q + r))$
37	6 35 36	mpbir2an	$⊢ 11 \in GoldbachOdd$

Metamath Proof Explorer

Theorem 11gbo

Proof