Definition df-gbe 46993

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 46990	. 2 class GoldbachEven
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1532	. . . . . . 7 class 𝑝
4		codd 46870	. . . . . . 7 class Odd
5	3, 4	wcel 2098	. . . . . 6 wff 𝑝 ∈ Odd
6		vq	. . . . . . . 8 setvar 𝑞
7	6	cv 1532	. . . . . . 7 class 𝑞
8	7, 4	wcel 2098	. . . . . 6 wff 𝑞 ∈ Odd
9		vz	. . . . . . . 8 setvar 𝑧
10	9	cv 1532	. . . . . . 7 class 𝑧
11		caddc 11115	. . . . . . . 8 class +
12	3, 7, 11	co 7405	. . . . . . 7 class (𝑝 + 𝑞)
13	10, 12	wceq 1533	. . . . . 6 wff 𝑧 = (𝑝 + 𝑞)
14	5, 8, 13	w3a 1084	. . . . 5 wff (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
15		cprime 16615	. . . . 5 class ℙ
16	14, 6, 15	wrex 3064	. . . 4 wff ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
17	16, 2, 15	wrex 3064	. . 3 wff ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))
18		ceven 46869	. . 3 class Even
19	17, 9, 18	crab 3426	. 2 class {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}
20	1, 19	wceq 1533	1 wff GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))}

This definition is referenced by:  isgbe  46996