Definition df-gbe 47622

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 47619	. 2 class GoldbachEven
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1536	. . . . . . 7 class 𝑝
4		codd 47499	. . . . . . 7 class Odd
5	3, 4	wcel 2108	. . . . . 6 wff 𝑝 ∈ Odd
6		vq	. . . . . . . 8 setvar 𝑞
7	6	cv 1536	. . . . . . 7 class 𝑞
8	7, 4	wcel 2108	. . . . . 6 wff 𝑞 ∈ Odd
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1536	. . . . . . 7 class 𝑧
11		caddc 11187	. . . . . . . 8 class +
12	3, 7, 11	co 7448	. . . . . . 7 class (𝑝 + 𝑞)
13	10, 12	wceq 1537	. . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
14	5, 8, 13	w3a 1087	. . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15		cprime 16718	. . . . 5 class ℙ
16	14, 6, 15	wrex 3076	. . . 4 wff ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
17	16, 2, 15	wrex 3076	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18		ceven 47498	. . 3 class Even
19	17, 9, 18	crab 3443	. 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
20	1, 19	wceq 1537	1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

This definition is referenced by:  isgbe  47625