Definition df-gbe 48375

Description: Define the set of (even) Goldbach numbers, which are positive even integers that can be expressed as the sum of two odd primes. By this definition, the binary Goldbach conjecture can be expressed as ∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ). (Contributed by AV, 14-Jun-2020.)

Assertion

Ref	Expression
df-gbe	⊢ GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

Distinct variable group:   𝑧,𝑝,𝑞

Detailed syntax breakdown of Definition df-gbe

Step	Hyp	Ref	Expression
1		cgbe 48372	. 2 class GoldbachEven
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1561	. . . . . . 7 class 𝑝
4		codd 48252	. . . . . . 7 class Odd
5	3, 4	wcel 2144	. . . . . 6 wff 𝑝 ∈ Odd
6		vq	. . . . . . . 8 setvar 𝑞
7	6	cv 1561	. . . . . . 7 class 𝑞
8	7, 4	wcel 2144	. . . . . 6 wff 𝑞 ∈ Odd
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1561	. . . . . . 7 class 𝑧
11		caddc 11078	. . . . . . . 8 class +
12	3, 7, 11	co 7398	. . . . . . 7 class (𝑝 + 𝑞)
13	10, 12	wceq 1562	. . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
14	5, 8, 13	w3a 1099	. . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15		cprime 16707	. . . . 5 class ℙ
16	14, 6, 15	wrex 3088	. . . 4 wff ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
17	16, 2, 15	wrex 3088	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18		ceven 48251	. . 3 class Even
19	17, 9, 18	crab 3416	. 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
20	1, 19	wceq 1562	1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

This definition is referenced by:  isgbe  48378