df-gbo

Description: Define the set of (strong) odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of threeodd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as A. m e. Odd ( 7 < m -> m e. GoldbachOdd ) . (Contributed by AV, 26-Jul-2020)

		Ref	Expression
	Assertion	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)\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgbo	$class GoldbachOdd$
1		vz	$setvar z$
2		codd	$class Odd$
3		vp	$setvar p$
4		cprime	$class ℙ$
5		vq	$setvar q$
6		vr	$setvar r$
7	3	cv	$setvar p$
8	7 2	wcel	$wff p \in Odd$
9	5	cv	$setvar q$
10	9 2	wcel	$wff q \in Odd$
11	6	cv	$setvar r$
12	11 2	wcel	$wff r \in Odd$
13	8 10 12	w3a	$wff (p \in Odd \land q \in Odd \land r \in Odd)$
14	1	cv	$setvar z$
15		caddc	$class +$
16	7 9 15	co	$class (p + q)$
17	16 11 15	co	$class (p + q + r)$
18	14 17	wceq	$wff z = p + q + r$
19	13 18	wa	$wff ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r)$
20	19 6 4	wrex	$wff \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r)$
21	20 5 4	wrex	$wff \exists q \in ℙ \exists r \in ℙ ((p \in Odd \land q \in Odd \land r \in Odd) \land z = p + q + r)$
22	21 3 4	wrex	$wff \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)$
23	22 1 2	crab	$class \{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)\}$
24	0 23	wceq	$wff 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)\}$

Metamath Proof Explorer

Definition df-gbo

Detailed syntax breakdown